-- The exchange improves the decomposition: the partition sequence and the
-- chosen colours agree with the original below the level of the exchanged
-- edge, and at that level the exchange is coarser or chooses a larger
-- colour, so it precedes the original in the order.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.GraphTheory.TreePacking.ExchangeOrder
import Exchange

-- Connectivity of a vertex set is monotone in the edge set, and survives
-- the replacement of an edge whose ends the new edges join.
theorem Connects.monotone (S leftEnd rightEnd F G : Set)
  requires subset : F ⊆ G
  requires connected : Connects(S, leftEnd, rightEnd, F)
  shows Connects(S, leftEnd, rightEnd, G)
proof
  intros u hu v hv
  exact Joined.monotone with subset, (connected with u, hu, v, hv)

theorem Connects.replace_edge (V S leftEnd rightEnd F G g : Set)
  requires ends : ∀ h ∈ G, leftEnd(h) ∈ V ∧ rightEnd(h) ∈ V
  requires edgeEnds : leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V
  requires cover : F ⊆ G ∪ {g}
  requires bridged : Joined(leftEnd, rightEnd, G, leftEnd(g), rightEnd(g))
  requires connected : Connects(S, leftEnd, rightEnd, F)
  shows Connects(S, leftEnd, rightEnd, G)
proof
  intros u hu v hv
  have joined := Joined.monotone with cover, (connected with u, hu, v, hv)
  exact Joined.drop_edge with ends, edgeEnds, joined, bridged

-- A component of F within X is connected by the edges of F inside it.
theorem componentBy.connects_inside (X leftEnd rightEnd F u : Set)
  requires ends : ∀ e ∈ F, leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X
  requires vertex : u ∈ X
  shows Connects(componentBy(X, leftEnd, rightEnd, F, u), leftEnd, rightEnd,
    inside(leftEnd, rightEnd, F, componentBy(X, leftEnd, rightEnd, F, u)))
proof
  have closed := componentBy.closed at X, leftEnd, rightEnd, F, u with ends
  intros v hv w hw
  obtain ⟨vIn, joinedV⟩ := hv
  obtain ⟨_, joinedW⟩ := hw
  have back := Joined.symmetric with ends, vertex, vIn, joinedV
  have joined := Joined.transitive with back, joinedW
  exact Joined.inside with closed, hv, joined

-- In an even set whose edges all keep their ends within classes of P, the
-- ends of an edge inside the class S are joined by the other edges inside S.
theorem EvenEdgeSet.joined_inside (V P S leftEnd rightEnd C h : Set)
  requires finiteVertices : Finite(V)
  requires partition : Partition(V, P)
  requires class : S ∈ P
  requires ends : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V
  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)
  requires edge : h ∈ C
  requires inside : leftEnd(h) ∈ S ∧ rightEnd(h) ∈ S
  requires together :
    ∀ g ∈ C, ∃ Y ∈ P, leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y
  shows Joined(leftEnd, rightEnd, inside(leftEnd, rightEnd, C ∖ {h}, S),
    leftEnd(h), rightEnd(h))
proof
  have closed : ClosedUnder(leftEnd, rightEnd, C, S)
    intros g inC
    obtain ⟨Y, classY, leftY, rightY⟩ := together with g, inC
    by_cases same : S = Y
    . rw same
      tauto
    . have apartSY := Disjoint.iff.forward
        with (partition.right.left with S, class, Y, classY, same)
      constructor
      . intro leftS
        exfalso
        exact apartSY with leftEnd(g), leftS, leftY
      . intro rightS
        exfalso
        exact apartSY with rightEnd(g), rightS, rightY
  have joinedC := EvenEdgeSet.ends_joined with finiteVertices, ends, even, edge
  have restSubset := difference.subset_left at C, {h}
  have closedRest : ClosedUnder(leftEnd, rightEnd, C ∖ {h}, S)
    intros g inRest
    exact closed with g, (restSubset with g, inRest)
  exact Joined.inside with closedRest, inside.left, joinedC

