Grace/Cumulus/GraphTheory/TreePacking/Decompositions.g17

Open in Workbench Download source

Imports

Multigraph.Trees · Multigraph.Quotient · Multigraph.Subgraph

Declarations

Source

1-- Decompositions of the edge set into k colour classes, the tree-packing2-- condition of Tutte and Nash-Williams, and partitions of the vertex set as3-- they refine along a decomposition.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.GraphTheory.TreePacking.Decompositions10import Multigraph.Trees11import Multigraph.Quotient12import Multigraph.Subgraph1314-- Section: Decompositions, packings, and the packing condition.1516-- A k-decomposition: T assigns to every colour i ∈ k an edge class, and the17-- classes partition E.18predicate Decomposition (E T : Set, k : Nat) :=19  FunctionBetween(T, k, 𝒫(E)) ∧ (∀ e ∈ E, ∃ i ∈ k, e ∈ T(i)) ∧20  (∀ i ∈ k, ∀ j ∈ k, i ≠ j → Disjoint(T(i), T(j)))2122-- A tree packing: k pairwise edge-disjoint spanning trees inside E, one23-- for each colour i ∈ k; they need not exhaust E.24predicate TreePacking (V E leftEnd rightEnd : Set, k : Nat) :=25  ∃ T, FunctionBetween(T, k, 𝒫(E)) ∧26    (∀ i ∈ k, ∀ j ∈ k, i ≠ j → Disjoint(T(i), T(j))) ∧27    (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i)))2829-- Every partition P of V is joined by at least k(|P| − 1) edges.30predicate PackingCondition (V E leftEnd rightEnd : Set, k : Nat) :=31  ∀ P, Partition(V, P) →32    k * (cardinality(P) - 1) ≤33      cardinality(crossingClasses(P, leftEnd, rightEnd, E))3435-- F connects every class of P from within, by its edges inside the class.36predicate InternallyConnected (leftEnd rightEnd F P : Set) :=37  ∀ X ∈ P, Connects(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X))3839-- Section: Partitions and their crossing edges.4041theorem Partition.finite (V P : Set)42  requires finiteVertices : Finite(V)43  requires partition : Partition(V, P)44  shows Finite(P)45proof46  have subset : P ⊆ 𝒫(V)47    intros X class48    exact powerset.membership_iff.backward49      with (partition.left with X, class).left50  exact Finite.subset with (Finite.powerset with finiteVertices), subset5152-- A vertex lies in a class of a partition exactly when that class is its own.53theorem classOf.eq_iff_member (V P Y v : Set)54  requires partition : Partition(V, P)55  requires class : Y ∈ P56  requires vertex : v ∈ V57  shows classOf(P, v) = Y ↔ v ∈ Y58proof59  constructor60  . intro same61    rw ← same62    exact (classOf.member with partition, vertex).right63  . intro member64    exact classOf.eq_of_member with partition.right.left, class, member6566theorem crossingClasses.subset (P leftEnd rightEnd F : Set)67  shows crossingClasses(P, leftEnd, rightEnd, F) ⊆ F68proof69  intros e edge70  exact edge.left7172theorem crossingClasses.finite (P leftEnd rightEnd F : Set)73  requires finite : Finite(F)74  shows Finite(crossingClasses(P, leftEnd, rightEnd, F))75proof76  exact Finite.subset with finite, crossingClasses.subset7778theorem crossingClasses.monotone (P leftEnd rightEnd F G : Set)79  requires subset : F ⊆ G80  shows crossingClasses(P, leftEnd, rightEnd, F) ⊆81    crossingClasses(P, leftEnd, rightEnd, G)82proof83  intros e edge84  exact ⟨(subset with e, edge.left), edge.right⟩8586theorem crossingClasses.union (P leftEnd rightEnd F G : Set)87  shows crossingClasses(P, leftEnd, rightEnd, F ∪ G) =88    crossingClasses(P, leftEnd, rightEnd, F) ∪89      crossingClasses(P, leftEnd, rightEnd, G)90proof91  ext e92  simp [crossingClasses]9394-- Section: Refining a partition by the components inside its classes.9596-- Refining P by the components of F within each class.97def refinements (leftEnd rightEnd F P : Set) : Set :=98  { componentsBy(X, leftEnd, rightEnd,99      inside(leftEnd, rightEnd, F, X)) | X ∈ P }100def refineBy (leftEnd rightEnd F P : Set) : Set :=101  ⋃(refinements(leftEnd, rightEnd, F, P))102103-- A class of the refinement is a component of some class of P.104theorem refineBy.membership (leftEnd rightEnd F P Y : Set)105  shows Y ∈ refineBy(leftEnd, rightEnd, F, P) ↔106    ∃ X ∈ P,107      Y ∈ componentsBy(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X))108proof109  unfold refineBy110  rw union.membership111  constructor112  . intro inUnion113    obtain ⟨Z, inFamily, inZ⟩ := inUnion114    obtain ⟨X, class, rfl⟩ := inFamily115    exact ⟨X, class, inZ⟩116  . intro inComponents117    obtain ⟨X, class, member⟩ := inComponents118    witness componentsBy(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X))119    exact ⟨⟨X, class, rfl⟩, member⟩120121theorem refineBy.partition (V leftEnd rightEnd F P : Set)122  requires partition : Partition(V, P)123  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V124  shows Partition(V, refineBy(leftEnd, rightEnd, F, P))125proof126  obtain ⟨classes, apart, covers⟩ := partition127  constructor128  -- A component of a class is a nonempty subset of the class, so of V.129  . intros Y inRefined130    obtain ⟨X, class, inComponents⟩ :=131      refineBy.membership.forward with inRefined132    have componentPartition := componentsBy.partition133      at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X)134      with inside.ends135    obtain ⟨subsetX, nonempty⟩ :=136      componentPartition.left with Y, inComponents137    exact ⟨(Subset.transitive with subsetX, (classes with X, class).left),138      nonempty⟩139  constructor140  -- Two components of one class are disjoint as components; of different141  -- classes, as subsets of disjoint classes.142  . intros Y inY Z inZ different143    obtain ⟨X, classX, inComponentsX⟩ := refineBy.membership.forward with inY144    obtain ⟨W, classW, inComponentsW⟩ := refineBy.membership.forward with inZ145    by_cases same : X = W146    . rw ← same at inComponentsW147      have componentPartition := componentsBy.partition148        at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X)149        with inside.ends150      exact componentPartition.right.left151        with Y, inComponentsX, Z, inComponentsW, different152    . obtain ⟨u, _, rfl⟩ := inComponentsX153      obtain ⟨w, _, rfl⟩ := inComponentsW154      have apartXW := apart with X, classX, W, classW, same155      exact Disjoint.of_subset_right with156        (Disjoint.of_subset_left with apartXW, componentBy.subset),157        componentBy.subset158  -- Every vertex lies in its component within its class.159  . intros v inV160    obtain ⟨X, class, inX⟩ := covers with v, inV161    have contains := componentsBy.contains162      at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X), v with inX163    witness componentBy(X, leftEnd, rightEnd,164      inside(leftEnd, rightEnd, F, X), v)165    exact ⟨(refineBy.membership.backward with ⟨X, class, contains⟩),166      (componentBy.self with inX)⟩167168theorem refineBy.refines (leftEnd rightEnd F P : Set)169  shows Refines(refineBy(leftEnd, rightEnd, F, P), P)170proof171  intros Y inRefined172  obtain ⟨X, class, u, _, rfl⟩ := refineBy.membership.forward with inRefined173  exact ⟨X, class, componentBy.subset⟩174175-- The refinement is P itself exactly when F connects each class from within.176theorem refineBy.fixed_iff (V leftEnd rightEnd F P : Set)177  requires partition : Partition(V, P)178  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V179  shows refineBy(leftEnd, rightEnd, F, P) = P ↔180    InternallyConnected(leftEnd, rightEnd, F, P)181proof182  obtain ⟨classes, apart, covers⟩ := partition183  constructor184  -- Fixed: the component of u within its class X is a class of P meeting X185  -- at u, so it is X, and every vertex of X is joined to u.186  . intros fixed X class u inX v inV187    have contains := componentsBy.contains188      at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X), u with inX189    have inRefined := refineBy.membership.backward with ⟨X, class, contains⟩190    rw fixed at inRefined191    have whole :192        componentBy(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X), u)193          = X194      by_contra different195      have apartComponent := apart with196        componentBy(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X), u),197        inRefined, X, class, different198      have self := componentBy.self199        at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X), u with inX200      have apartAll := Disjoint.iff.forward with apartComponent201      exact apartAll with u, self, inX202    rw ← whole at inV203    exact inV.right204  -- Connected: the components of a connected class are the class alone.205  . intro internal206    ext Y207    rw refineBy.membership208    constructor209    . intro inRefined210      obtain ⟨X, class, inComponents⟩ := inRefined211      have single := componentsBy.connected_subset with (internal with X, class)212      have same := singleton.membership.forward213        with (single with Y, inComponents)214      rw same215      exact class216    . intro class217      obtain ⟨u, inY⟩ :=218        Nonempty.of_ne_empty with (classes with Y, class).right219      have whole := componentBy.eq_vertices with (internal with Y, class), inY220      have contains := componentsBy.contains221        at Y, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, Y), u with inY222      rw whole at contains223      exact ⟨Y, class, contains⟩224225-- Section: Connectivity passes to the quotient by a partition.226227-- Joined vertices have joined classes in the quotient: the union of a set of228-- classes closed under the quotient edges of F is closed under F.229theorem Joined.quotient (V E P leftEnd rightEnd F u v : Set)230  requires graph : Graph(V, E, leftEnd, rightEnd)231  requires partition : Partition(V, P)232  requires edges : F ⊆ E233  requires first : u ∈ V234  requires second : v ∈ V235  requires joined : Joined(leftEnd, rightEnd, F, u, v)236  shows Joined(quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd), F,237    classOf(P, u), classOf(P, v))238proof239  intros A start closed240  have classes : A ∩ P ⊆ P := intersection.subset_right241  have closedUnion : ClosedUnder(leftEnd, rightEnd, F, ⋃(A ∩ P))242    intros e inF243    have inE := edges with e, inF244    obtain ⟨leftValue, rightValue⟩ :=245      quotientEnd.value with graph, partition, inE246    obtain ⟨leftIn, rightIn⟩ := Graph.ends with graph, e, inE247    have leftClass := (classOf.member with partition, leftIn).left248    have rightClass := (classOf.member with partition, rightIn).left249    have balanced := closed with e, inF250    rw [leftValue, rightValue] at balanced251    rw [(classOf.mem_union_iff with partition, classes, leftIn),252      (classOf.mem_union_iff with partition, classes, rightIn)]253    simp [balanced, leftClass, rightClass]254  have startUnion : u ∈ ⋃(A ∩ P)255    have class := (classOf.member with partition, first).left256    rw classOf.mem_union_iff with partition, classes, first257    simp [start, class]258  have reached := joined with ⋃(A ∩ P), startUnion, closedUnion259  rw classOf.mem_union_iff with partition, classes, second at reached260  exact reached.left261262theorem Connects.quotient (V E P leftEnd rightEnd F : Set)263  requires graph : Graph(V, E, leftEnd, rightEnd)264  requires partition : Partition(V, P)265  requires edges : F ⊆ E266  requires connected : Connects(V, leftEnd, rightEnd, F)267  shows Connects(P, quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd), F)268proof269  intros X classX Y classY270  obtain ⟨u, inX⟩ :=271    Nonempty.of_ne_empty with (partition.left with X, classX).right272  obtain ⟨v, inY⟩ :=273    Nonempty.of_ne_empty with (partition.left with Y, classY).right274  have uIn := (partition.left with X, classX).left with u, inX275  have vIn := (partition.left with Y, classY).left with v, inY276  have classU := classOf.eq_of_member with partition.right.left, classX, inX277  have classV := classOf.eq_of_member with partition.right.left, classY, inY278  have joined := Joined.quotient with279    graph, partition, edges, uIn, vIn, (connected with u, uIn, v, vIn)280  rwa [classU, classV] at joined281282theorem quotientEnd.ends (V E P leftEnd rightEnd F : Set)283  requires graph : Graph(V, E, leftEnd, rightEnd)284  requires partition : Partition(V, P)285  requires edges : F ⊆ E286  shows ∀ e ∈ F,287    quotientEnd(E, P, leftEnd)(e) ∈ P ∧ quotientEnd(E, P, rightEnd)(e) ∈ P288proof289  exact ends_in.subset with290    (Graph.ends with (quotientEnd.graph with graph, partition)), edges291292-- A connected edge set crosses a partition in at least |P| − 1 edges: its293-- crossing edges connect the quotient, which has |P| vertices.294theorem crossingClasses.lower_bound (V E P leftEnd rightEnd F : Set)295  requires graph : Graph(V, E, leftEnd, rightEnd)296  requires finiteVertices : Finite(V)297  requires finiteEdges : Finite(E)298  requires partition : Partition(V, P)299  requires edges : F ⊆ E300  requires connected : Connects(V, leftEnd, rightEnd, F)301  shows cardinality(P) ≤302    cardinality(crossingClasses(P, leftEnd, rightEnd, F)) + 1303proof304  have finiteClasses := Partition.finite with finiteVertices, partition305  have crossingEdges : crossingClasses(P, leftEnd, rightEnd, F) ⊆ E :=306    Subset.transitive with crossingClasses.subset, edges307  have finiteCrossing := Finite.subset with finiteEdges, crossingEdges308  have ends := quotientEnd.ends with graph, partition, crossingEdges309  have connectedQuotient :=310    (Connects.quotient_iff with graph, partition, edges).forward311      with (Connects.quotient with graph, partition, edges, connected)312  have lower := componentsBy.lower_bound313    with finiteClasses, finiteCrossing, ends314  have one := componentsBy.le_one_of_connected with connectedQuotient315  arith316317-- Section: Necessity of the packing condition.318319theorem sub.one_le_of_le_add_one (a b : Nat)320  requires below : a ≤ b + 1321  shows a - 1 ≤ b322proof323  have shape := natural.zero_or_successor at a324  rcases shape with zero | ⟨q, natural, rfl⟩325  . rw [zero, sub.zero_left]326    arith327  . rw [sub.one, predecessor.succ]328    arith329330-- The first j colour classes together.331def coloursBelow (T : Set, j : Nat) → Set332  | T, zero => ∅333  | T, succ(m) => coloursBelow(T, m) ∪ T(m)334335-- The first j trees of a packing lie in E, miss every later colour, and336-- cross a partition in at least j(|P| − 1) edges, one tree at a time.337theorem coloursBelow.count (V E P leftEnd rightEnd T : Set, k j : Nat)338  requires graph : Graph(V, E, leftEnd, rightEnd)339  requires finiteVertices : Finite(V)340  requires finiteEdges : Finite(E)341  requires partition : Partition(V, P)342  requires function : FunctionBetween(T, k, 𝒫(E))343  requires apart : ∀ i ∈ k, ∀ j ∈ k, i ≠ j → Disjoint(T(i), T(j))344  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))345  requires below : j ≤ k346  shows coloursBelow(T, j) ⊆ E ∧347    (∀ i ∈ k, j ≤ i → Disjoint(coloursBelow(T, j), T(i))) ∧348    j * (cardinality(P) - 1) ≤349      cardinality(crossingClasses(P, leftEnd, rightEnd, coloursBelow(T, j)))350proof351  induction j352  | zero =>353    intro below354    unfold coloursBelow355    refine ⟨empty.subset, _, _⟩356    . intros i inK order357      exact Disjoint.empty_left358    . have finiteCrossing := crossingClasses.finite359        at P, leftEnd, rightEnd, ∅ with Finite.empty360      have finiteClasses := Partition.finite with finiteVertices, partition361      rw mul.left_zero362      arith363  | succ(m) using ih =>364    intro below365    have earlier : m ≤ k by arith366    obtain ⟨subsetE, apartBelow, count⟩ := ih with earlier367    have less : m < k by arith368    have inK := membership.of_Less at m, k with *, less369    have classE : T(m) ⊆ E := powerset.membership_iff.forward with370      (FunctionBetween.apply_closed with function, inK)371    have tree := trees with m, inK372    unfold coloursBelow373    refine ⟨(Subset.union2_iff.backward with ⟨subsetE, classE⟩), _, _⟩374    . intros i inK2 order375      have later : m ≤ i by arith376      have distinct : m ≠ i by arith377      exact Disjoint.union2_iff.backward with378        ⟨(apartBelow with i, inK2, later),379          (apart with m, inK, i, inK2, distinct)⟩380    . -- The crossing edges of the new tree are disjoint from those so far,381      -- and number at least |P| − 1.382      have apartClass := apartBelow with m, inK, (LessEqual.reflexive at m)383      have apartCrossing : Disjoint(crossingClasses(P, leftEnd, rightEnd,384          coloursBelow(T, m)), crossingClasses(P, leftEnd, rightEnd, T(m))) :=385        Disjoint.of_subset_right with386          (Disjoint.of_subset_left with apartClass, crossingClasses.subset),387          crossingClasses.subset388      have finiteBelow := crossingClasses.finite389        at P, leftEnd, rightEnd, coloursBelow(T, m)390        with (Finite.subset with finiteEdges, subsetE)391      have finiteClass := crossingClasses.finite392        at P, leftEnd, rightEnd, T(m)393        with (Finite.subset with finiteEdges, classE)394      have sum := cardinality.union_disjoint395        with finiteBelow, finiteClass, apartCrossing396      have lower := crossingClasses.lower_bound with397        graph, finiteVertices, finiteEdges, partition, classE, tree.right.left398      have finiteClasses := Partition.finite with finiteVertices, partition399      have bound := sub.one_le_of_le_add_one with lower400      have step := mul.succ_left at m, cardinality(P) - 1401      rw [crossingClasses.union, sum, step]402      arith403404-- Necessity of the packing condition: a tree meets every partition in at405-- least |P| − 1 crossing edges, and the k trees are disjoint.406theorem TreePacking.condition (V E leftEnd rightEnd : Set, k : Nat)407  requires graph : Graph(V, E, leftEnd, rightEnd)408  requires finiteVertices : Finite(V)409  requires finiteEdges : Finite(E)410  requires packing : TreePacking(V, E, leftEnd, rightEnd, k)411  shows PackingCondition(V, E, leftEnd, rightEnd, k)412proof413  intros P partition414  obtain ⟨T, function, apart, trees⟩ := packing415  obtain ⟨subsetE, _, count⟩ := coloursBelow.count with416    graph, finiteVertices, finiteEdges, partition, function, apart, trees,417    (LessEqual.reflexive at k)418  have finiteClasses := Partition.finite with finiteVertices, partition419  have finiteCrossing := crossingClasses.finite420    at P, leftEnd, rightEnd, E with finiteEdges421  have finiteBelow := crossingClasses.finite422    at P, leftEnd, rightEnd, coloursBelow(T, k)423    with (Finite.subset with finiteEdges, subsetE)424  have bound := cardinality.monotone with finiteCrossing,425    (crossingClasses.monotone with subsetE)426  arith427428-- Section: A spanning tree internally connected on a partition.429430-- When T connects each class of P from within, the edges of T inside the431-- classes have exactly the classes as components.432theorem componentBy.eq_class (V leftEnd rightEnd T P X u : Set)433  requires partition : Partition(V, P)434  requires ends : ∀ e ∈ T, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V435  requires internal : InternallyConnected(leftEnd, rightEnd, T, P)436  requires class : X ∈ P437  requires member : u ∈ X438  shows componentBy(V, leftEnd, rightEnd,439    T ∖ crossingClasses(P, leftEnd, rightEnd, T), u) = X440proof441  have apart := partition.right.left442  have subsetV := (partition.left with X, class).left443  -- X is closed under the edges inside classes: such an edge has both ends444  -- in one class.445  have closed : ClosedUnder(leftEnd, rightEnd,446      T ∖ crossingClasses(P, leftEnd, rightEnd, T), X)447    intros e edge448    obtain ⟨inT, uncrossed⟩ := edge449    obtain ⟨leftIn, rightIn⟩ := ends with e, inT450    have same : classOf(P, leftEnd(e)) = classOf(P, rightEnd(e))451      by_contra different452      exact uncrossed with ⟨inT, different⟩453    rw [← (classOf.eq_iff_member with partition, class, leftIn),454      ← (classOf.eq_iff_member with partition, class, rightIn), same]455  -- The edges of T inside X lie inside the classes.456  have insideSubset : inside(leftEnd, rightEnd, T, X) ⊆457      T ∖ crossingClasses(P, leftEnd, rightEnd, T)458    intros e edge459    obtain ⟨inT, leftX, rightX⟩ := edge460    have leftClass := classOf.eq_of_member with apart, class, leftX461    have rightClass := classOf.eq_of_member with apart, class, rightX462    refine ⟨inT, _⟩463    intro crossed464    have different := crossed.right465    cc466  ext v467  constructor468  . intro inComponent469    exact inComponent.right with X, member, closed470  . intro inX471    have joined := internal with X, class, u, member, v, inX472    exact ⟨(subsetV with v, inX), (Joined.monotone with insideSubset, joined)⟩473474theorem componentsBy.eq_classes (V leftEnd rightEnd T P : Set)475  requires partition : Partition(V, P)476  requires ends : ∀ e ∈ T, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V477  requires internal : InternallyConnected(leftEnd, rightEnd, T, P)478  shows componentsBy(V, leftEnd, rightEnd,479    T ∖ crossingClasses(P, leftEnd, rightEnd, T)) = P480proof481  ext X482  constructor483  . intro inComponents484    obtain ⟨u, inV, rfl⟩ := inComponents485    obtain ⟨Y, classY, inY⟩ := partition.right.right with u, inV486    rw componentBy.eq_class with partition, ends, internal, classY, inY487    exact classY488  . intro class489    obtain ⟨u, inX⟩ :=490      Nonempty.of_ne_empty with (partition.left with X, class).right491    have inV := (partition.left with X, class).left with u, inX492    rw ← (componentBy.eq_class with partition, ends, internal, class, inX)493    exact componentsBy.contains with inV494495-- A spanning tree internally connected on P crosses P in exactly |P| − 1496-- edges: its uncrossing edges form a forest with the classes as components,497-- so they number |V| − |P|.498theorem SpanningTree.crossing_count (V leftEnd rightEnd T P : Set)499  requires finiteVertices : Finite(V)500  requires partition : Partition(V, P)501  requires ends : ∀ e ∈ T, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V502  requires tree : SpanningTree(V, leftEnd, rightEnd, T)503  requires internal : InternallyConnected(leftEnd, rightEnd, T, P)504  shows cardinality(crossingClasses(P, leftEnd, rightEnd, T)) + 1 =505    cardinality(P)506proof507  obtain ⟨finite, _, count⟩ := tree508  have restSubset := difference.subset_left509    at T, crossingClasses(P, leftEnd, rightEnd, T)510  have restFinite := Finite.subset with finite, restSubset511  have restEnds := ends_in.subset with ends, restSubset512  have finiteCrossing := crossingClasses.finite513    at P, leftEnd, rightEnd, T with finite514  have finiteClasses := Partition.finite with finiteVertices, partition515  have forest := Forest.subset with516    (SpanningTree.forest with finiteVertices, ends, tree), restSubset517  have components := componentsBy.eq_classes with partition, ends, internal518  have upper := Forest.edge_bound with finiteVertices, restEnds, forest519  have lower := componentsBy.lower_bound520    with finiteVertices, restFinite, restEnds521  rw components at upper, lower522  have cover : (T ∖ crossingClasses(P, leftEnd, rightEnd, T)) ∪523      crossingClasses(P, leftEnd, rightEnd, T) = T524    have crossingSubset := crossingClasses.subset at P, leftEnd, rightEnd, T525    ext e526    simp527  have sum := cardinality.union_disjoint with528    restFinite, finiteCrossing, Disjoint.difference_left529  rw cover at sum530  arith531