Grace/Cumulus/GraphTheory/TreePacking/Kaiser.g17

Open in Workbench Download source

Imports

ExchangeOrder

Declarations

Source

1-- The tree-packing theorem of Tutte and Nash-Williams by Kaiser's argument:2-- under the packing condition, a maximal decomposition into k trees and a3-- rest has a connected rest, since an edge of least level in an even set of4-- the rest would admit an improving exchange, and k + 1 disjoint spanning5-- trees follow by induction.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.GraphTheory.TreePacking.Kaiser12import ExchangeOrder1314-- A connected finite edge set holds a spanning tree: a maximal forest15-- inside it joins whatever it joins.16theorem SpanningTree.within (V leftEnd rightEnd F : Set)17  requires finiteVertices : Finite(V)18  requires nonempty : V ≠ ∅19  requires finite : Finite(F)20  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V21  requires connected : Connects(V, leftEnd, rightEnd, F)22  shows ∃ G ⊆ F, SpanningTree(V, leftEnd, rightEnd, G)23proof24  have finiteFamily := forestsIn.finite at V, leftEnd, rightEnd, F with finite25  have emptyForest := forestsIn.contains_empty at V, leftEnd, rightEnd, F26  obtain ⟨G, inFamily, _, maximal⟩ :=27    Finite.maximal_extension with finiteFamily, emptyForest28  obtain ⟨inPowerset, forest⟩ := inFamily29  have subsetF := powerset.membership_iff.forward with inPowerset30  have endsG := ends_in.subset with ends, subsetF31  have connectedG : Connects(V, leftEnd, rightEnd, G)32    intros u hu v hv33    exact Forest.maximal_joined with finiteVertices, ends, inFamily, maximal,34      hu, (connected with u, hu, v, hv)35  refine ⟨G, subsetF, ?_⟩36  exact SpanningTree.of_connected_forest with37    finiteVertices, nonempty, endsG, forest, connectedG3839-- The function on succ(k) agreeing with T below k and taking G at k: it40-- adjoins the edges in no tree as a last colour, and later replaces the41-- last colour by a spanning tree inside it.42def replaceLast (E T G : Set, k : Nat) : Set :=43  { p ∈ succ(k) × 𝒫(E) | ∃ i ∈ succ(k),44    (i ∈ k ∧ p = (i, T(i))) ∨ (i = k ∧ p = (i, G)) }4546theorem replaceLast.shape (E T G x y : Set, k : Nat)47  requires member : (x, y) ∈ replaceLast(E, T, G, k)48  shows (x ∈ k ∧ y = T(x)) ∨ (x = k ∧ y = G)49proof50  obtain ⟨_, i, _, cases⟩ := member51  rcases cases with ⟨below, shape⟩ | ⟨same, shape⟩52  . obtain ⟨xi, yT⟩ := orderedPair.injective with shape53    left54    rw xi55    exact ⟨below, yT⟩56  . obtain ⟨xi, yG⟩ := orderedPair.injective with shape57    right58    rw xi59    exact ⟨same, yG⟩6061theorem replaceLast.function (E T G : Set, k : Nat)62  requires classes : ∀ i ∈ k, T(i) ∈ 𝒫(E)63  requires last : G ∈ 𝒫(E)64  shows replaceLast(E, T, G, k) : succ(k) → 𝒫(E)65proof66  have notSelf := membership.irreflexive at k67  constructor68  . intros p member69    exact member.left70  constructor71  . intros x y relatedY z relatedZ72    have shapeY := replaceLast.shape with relatedY73    have shapeZ := replaceLast.shape with relatedZ74    rcases shapeY with ⟨xBelow, yT⟩ | ⟨xLast, yG⟩75    . rcases shapeZ with ⟨_, zT⟩ | ⟨zLast, _⟩76      . cc77      . exfalso78        rw zLast at xBelow79        exact notSelf with xBelow80    . rcases shapeZ with ⟨zBelow, _⟩ | ⟨_, zG⟩81      . exfalso82        rw xLast at zBelow83        exact notSelf with zBelow84      . cc85  . intros x input86    have cases := membership.successor_forward{n := k} with input87    rcases cases with below | same88    . have class := classes with x, below89      refine ⟨T(x), class, ?_⟩90      unfold relates91      refine ⟨(product.pair with input, class), x, input, ?_⟩92      left93      exact ⟨below, rfl⟩94    . refine ⟨G, last, ?_⟩95      unfold relates96      refine ⟨(product.pair with input, last), x, input, ?_⟩97      right98      exact ⟨same, rfl⟩99100theorem replaceLast.value_below (E T G : Set, k i : Nat)101  requires classes : ∀ i ∈ k, T(i) ∈ 𝒫(E)102  requires last : G ∈ 𝒫(E)103  requires index : i ∈ k104  shows replaceLast(E, T, G, k)(i) = T(i)105proof106  have inSucc : i ∈ succ(k) by simp [index]107  have class := classes with i, index108  have related : relates(replaceLast(E, T, G, k), i, T(i))109    unfold relates110    refine ⟨(product.pair with inSucc, class), i, inSucc, ?_⟩111    left112    exact ⟨index, rfl⟩113  exact FunctionBetween.apply_value with114    (replaceLast.function with classes, last), inSucc, related115116theorem replaceLast.value_last (E T G : Set, k : Nat)117  requires classes : ∀ i ∈ k, T(i) ∈ 𝒫(E)118  requires last : G ∈ 𝒫(E)119  shows replaceLast(E, T, G, k)(k) = G120proof121  have kIn : k ∈ succ(k) by simp122  have related : relates(replaceLast(E, T, G, k), k, G)123    unfold relates124    refine ⟨(product.pair with kIn, last), k, kIn, ?_⟩125    right126    exact ⟨rfl, rfl⟩127  exact FunctionBetween.apply_value with128    (replaceLast.function with classes, last), kIn, related129130-- The packing condition for succ(k) colours gives it for k.131theorem PackingCondition.below (V E leftEnd rightEnd : Set, k : Nat)132  requires finiteVertices : Finite(V)133  requires finiteEdges : Finite(E)134  requires condition : PackingCondition(V, E, leftEnd, rightEnd, succ(k))135  shows PackingCondition(V, E, leftEnd, rightEnd, k)136proof137  intros P partition138  have packed := condition with P, partition139  have finiteClasses := Partition.finite with finiteVertices, partition140  have finiteCrossing : Finite(crossingClasses(P, leftEnd, rightEnd, E)) :=141    Finite.subset with finiteEdges,142      (crossingClasses.subset at P, leftEnd, rightEnd, E)143  have step := mul.succ_left at k, cardinality(P) - 1144  rw step at packed145  arith146147-- A packing of k trees extends to a decomposition into succ(k) colours,148-- the edges in no tree forming the last colour.149theorem TreePacking.decomposition (V E leftEnd rightEnd T : Set, k : Nat)150  requires function : FunctionBetween(T, k, 𝒫(E))151  requires apart : ∀ i ∈ k, ∀ j ∈ k, i ≠ j → Disjoint(T(i), T(j))152  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))153  shows Decomposition(E, replaceLast(E, T, E ∖ coloursBelow(T, k), k),154      succ(k)) ∧155    (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd,156      replaceLast(E, T, E ∖ coloursBelow(T, k), k)(i)))157proof158  have last : E ∖ coloursBelow(T, k) ∈ 𝒫(E) :=159    powerset.membership_iff.backward with difference.subset_left160  have classes : ∀ i ∈ k, T(i) ∈ 𝒫(E)161    intros i index162    exact FunctionBetween.apply_closed with function, index163  constructor164  . refine ⟨(replaceLast.function with classes, last), ?_, ?_⟩165    . -- Every edge has a colour: its tree, or the last colour.166      intros g inE167      by_cases inBelow : g ∈ coloursBelow(T, k)168      . obtain ⟨i, index, inT⟩ := coloursBelow.colour with inBelow169        have iNat := natural.member at k with i, index170        have inSucc : i ∈ succ(k) by simp [index]171        refine ⟨i, inSucc, ?_⟩172        rw replaceLast.value_below with classes, last, index173        exact inT174      . have kIn : k ∈ succ(k) by simp175        refine ⟨k, kIn, ?_⟩176        rw replaceLast.value_last with classes, last177        simp [inE, inBelow]178    . -- The trees are disjoint, and the last colour misses them all.179      intros i indexI j indexJ different180      have iNat := natural.member at succ(k) with i, indexI181      have jNat := natural.member at succ(k) with j, indexJ182      have casesI := membership.successor_forward{n := k} with indexI183      have casesJ := membership.successor_forward{n := k} with indexJ184      rcases casesI with belowI | lastI185      . rw replaceLast.value_below with classes, last, belowI186        rcases casesJ with belowJ | lastJ187        . rw replaceLast.value_below with classes, last, belowJ188          exact apart with i, belowI, j, belowJ, different189        . rw [lastJ, (replaceLast.value_last with classes, last)]190          apply Disjoint.iff.backward191          intros g inT inRest192          have inBelow := coloursBelow.contains with belowI, inT193          exact (difference.membership.forward with inRest).right with inBelow194      . rw [lastI, (replaceLast.value_last with classes, last)]195        rcases casesJ with belowJ | lastJ196        . rw replaceLast.value_below with classes, last, belowJ197          apply Disjoint.iff.backward198          intros g inRest inT199          have inBelow := coloursBelow.contains with belowJ, inT200          exact (difference.membership.forward with inRest).right with inBelow201        . exfalso202          rw [lastI, lastJ] at different203          exact different with rfl204  . intros i index205    have iNat := natural.member at k with i, index206    rw replaceLast.value_below with classes, last, index207    exact trees with i, index208209-- The even set closed by e in the colour c refined at the level m of e has210-- an edge other than e of level below m: otherwise every edge of the set211-- would keep its ends within the class X of e at stage m, so the set would212-- join the ends of e inside X by edges of T(c), against the level of e.213theorem fundamental.lower_level (V E leftEnd rightEnd T e C : Set, c k m : Nat)214  requires graph : Graph(V, E, leftEnd, rightEnd)215  requires finiteVertices : Finite(V)216  requires nonempty : V ≠ ∅217  requires decomposition : Decomposition(E, T, succ(k))218  requires edge : e ∈ E219  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)220  requires colour : c = leastNatural(disconnectedColour(leftEnd, rightEnd, T,221    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)))222  requires closes :223    C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)224  shows ∃ g ∈ C, g ≠ e ∧225    (∃ n ∈ ℕ, n < m ∧226      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n))227proof228  obtain ⟨subsetC, eInC, even⟩ := closes229  obtain ⟨together, parted⟩ := level230  obtain ⟨X, class, leftIn, rightIn⟩ := together231  have partition : Partition(V,232      partitionSequence(V, leftEnd, rightEnd, T, succ(k), m)) :=233    partitionSequence.partition with graph, nonempty, decomposition234  obtain ⟨some, _⟩ := FiniteLevel.refining_colour with235    graph, nonempty, decomposition, level236  obtain ⟨colourIn, _⟩ := disconnectedColour.least with some237  rw ← colour at colourIn238  have ends := Decomposition.ends with graph, decomposition, colourIn239  have endsC : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V240    intros g inC241    have inUnion := subsetC with g, inC242    simp at inUnion243    rcases inUnion with inT | same244    . exact ends with g, inT245    . rw same246      exact Graph.ends with graph, e, edge247  by_contra none248  -- Every edge of C keeps its ends together at stage m, so X is closed.249  have togetherAll : ∀ g ∈ C,250      ∃ Y ∈ partitionSequence(V, leftEnd, rightEnd, T, succ(k), m),251        leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y252    intros g inC253    by_contra apart254    have start := partitionSequence.together_zero255      at V, leftEnd, rightEnd, T, g, succ(k) with (endsC with g, inC)256    obtain ⟨n, natural, less, levelG⟩ :=257      FiniteLevel.of_parted with start, apart258    have notE : g ≠ e259      intro same260      rw under same at apart261      exact apart with ⟨X, class, leftIn, rightIn⟩262    exact none with ⟨g, inC, notE, n, natural, less, levelG⟩263  -- So C ∖ {e} joins the ends of e inside X by edges of T(c), and they264  -- share a component of T(c) within X, a class of stage m + 1.265  have joinedInside := EvenEdgeSet.joined_inside with finiteVertices,266    partition, class, endsC, even, eInC, ⟨leftIn, rightIn⟩, togetherAll267  have restSubset : inside(leftEnd, rightEnd, C ∖ {e}, X) ⊆268      inside(leftEnd, rightEnd, T(c), X)269    intros g inInside270    obtain ⟨inRest, leftG, rightG⟩ := inInside271    obtain ⟨inC, notE⟩ :=272      difference.singleton_membership.forward with inRest273    have inUnion := subsetC with g, inC274    simp [notE] at inUnion275    exact ⟨inUnion, leftG, rightG⟩276  have joined := Joined.monotone with restSubset, joinedInside277  rw under colour at ends278  apply parted279  rw under partitionSequence.succ280  rw under partitionStep.refined with partition, ends, some281  rw under ← colour282  exact refineBy.together with class, ⟨leftIn, rightIn⟩, joined283284-- The finite levels of the edges of the last colour lying in its even285-- sets, and the finite levels of the edges other than e of an even set.286def cycleLevels (V leftEnd rightEnd T : Set, k : Nat) : Set :=287  { n ∈ ℕ | ∃ g ∈ T(k),288    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) ∧289    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) }290291def closedLevels (V leftEnd rightEnd T C e : Set, k : Nat) : Set :=292  { n ∈ ℕ | ∃ g ∈ C, g ≠ e ∧293    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) }294295-- No edge of the last colour in an even set of it has a least finite296-- level under a maximal decomposition: the colour refined at that level297-- closes an even set through it, whose edge f of least level is below, and298-- exchanging the two edges gives a decomposition preceding the maximal one.299theorem Kaiser.no_least_edge (V E leftEnd rightEnd T e : Set, c k m : Nat)300  requires graph : Graph(V, E, leftEnd, rightEnd)301  requires finiteVertices : Finite(V)302  requires finiteEdges : Finite(E)303  requires nonempty : V ≠ ∅304  requires decomposition : Decomposition(E, T, succ(k))305  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))306  requires maximal : ¬(∃ U, Decomposition(E, U, succ(k)) ∧307    (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, U(i))) ∧308    Precedes(V, leftEnd, rightEnd, T, U, succ(k)))309  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)310  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,311    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →312    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →313      m ≤ n314  requires cycle :315    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)316  requires colour : c = leastNatural(disconnectedColour(leftEnd, rightEnd, T,317    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)))318  shows ⊥319proof320  -- c is a colour below k not holding e, so e closes an even set in T(c).321  obtain ⟨C₀, subsetC₀, eInC₀, _⟩ := cycle322  have first : e ∈ T(k) := subsetC₀ with e, eInC₀323  obtain ⟨colourC, outside, _⟩ := FiniteLevel.colour_below with324    graph, nonempty, decomposition, level, first, colour325  have colourIn : c ∈ succ(k) by simp [colourC]326  have kIn : k ∈ succ(k) by simp327  have endsC := Decomposition.ends with graph, decomposition, colourIn328  have endsK := Decomposition.ends with graph, decomposition, kIn329  have classK := Decomposition.class_subset with decomposition, kIn330  have edge : e ∈ E := classK with e, first331  obtain ⟨C, subsetC, eInC, even⟩ := SpanningTree.fundamental with332    finiteVertices, ⟨endsC, (endsK with e, first)⟩, (trees with c, colourC),333    outside334  -- Its edges other than e have finite levels, one of them below m; f is335  -- an edge of least such level.336  obtain ⟨g, gInC, gNotE, n, nNatural, nLess, gLevel⟩ :=337    fundamental.lower_level with graph, finiteVertices, nonempty,338      decomposition, edge, level, colour, ⟨subsetC, eInC, even⟩339  have subsetLevels : closedLevels(V, leftEnd, rightEnd, T, C, e, k) ⊆ ℕ340    intros p member341    exact member.left342  have inLevels : n ∈ closedLevels(V, leftEnd, rightEnd, T, C, e, k) :=343    ⟨nNatural, g, gInC, gNotE, gLevel⟩344  have inhabited : Nonempty(closedLevels(V, leftEnd, rightEnd, T, C, e, k)) :=345    ⟨n, inLevels⟩346  obtain ⟨pNatural, f, fInC, fNotE, fLevel⟩ :=347    leastNatural.member with inhabited, subsetLevels348  have pLeast := leastNatural.least with inhabited, subsetLevels, inLevels349  have pNat := nat.omega.backward with pNatural350  have nNat := nat.omega.backward with nNatural351  have closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧352      f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧353      (∀ g ∈ C, ∀ n ∈ ℕ,354        FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →355        (∃ p ∈ ℕ,356          FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))357    refine ⟨C, subsetC, eInC, fInC, fNotE, even, ?_⟩358    intros h hInC q qNatural hLevel359    refine ⟨leastNatural(closedLevels(V, leftEnd, rightEnd, T, C, e, k)),360      pNatural, fLevel, ?_⟩361    by_cases same : h = e362    . -- The level of e is m, above the level of g and so of f.363      rw same at hLevel364      have unique := FiniteLevel.unique with graph, decomposition, level, hLevel365      rw ← unique366      arith367    . exact leastNatural.least with inhabited, subsetLevels,368        ⟨qNatural, h, hInC, same, hLevel⟩369  obtain ⟨precedes, treesU⟩ := exchange.precedes with graph, finiteVertices,370    finiteEdges, nonempty, decomposition, trees, level, least, cycle, colour,371    closes372  have second : f ∈ T(c)373    have inUnion := subsetC with f, fInC374    simp [fNotE] at inUnion375    exact inUnion376  have decompositionU := exchange.decomposition377    at V, E, leftEnd, rightEnd, T, e, f, c, k378    with decomposition, colourC, first, second379  exact maximal with380    ⟨exchange(E, T, e, f, c, k), decompositionU, treesU, precedes⟩381382-- The last colour of a maximal decomposition connects V: otherwise383-- Kaiser.cycle_edge gives edges of finite level in even sets of the last384-- colour, and one of least level is excluded by Kaiser.no_least_edge.385theorem Kaiser.last_connected (V E leftEnd rightEnd T : Set, k : Nat)386  requires graph : Graph(V, E, leftEnd, rightEnd)387  requires finiteVertices : Finite(V)388  requires finiteEdges : Finite(E)389  requires nonempty : V ≠ ∅390  requires decomposition : Decomposition(E, T, succ(k))391  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))392  requires condition : PackingCondition(V, E, leftEnd, rightEnd, succ(k))393  requires maximal : ¬(∃ U, Decomposition(E, U, succ(k)) ∧394    (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, U(i))) ∧395    Precedes(V, leftEnd, rightEnd, T, U, succ(k)))396  shows Connects(V, leftEnd, rightEnd, T(k))397proof398  by_contra disconnected399  obtain ⟨C₀, subsetC₀, even₀, e₀, inC₀, n₀, natural₀, level₀⟩ :=400    Kaiser.cycle_edge with graph, finiteVertices, finiteEdges, nonempty,401      decomposition, trees, condition, disconnected402  have subsetLevels : cycleLevels(V, leftEnd, rightEnd, T, k) ⊆ ℕ403    intros n member404    exact member.left405  have inLevels : n₀ ∈ cycleLevels(V, leftEnd, rightEnd, T, k) :=406    ⟨natural₀, e₀, (subsetC₀ with e₀, inC₀), level₀,407      C₀, subsetC₀, inC₀, even₀⟩408  have inhabited : Nonempty(cycleLevels(V, leftEnd, rightEnd, T, k)) :=409    ⟨n₀, inLevels⟩410  obtain ⟨mNatural, e, first, level, cycle⟩ :=411    leastNatural.member with inhabited, subsetLevels412  have mNat := nat.omega.backward with mNatural413  have least : ∀ g ∈ T(k), ∀ n ∈ ℕ,414      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →415      (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →416        leastNatural(cycleLevels(V, leftEnd, rightEnd, T, k)) ≤ n417    intros g inT n natural levelG cycleG418    exact leastNatural.least with inhabited, subsetLevels,419      ⟨natural, g, inT, levelG, cycleG⟩420  obtain ⟨c, colour⟩ := exists_eq at leastNatural(disconnectedColour(421    leftEnd, rightEnd, T, partitionSequence(V, leftEnd, rightEnd, T, succ(k),422      leastNatural(cycleLevels(V, leftEnd, rightEnd, T, k))), succ(k)))423  have cNat : Nat(c)424    rw colour425    exact leastNatural.natural with (disconnectedColour.subset at leftEnd,426      rightEnd, T, partitionSequence(V, leftEnd, rightEnd, T, succ(k),427        leastNatural(cycleLevels(V, leftEnd, rightEnd, T, k))), succ(k))428  exact Kaiser.no_least_edge with graph, finiteVertices, finiteEdges,429    nonempty, decomposition, trees, maximal, level, least, cycle, colour430431-- Tutte and Nash-Williams: the packing condition suffices. By induction432-- on k: the condition for succ(k) gives k trees, which extend to a433-- decomposition into succ(k) colours; a maximal one has a connected last434-- colour, which holds the last tree.435theorem treePacking (V E leftEnd rightEnd : Set, k : Nat)436  requires graph : Graph(V, E, leftEnd, rightEnd)437  requires finiteVertices : Finite(V)438  requires finiteEdges : Finite(E)439  requires nonempty : V ≠ ∅440  requires condition : PackingCondition(V, E, leftEnd, rightEnd, k)441  shows TreePacking(V, E, leftEnd, rightEnd, k)442proof443  induction k444  | zero =>445    intro _446    witness ∅447    refine ⟨?_, ?_, ?_⟩448    . constructor449      . exact empty.subset450      constructor451      . intros x y relatedY z relatedZ452        exfalso453        exact set.empty with relatedY454      . intros x input455        exfalso456        rw nat.zero at input457        exact set.empty with input458    . intros i index459      exfalso460      rw nat.zero at index461      exact set.empty with index462    . intros i index463      exfalso464      rw nat.zero at index465      exact set.empty with index466  | succ(n) using ih =>467    intro condition468    have below := PackingCondition.below with469      finiteVertices, finiteEdges, condition470    obtain ⟨T₀, function₀, apart₀, trees₀⟩ := ih with below471    obtain ⟨decomposition₀, trees₁⟩ :=472      TreePacking.decomposition with function₀, apart₀, trees₀473    have some : ∃ T, Decomposition(E, T, succ(n)) ∧474        (∀ i ∈ n, SpanningTree(V, leftEnd, rightEnd, T(i))) :=475      ⟨replaceLast(E, T₀, E ∖ coloursBelow(T₀, n), n),476        decomposition₀, trees₁⟩477    obtain ⟨T, decomposition, trees, maximal⟩ := Precedes.maximal with478      graph, finiteVertices, finiteEdges, nonempty, some479    have connected := Kaiser.last_connected with graph, finiteVertices,480      finiteEdges, nonempty, decomposition, trees, condition, maximal481    -- The last tree: a spanning tree inside the connected last colour.482    have kIn : n ∈ succ(n) by simp483    have classK := Decomposition.class_subset with decomposition, kIn484    have endsK := ends_in.subset with (Graph.ends with graph), classK485    have finiteK := Finite.subset with finiteEdges, classK486    obtain ⟨G, subsetG, tree⟩ := SpanningTree.within with487      finiteVertices, nonempty, finiteK, endsK, connected488    have classes : ∀ i ∈ n, T(i) ∈ 𝒫(E)489      intros i index490      have inSucc : i ∈ succ(n) by simp [index]491      exact FunctionBetween.apply_closed with decomposition.left, inSucc492    have last : G ∈ 𝒫(E) := powerset.membership_iff.backward with493      (Subset.transitive with subsetG, classK)494    witness replaceLast(E, T, G, n)495    refine ⟨(replaceLast.function with classes, last), ?_, ?_⟩496    . -- The colours stay disjoint, the last tree lying in the last colour.497      intros i indexI j indexJ different498      have iNat := natural.member at succ(n) with i, indexI499      have jNat := natural.member at succ(n) with j, indexJ500      have casesI := membership.successor_forward{n := n} with indexI501      have casesJ := membership.successor_forward{n := n} with indexJ502      rcases casesI with belowI | lastI503      . rw replaceLast.value_below with classes, last, belowI504        rcases casesJ with belowJ | lastJ505        . rw replaceLast.value_below with classes, last, belowJ506          exact decomposition.right.right with507            i, indexI, j, indexJ, different508        . rw [lastJ, (replaceLast.value_last with classes, last)]509          rw lastJ at different510          exact Disjoint.of_subset_right with511            (decomposition.right.right with i, indexI, n, kIn, different),512            subsetG513      . rw [lastI, (replaceLast.value_last with classes, last)]514        rcases casesJ with belowJ | lastJ515        . rw replaceLast.value_below with classes, last, belowJ516          rw lastI at different517          exact Disjoint.of_subset_left with518            (decomposition.right.right with n, kIn, j, indexJ, different),519            subsetG520        . exfalso521          rw [lastI, lastJ] at different522          exact different with rfl523    . intros i index524      have iNat := natural.member at succ(n) with i, index525      have cases := membership.successor_forward{n := n} with index526      rcases cases with below | same527      . rw replaceLast.value_below with classes, last, below528        exact trees with i, below529      . rw [same, (replaceLast.value_last with classes, last)]530        exact tree531