-- Replacing an edge h of F by an edge g keeps a vertex set S connected from
-- within when the ends of h, if both in S, stay joined inside S without h.
theorem Connects.inside_replace (V S leftEnd rightEnd F g h : Set)
  requires ends : ∀ x ∈ F ∪ {g}, leftEnd(x) ∈ V ∧ rightEnd(x) ∈ V
  requires edgeEnds : leftEnd(h) ∈ V ∧ rightEnd(h) ∈ V
  requires connected :
    Connects(S, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, S))
  requires bridged : leftEnd(h) ∈ S ∧ rightEnd(h) ∈ S →
    Joined(leftEnd, rightEnd, inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S),
      leftEnd(h), rightEnd(h))
  shows Connects(S, leftEnd, rightEnd,
    inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S))
proof
  have endsSwapped := ends_in.subset with ends,
    (difference.subset_left at F ∪ {g}, {h})
  have endsInside := ends_in.subset with endsSwapped,
    (inside.subset at leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S)
  by_cases hInside : leftEnd(h) ∈ S ∧ rightEnd(h) ∈ S
  . have cover : inside(leftEnd, rightEnd, F, S) ⊆
        inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S) ∪ {h}
      intros x inInside
      obtain ⟨inF, leftS, rightS⟩ := inInside
      by_cases same : x = h
      . rw same
        simp
      . have inSwapped : x ∈ (F ∪ {g}) ∖ {h} by simp [inF, same]
        have member : x ∈ inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S) :=
          ⟨inSwapped, leftS, rightS⟩
        simp [member]
    exact Connects.replace_edge with
      endsInside, edgeEnds, cover, (bridged with hInside), connected
  . have subset : inside(leftEnd, rightEnd, F, S) ⊆
        inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S)
      intros x inInside
      obtain ⟨inF, leftS, rightS⟩ := inInside
      have notH : x ≠ h
        intro same
        rw same at leftS, rightS
        exact hInside with ⟨leftS, rightS⟩
      refine ⟨?_, leftS, rightS⟩
      simp [inF, notH]
    exact Connects.monotone with subset, connected

-- Claim 1 of the proof: a class S of a stage up to m + 1 that a colour
-- connects from within stays connected from within after the exchange.
-- Colour c loses f, whose ends, when both in S, are joined inside S by the
-- rest of the even set closed by e, since f has the least level there;
-- the last colour loses e, whose ends, when both in S, are joined inside S
-- by the rest of its even set, every edge of which has level at least m.
theorem exchange.transfer (V E leftEnd rightEnd T e f S : Set, c k m n i : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires nonempty : V ≠ ∅
  requires decomposition : Decomposition(E, T, succ(k))
  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)
  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,
    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →
      m ≤ n
  requires cycle :
    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)
  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧
    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧
    (∀ g ∈ C, ∀ n ∈ ℕ,
      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
      (∃ p ∈ ℕ,
        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))
  requires colourC : c ∈ k
  requires first : e ∈ T(k)
  requires second : f ∈ T(c)
  requires bound : n ≤ succ(m)
  requires class : S ∈ partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)
  requires index : i ∈ succ(k)
  requires connected :
    Connects(S, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(i), S))
  shows Connects(S, leftEnd, rightEnd,
    inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(i), S))
proof
  have partition :
      Partition(V, partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)) :=
    partitionSequence.partition with graph, nonempty, decomposition
  have kIn : k ∈ succ(k) by simp
  have cIn : c ∈ succ(k) by simp [colourC]
  have endsK := Decomposition.ends with graph, decomposition, kIn
  have endsC := Decomposition.ends with graph, decomposition, cIn
  have endsE := endsK with e, first
  have endsF := endsC with f, second
  have mNatural : m ∈ ℕ := nat.omega.forward at m with *
  by_cases ic : i = c
  . rw [ic, (exchange.value_colour with decomposition, colourC, first, second)]
    rw ic at connected
    -- When the ends of f share S, n ≤ level(f), so every edge of the even
    -- set C closed by e keeps its ends in a class of stage n, and C ∖ {f}
    -- joins the ends of f inside S.
    have bridged : leftEnd(f) ∈ S ∧ rightEnd(f) ∈ S →
        Joined(leftEnd, rightEnd,
          inside(leftEnd, rightEnd, (T(c) ∪ {e}) ∖ {f}, S),
          leftEnd(f), rightEnd(f))
      intro fInside
      obtain ⟨C, subsetC, eInC, fInC, different, even, minimal⟩ := closes
      obtain ⟨p, pNatural, fLevel, _⟩ :=
        minimal with e, eInC, m, mNatural, level
      have pNat := nat.omega.backward with pNatural
      have nLe := FiniteLevel.le_of_together with
        graph, decomposition, fLevel, ⟨S, class, fInside⟩
      have endsCedges : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V :=
        ends_in.subset with (ends_in.union_edge with endsC, endsE), subsetC
      have togetherAll : ∀ g ∈ C,
          ∃ Y ∈ partitionSequence(V, leftEnd, rightEnd, T, succ(k), n),
            leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y
        intros g inC
        apply FiniteLevel.together_of_least with (endsCedges with g, inC)
        intros q qNatural gLevel
        obtain ⟨p₂, p₂Natural, fLevel₂, below⟩ :=
          minimal with g, inC, q, qNatural, gLevel
        have same :=
          FiniteLevel.unique with graph, decomposition, fLevel, fLevel₂
        have qNat := nat.omega.backward with qNatural
        rw ← same at below
        arith
      have joinedRest := EvenEdgeSet.joined_inside with finiteVertices,
        partition, class, endsCedges, even, fInC, fInside, togetherAll
      have restSubset : C ∖ {f} ⊆ (T(c) ∪ {e}) ∖ {f} :=
        difference.subset_of_subset with subsetC
      exact Joined.monotone with (inside.monotone with restSubset), joinedRest
    exact Connects.inside_replace with
      (ends_in.union_edge with endsC, endsE), endsF, connected, bridged
  by_cases ik : i = k
  . rw [ik, (exchange.value_last with decomposition, colourC, first, second)]
    rw ik at connected
    -- When the ends of e share S, n ≤ m, so every edge of the even set C₀
    -- of e keeps its ends in a class of stage n, and C₀ ∖ {e} joins the
    -- ends of e inside S.
    have bridged : leftEnd(e) ∈ S ∧ rightEnd(e) ∈ S →
        Joined(leftEnd, rightEnd,
          inside(leftEnd, rightEnd, (T(k) ∪ {f}) ∖ {e}, S),
          leftEnd(e), rightEnd(e))
      intro eInside
      obtain ⟨C₀, subsetC₀, eInC₀, even₀⟩ := cycle
      have nLe := FiniteLevel.le_of_together with
        graph, decomposition, level, ⟨S, class, eInside⟩
      have endsC₀ : ∀ g ∈ C₀, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V :=
        ends_in.subset with endsK, subsetC₀
      have togetherAll : ∀ g ∈ C₀,
          ∃ Y ∈ partitionSequence(V, leftEnd, rightEnd, T, succ(k), n),
            leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y
        intros g inC₀
        apply FiniteLevel.together_of_least with (endsC₀ with g, inC₀)
        intros q qNatural gLevel
        have mLe := least with g, (subsetC₀ with g, inC₀), q, qNatural,
          gLevel, ⟨C₀, subsetC₀, inC₀, even₀⟩
        have qNat := nat.omega.backward with qNatural
        arith
      have joinedRest := EvenEdgeSet.joined_inside with finiteVertices,
        partition, class, endsC₀, even₀, eInC₀, eInside, togetherAll
      have restSubset : C₀ ∖ {e} ⊆ (T(k) ∪ {f}) ∖ {e} :=
        difference.subset_of_subset with
          (Subset.transitive with subsetC₀, union2.subset_left)
      exact Joined.monotone with (inside.monotone with restSubset), joinedRest
    exact Connects.inside_replace with
      (ends_in.union_edge with endsK, endsF), endsE, connected, bridged
  rw (exchange.value_other with
    decomposition, colourC, first, second, index, ic, ik)
  exact connected

-- With equal partitions at a stage up to m + 1, the exchanged
-- decomposition chooses no smaller colour: a colour below the one chosen
-- for T is internally connected for T, hence for the exchange.
theorem exchange.colour_le (V E leftEnd rightEnd T e f : Set, c k m n : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires nonempty : V ≠ ∅
  requires decomposition : Decomposition(E, T, succ(k))
  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)
  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,
    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →
      m ≤ n
  requires cycle :
    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)
  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧
    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧
    (∀ g ∈ C, ∀ n ∈ ℕ,
      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
      (∃ p ∈ ℕ,
        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))
  requires colourC : c ∈ k
  requires first : e ∈ T(k)
  requires second : f ∈ T(c)
  requires bound : n ≤ succ(m)
  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =
    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      succ(k), n)
  shows stageColour(leftEnd, rightEnd, T,
      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≤
    stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
        succ(k), n), succ(k))
proof
  have naturalT := stageColour.natural at leftEnd, rightEnd, T,
    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)
  obtain ⟨b, colourB⟩ := exists_eq at stageColour(leftEnd, rightEnd,
    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,
      exchange(E, T, e, f, c, k), succ(k), n), succ(k))
  have naturalB := stageColour.natural at leftEnd, rightEnd,
    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,
      exchange(E, T, e, f, c, k), succ(k), n), succ(k)
  have memberB := stageColour.member at leftEnd, rightEnd,
    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,
      exchange(E, T, e, f, c, k), succ(k), n), succ(k)
  rw ← colourB at naturalB, memberB
  rw ← colourB
  by_contra above
  have less := Less.of_not_LessEqual with above
  simp at memberB
  rcases memberB with inColours | isEnd
  . -- b is disconnected for the exchange but, being below the chosen
    -- colour of T, connected for T, so connected for the exchange.
    obtain ⟨bIn, bDisconnected⟩ := inColours
    have internalT : InternallyConnected(leftEnd, rightEnd, T(b),
        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n))
      by_contra disconnected
      have inT : b ∈ disconnectedColour(leftEnd, rightEnd, T,
          partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ∪
          {succ(k)} by simp [bIn, disconnected]
      have below := stageColour.least with inT
      arith
    have internalU : InternallyConnected(leftEnd, rightEnd,
        exchange(E, T, e, f, c, k)(b),
        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n))
      intros S classS
      exact exchange.transfer with graph, finiteVertices, nonempty,
        decomposition, level, least, cycle, closes, colourC, first, second,
        bound, classS, bIn, (internalT with S, classS)
    rw ← same at bDisconnected
    exact bDisconnected with internalU
  . have endIn : succ(k) ∈ disconnectedColour(leftEnd, rightEnd, T,
        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ∪
        {succ(k)} by simp
    have below := stageColour.least with endIn
    rw isEnd at less
    arith

-- With equal partitions and chosen colours at a moving stage n, the next
-- partitions of T and of the exchange refine P_n along T(c_n) and along
-- exchange(c_n).
theorem exchange.next_classes (V E leftEnd rightEnd T e f : Set, c k n : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires nonempty : V ≠ ∅
  requires decomposition : Decomposition(E, T, succ(k))
  requires colourC : c ∈ k
  requires first : e ∈ T(k)
  requires second : f ∈ T(c)
  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =
    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      succ(k), n)
  requires colours : stageColour(leftEnd, rightEnd, T,
      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) =
    stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
        succ(k), n), succ(k))
  requires active : disconnectedColour(leftEnd, rightEnd, T,
    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≠ ∅
  shows partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(n)) =
      refineBy(leftEnd, rightEnd, T(leastNatural(disconnectedColour(leftEnd,
        rightEnd, T, partitionSequence(V, leftEnd, rightEnd, T, succ(k), n),
        succ(k)))), partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)) ∧
    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
        succ(k), succ(n)) =
      refineBy(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(leastNatural(
        disconnectedColour(leftEnd, rightEnd, T,
          partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)))),
        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n))
proof
  have partition :
      Partition(V, partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)) :=
    partitionSequence.partition with graph, nonempty, decomposition
  obtain ⟨colourIn, _⟩ := disconnectedColour.least with active
  have ends := Decomposition.ends with graph, decomposition, colourIn
  have decompositionU := exchange.decomposition
    at V, E, leftEnd, rightEnd, T, e, f, c, k
    with decomposition, colourC, first, second
  have endsU := Decomposition.ends with graph, decompositionU, colourIn
  have stageT := stageColour.of_some with active
  rw [stageT, ← same] at colours
  have activeU : disconnectedColour(leftEnd, rightEnd,
      exchange(E, T, e, f, c, k),
      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≠ ∅
    intro none
    rw (stageColour.of_none with none) at colours
    rw colours at colourIn
    exact membership.irreflexive with colourIn
  have stageU := stageColour.of_some with activeU
  rw stageU at colours
  rw under colours at endsU
  constructor
  . rw [partitionSequence.succ,
      (partitionStep.refined with partition, ends, active)]
  . rw [partitionSequence.succ, ← same,
      (partitionStep.refined with partition, endsU, activeU), ← colours]

-- Claim 2, the partition half: under agreement at a moving stage n ≤ m the
-- next partition of T refines that of the exchange, as each class of the
-- former, connected from within by T(c_n), is connected from within by
-- exchange(c_n) and so lies in a class of the latter.
theorem exchange.refines_next (V E leftEnd rightEnd T e f : Set, c k m n : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires nonempty : V ≠ ∅
  requires decomposition : Decomposition(E, T, succ(k))
  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)
  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,
    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →
      m ≤ n
  requires cycle :
    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)
  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧
    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧
    (∀ g ∈ C, ∀ n ∈ ℕ,
      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
      (∃ p ∈ ℕ,
        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))
  requires colourC : c ∈ k
  requires first : e ∈ T(k)
  requires second : f ∈ T(c)
  requires bound : n ≤ m
  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =
    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      succ(k), n)
  requires colours : stageColour(leftEnd, rightEnd, T,
      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) =
    stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
        succ(k), n), succ(k))
  requires active : disconnectedColour(leftEnd, rightEnd, T,
    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≠ ∅
  shows Refines(partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(n)),
    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      succ(k), succ(n)))
proof
  obtain ⟨nextT, nextU⟩ := exchange.next_classes with graph, nonempty,
    decomposition, colourC, first, second, same, colours, active
  obtain ⟨colourIn, _⟩ := disconnectedColour.least with active
  obtain ⟨d, colourD⟩ := exists_eq at leastNatural(disconnectedColour(
    leftEnd, rightEnd, T,
    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)))
  rw ← colourD at nextT, nextU, colourIn
  have dNat := natural.member at succ(k) with d, colourIn
  have boundSucc : succ(n) ≤ succ(m) by arith
  intros S classS
  have classNext := classS
  rw nextT at classS
  obtain ⟨X, classX, inComponents⟩ :=
    refineBy.membership.forward with classS
  obtain ⟨u, uIn, rfl⟩ := inComponents
  have endsX := inside.ends at leftEnd, rightEnd, T(d), X
  have connectedS := componentBy.connects_inside with endsX, uIn
  have connectedT := Connects.monotone with
    (inside.monotone with (inside.subset at leftEnd, rightEnd, T(d), X)),
    connectedS
  have connectedU := exchange.transfer with graph, finiteVertices, nonempty,
    decomposition, level, least, cycle, closes, colourC, first, second,
    boundSucc, classNext, colourIn, connectedT
  have selfU := componentBy.self
    at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(d), X), u with uIn
  have subsetX := componentBy.subset
    at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(d), X), u
  have grow : inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(d),
      componentBy(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(d), X), u))
      ⊆ inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(d), X)
    intros g inInside
    obtain ⟨inU, leftS, rightS⟩ := inInside
    exact ⟨inU, (subsetX with leftEnd(g), leftS),
      (subsetX with rightEnd(g), rightS)⟩
  witness componentBy(X, leftEnd, rightEnd,
    inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(d), X), u)
  rw nextU
  refine ⟨?_, ?_⟩
  . exact refineBy.membership.backward with
      ⟨X, classX, (componentsBy.contains with uIn)⟩
  . intros v hv
    have joined := connectedU with u, selfU, v, hv
    exact ⟨(subsetX with v, hv), (Joined.monotone with grow, joined)⟩

-- At a stage n ≤ m + 1 where the partitions agree, and the earlier stages
-- agree, the exchange chooses no smaller colour: either it chooses a larger
-- one, and T precedes it at stage n, or the agreement reaches stage n.
theorem exchange.agree_step (V E leftEnd rightEnd T e f : Set, c k m n : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires nonempty : V ≠ ∅
  requires decomposition : Decomposition(E, T, succ(k))
  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)
  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,
    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →
      m ≤ n
  requires cycle :
    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)
  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧
    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧
    (∀ g ∈ C, ∀ n ∈ ℕ,
      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
      (∃ p ∈ ℕ,
        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))
  requires colourC : c ∈ k
  requires first : e ∈ T(k)
  requires second : f ∈ T(c)
  requires bound : n ≤ succ(m)
  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =
    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
      succ(k), n)
  requires agree : ∀ i ∈ n,
      partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =
        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
          succ(k), i) ∧
      stageColour(leftEnd, rightEnd, T,
          partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =
        stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),
          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
            succ(k), i), succ(k))
  shows Precedes(V, leftEnd, rightEnd, T, exchange(E, T, e, f, c, k),
      succ(k)) ∨
    (∀ i ∈ succ(n),
      partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =
        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
          succ(k), i) ∧
      stageColour(leftEnd, rightEnd, T,
          partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =
        stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),
          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
            succ(k), i), succ(k)))
proof
  have below := exchange.colour_le with graph, finiteVertices, nonempty,
    decomposition, level, least, cycle, closes, colourC, first, second,
    bound, same
  have naturalT := stageColour.natural at leftEnd, rightEnd, T,
    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)
  have naturalU := stageColour.natural at leftEnd, rightEnd,
    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,
      exchange(E, T, e, f, c, k), succ(k), n), succ(k)
  have natural : n ∈ ℕ := nat.omega.forward at n with *
  have order := LessEqual.cases with below
  rcases order with less | equal
  . left
    refine ⟨n, natural, agree, ?_⟩
    right
    exact ⟨same, less⟩
  . right
    intros i member
    have cases := membership.successor_forward{n := n} with member
    rcases cases with earlier | isN
    . exact agree with i, earlier
    . rw isN
      exact ⟨same, equal⟩

-- Claim 2: up to stage m, either the exchange already precedes T at some
-- stage, or the partitions and chosen colours agree at every stage so far.
theorem exchange.good_below (V E leftEnd rightEnd T e f : Set, c k m n : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires nonempty : V ≠ ∅
  requires decomposition : Decomposition(E, T, succ(k))
  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)
  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,
    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →
      m ≤ n
  requires cycle :
    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)
  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧
    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧
    (∀ g ∈ C, ∀ n ∈ ℕ,
      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
      (∃ p ∈ ℕ,
        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))
  requires colourC : c ∈ k
  requires first : e ∈ T(k)
  requires second : f ∈ T(c)
  requires some : disconnectedColour(leftEnd, rightEnd, T,
    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)) ≠ ∅
  requires bound : n ≤ m
  shows Precedes(V, leftEnd, rightEnd, T, exchange(E, T, e, f, c, k),
      succ(k)) ∨
    (∀ i ∈ succ(n),
      partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =
        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
          succ(k), i) ∧
      stageColour(leftEnd, rightEnd, T,
          partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =
        stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),
          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
            succ(k), i), succ(k)))
proof
  induction n
  | zero =>
    intro bound
    have zeroT := partitionSequence.zero at V, leftEnd, rightEnd, T, succ(k)
    have zeroU := partitionSequence.zero
      at V, leftEnd, rightEnd, exchange(E, T, e, f, c, k), succ(k)
    have sameZero : partitionSequence(V, leftEnd, rightEnd, T, succ(k), 0) =
        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
          succ(k), 0)
      rw [zeroT, zeroU]
    have start : 0 ≤ succ(m) by arith
    have none : ∀ i ∈ 0,
        partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =
          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
            succ(k), i) ∧
        stageColour(leftEnd, rightEnd, T,
            partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =
          stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),
            partitionSequence(V, leftEnd, rightEnd,
              exchange(E, T, e, f, c, k), succ(k), i), succ(k))
      intros i member
      exfalso
      rw nat.zero at member
      exact set.empty with member
    exact exchange.agree_step with graph, finiteVertices, nonempty,
      decomposition, level, least, cycle, closes, colourC, first, second,
      start, sameZero, none
  | succ(q) using ih =>
    intro bound
    have earlier : q ≤ m by arith
    have result := ih with earlier
    rcases result with precedes | good
    . left
      exact precedes
    . have self : q ∈ succ(q) by simp
      obtain ⟨sameN, coloursN⟩ := good with q, self
      -- The sequence of T is still moving at stage q, as it moves at m.
      have active : disconnectedColour(leftEnd, rightEnd, T,
          partitionSequence(V, leftEnd, rightEnd, T, succ(k), q),
          succ(k)) ≠ ∅
        obtain ⟨d, dNat, sum⟩ := earlier
        rw ← sum at some
        exact partitionSequence.active with
          graph, nonempty, decomposition, some
      have refines := exchange.refines_next with graph, finiteVertices,
        nonempty, decomposition, level, least, cycle, closes, colourC, first,
        second, earlier, sameN, coloursN, active
      by_cases equal :
        partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(q)) =
          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
            succ(k), succ(q))
      . have boundSucc : succ(q) ≤ succ(m) by arith
        exact exchange.agree_step with graph, finiteVertices,
          nonempty, decomposition, level, least, cycle, closes, colourC,
          first, second, boundSucc, equal, good
      . left
        have natural : succ(q) ∈ ℕ := nat.omega.forward at succ(q) with *
        refine ⟨succ(q), natural, good, ?_⟩
        left
        exact ⟨refines, equal⟩

-- Claims 1 and 2 of the proof, as the exchange step improving the
-- decomposition in the order.
theorem exchange.precedes (V E leftEnd rightEnd T e f : Set, c k m : Nat)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires nonempty : V ≠ ∅
  requires decomposition : Decomposition(E, T, succ(k))
  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))
  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)
  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,
    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →
      m ≤ n
  requires cycle :
    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)
  requires colour : c = leastNatural(disconnectedColour(leftEnd, rightEnd, T,
    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)))
  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧
    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧
    (∀ g ∈ C, ∀ n ∈ ℕ,
      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →
      (∃ p ∈ ℕ,
        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))
  shows Precedes(V, leftEnd, rightEnd, T, exchange(E, T, e, f, c, k),
      succ(k)) ∧
    (∀ i ∈ k,
      SpanningTree(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k)(i)))
proof
  -- The setting: e is of the last colour, c is a colour below k, and f is
  -- of colour c, as e is not.
  obtain ⟨C₀, subsetC₀, eInC₀, _⟩ := cycle
  have first : e ∈ T(k) := subsetC₀ with e, eInC₀
  obtain ⟨colourC, outside, some⟩ := FiniteLevel.colour_below with
    graph, nonempty, decomposition, level, first, colour
  have colourIn : c ∈ succ(k) by simp [colourC]
  obtain ⟨C, subsetC, eInC, fInC, different, even, _⟩ := closes
  have second : f ∈ T(c)
    have inUnion := subsetC with f, fInC
    simp [different] at inUnion
    exact inUnion
  refine ⟨?_, ?_⟩
  . -- Claim 2 up to stage m; then at m + 1 the partition of T refines
    -- that of the exchange and differs from it, since e, now of colour c,
    -- keeps its ends together there while T parts them.
    have selfM : m ≤ m := LessEqual.reflexive at m
    have result := exchange.good_below with graph, finiteVertices, nonempty,
      decomposition, level, least, cycle, closes, colourC, first, second,
      some, selfM
    rcases result with precedes | good
    . exact precedes
    . have selfIn : m ∈ succ(m) by simp
      obtain ⟨sameM, coloursM⟩ := good with m, selfIn
      obtain ⟨_, nextU⟩ := exchange.next_classes with graph, nonempty,
        decomposition, colourC, first, second, sameM, coloursM, some
      rw ← colour at nextU
      have refines := exchange.refines_next with graph, finiteVertices,
        nonempty, decomposition, level, least, cycle, closes, colourC, first,
        second, selfM, sameM, coloursM, some
      have eInU : e ∈ exchange(E, T, e, f, c, k)(c)
        rw exchange.class_membership with
          decomposition, colourC, first, second, colourIn
        left
        exact ⟨rfl, rfl⟩
      have strict :
          partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(m)) ≠
            partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),
              succ(k), succ(m))
        intro equal
        obtain ⟨together, parted⟩ := level
        obtain ⟨X, classX, leftIn, rightIn⟩ := together
        have insideEdge : e ∈ inside(leftEnd, rightEnd,
            exchange(E, T, e, f, c, k)(c), X) := ⟨eInU, leftIn, rightIn⟩
        have joined := Joined.of_edge at leftEnd, rightEnd, _, _ with insideEdge
        apply parted
        rw under equal
        rw under nextU
        exact refineBy.together with classX, ⟨leftIn, rightIn⟩, joined
      have natural : succ(m) ∈ ℕ := nat.omega.forward at succ(m) with *
      refine ⟨succ(m), natural, good, ?_⟩
      left
      exact ⟨refines, strict⟩
  . -- The trees: colour c exchanges f for e along the even set it closes,
    -- and the other colours below k are unchanged.
    intros i index
    have iNat := natural.member at k with i, index
    have inSucc : i ∈ succ(k) by simp [index]
    have less := Less.of_membership at i, k with index
    have notK : i ≠ k by arith
    by_cases ic : i = c
    . rw [ic, (exchange.value_colour with
        decomposition, colourC, first, second)]
      have kIn : k ∈ succ(k) by simp
      have endsC := Decomposition.ends with graph, decomposition, colourIn
      have endsK := Decomposition.ends with graph, decomposition, kIn
      have exchanged := SpanningTree.exchange with finiteVertices,
        ⟨endsC, (endsK with e, first)⟩, (trees with c, colourC), outside,
        even, ⟨subsetC, eInC⟩, ⟨fInC, different⟩
      have same : (T(c) ∪ {e}) ∖ {f} = (T(c) ∖ {f}) ∪ {e}
        ext g
        simp [different]
      rw same
      exact exchanged
    . rw (exchange.value_other with
        decomposition, colourC, first, second, inSucc, ic, notK)
      exact trees with i, index