Grace/Cumulus/GraphTheory/DoubleCover/Cycles.g17

Open in Workbench Download source

Imports

Covers · Cardinal.FiniteUnion

Declarations

• Cycle predicate
• edgesInto def
• edgesInto.subset theorem derivation
• edgesInto.ends_inside theorem derivation
• edgesInto.ends_outside theorem derivation
• edgesInto.even theorem derivation
• EvenEdgeSet.smaller_of_apart theorem derivation
• avoiding def
• avoiding.subset theorem derivation
• avoiding.degree theorem derivation
• avoiding.not_joined theorem derivation
• edge.other_end theorem derivation
• Disjoint.singleton_of_fresh theorem derivation
• degreeIn.single_parity_ends theorem derivation
• EvenEdgeSet.of_path_two_edges theorem derivation
• EvenEdgeSet.smaller_of_degree theorem derivation
• EvenEdgeSet.cycle_or_smaller theorem derivation
• cardinality.proper theorem derivation
• EvenEdgeSet.cycle_of_size theorem derivation
• EvenEdgeSet.contains_cycle theorem derivation
• cycleDecomposition.empty theorem derivation
• EvenEdgeSet.decomposition_of_size theorem derivation
• EvenEdgeSet.cycle_decomposition theorem derivation

Source

1-- Cycles in even edge sets: a cycle is a nonempty even edge set with every2-- degree 0 or 2 whose edges are joined to one another, every nonempty even3-- edge set contains a cycle, and a finite even edge set splits into cycles.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.DoubleCover.Cycles10import Covers11import Cardinal.FiniteUnion1213-- Section: Cycles in even sets.1415-- A cycle: a nonempty even edge set in which every vertex has degree 0 or 216-- and whose edges are all joined to one another.17predicate Cycle (V leftEnd rightEnd C : Set) :=18  C ≠ ∅ ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧19  (∀ v ∈ V, degreeIn(leftEnd, rightEnd, C, v) = 0 ∨20    degreeIn(leftEnd, rightEnd, C, v) = 2) ∧21  (∀ e ∈ C, ∀ f ∈ C,22    Joined(leftEnd, rightEnd, C, leftEnd(e), leftEnd(f)))2324-- A nonempty even edge set that is not a cycle has a proper nonempty even25-- subset: the edges into one component when two edges are not joined, and26-- a path closed by two edges at a vertex of degree other than two.2728-- The edges of C whose left end lies in A. When A is closed under C they29-- carry every end of C at a vertex of A and none elsewhere.30def edgesInto (leftEnd C A : Set) : Set := { e ∈ C | leftEnd(e) ∈ A }3132theorem edgesInto.subset (leftEnd C A : Set)33  shows edgesInto(leftEnd, C, A) ⊆ C34proof35  intros e he36  exact he.left3738theorem edgesInto.ends_inside (leftEnd rightEnd C A v : Set)39  requires closed : ClosedUnder(leftEnd, rightEnd, C, A)40  requires member : v ∈ A41  shows incidentEnds(leftEnd, rightEnd, edgesInto(leftEnd, C, A), v) =42    incidentEnds(leftEnd, rightEnd, C, v)43proof44  apply Subset.antisymmetric45  . exact incidentEnds.monotone with edgesInto.subset46  . intros p hp47    obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp48    have sides := (incidentEnds.pair.forward with hp).right49    have balanced := closed with e, he50    have inside : leftEnd(e) ∈ A51      rcases sides with ⟨_, atLeft⟩ | ⟨_, atRight⟩52      . rw atLeft53        exact member54      . rw atRight at balanced55        exact balanced.backward with member56    exact incidentEnds.pair.backward with ⟨⟨he, inside⟩, sides⟩5758theorem edgesInto.ends_outside (leftEnd rightEnd C A v : Set)59  requires closed : ClosedUnder(leftEnd, rightEnd, C, A)60  requires outside : ¬v ∈ A61  shows incidentEnds(leftEnd, rightEnd, edgesInto(leftEnd, C, A), v) = ∅62proof63  apply Subset.antisymmetric64  . intros p hp65    obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp66    have sides := (incidentEnds.pair.forward with hp).right67    have balanced := closed with e, he.left68    have inside := he.right69    exfalso70    apply outside71    rcases sides with ⟨_, atLeft⟩ | ⟨_, atRight⟩72    . rw ← atLeft73      exact inside74    . rw ← atRight75      exact balanced.forward with inside76  . exact empty.subset7778theorem edgesInto.even (V leftEnd rightEnd C A : Set)79  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)80  requires closed : ClosedUnder(leftEnd, rightEnd, C, A)81  shows EvenEdgeSet(V, leftEnd, rightEnd, edgesInto(leftEnd, C, A))82proof83  constructor84  . exact Finite.subset with even.left, edgesInto.subset85  . intros v hv86    have evenV := even.right with v, hv87    unfold degreeIn at evenV88    unfold degreeIn89    by_cases member : v ∈ A90    . rw edgesInto.ends_inside with closed, member91      exact evenV92    . rw [(edgesInto.ends_outside with closed, member), cardinality.empty]93      exact Even.zero9495-- Two edges of an even set not joined through it: the edges into the96-- component of the first form a proper nonempty even subset.97theorem EvenEdgeSet.smaller_of_apart (V leftEnd rightEnd C e f : Set)98  requires ends : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V99  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)100  requires edges : e ∈ C ∧ f ∈ C101  requires apart : ¬Joined(leftEnd, rightEnd, C, leftEnd(e), leftEnd(f))102  shows ∃ B ⊆ C, B ≠ ∅ ∧ B ≠ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, B)103proof104  have closed := componentBy.closed at V, leftEnd, rightEnd, C, leftEnd(e)105    with ends106  have leftIn := (ends with e, edges.left).left107  have inside : e ∈ edgesInto(leftEnd, C,108      componentBy(V, leftEnd, rightEnd, C, leftEnd(e))) :=109    ⟨edges.left, (componentBy.self with leftIn)⟩110  have outside : ¬f ∈ edgesInto(leftEnd, C,111      componentBy(V, leftEnd, rightEnd, C, leftEnd(e)))112    intro member113    exact apart with member.right.right114  refine ⟨edgesInto(leftEnd, C,115    componentBy(V, leftEnd, rightEnd, C, leftEnd(e))),116    edgesInto.subset, ?_, ?_, (edgesInto.even with even, closed)⟩117  . intro empty118    rw empty at inside119    simp at inside120  . intro same121    rw same at outside122    exact outside with edges.right123124-- The edges of C not at v; v is isolated in them.125def avoiding (leftEnd rightEnd C v : Set) : Set :=126  { g ∈ C | leftEnd(g) ≠ v ∧ rightEnd(g) ≠ v }127128theorem avoiding.subset (leftEnd rightEnd C v : Set)129  shows avoiding(leftEnd, rightEnd, C, v) ⊆ C130proof131  intros g hg132  exact hg.left133134theorem avoiding.degree (leftEnd rightEnd C v Q : Set)135  requires subset : Q ⊆ avoiding(leftEnd, rightEnd, C, v)136  shows degreeIn(leftEnd, rightEnd, Q, v) = 0137proof138  have none : incidentEnds(leftEnd, rightEnd, Q, v) = ∅139    apply Subset.antisymmetric140    . intros p hp141      obtain ⟨g, hg, i, hi, rfl⟩ := incidentEnds.shape with hp142      have sides := (incidentEnds.pair.forward with hp).right143      have away := (subset with g, hg).right144      exfalso145      tauto146    . exact empty.subset147  unfold degreeIn148  rw none149  exact cardinality.empty150151-- A vertex other than v is not joined to v by the edges avoiding v.152theorem avoiding.not_joined (V leftEnd rightEnd C v a : Set)153  requires ends : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V154  requires vertex : a ∈ V155  requires distinct : a ≠ v156  shows ¬Joined(leftEnd, rightEnd, avoiding(leftEnd, rightEnd, C, v), a, v)157proof158  intro joined159  have closed : ClosedUnder(leftEnd, rightEnd,160      avoiding(leftEnd, rightEnd, C, v), V ∖ {v})161    intros g hg162    have bounds := ends with g, hg.left163    have away := hg.right164    simp [bounds.left, bounds.right, away.left, away.right]165  have start : a ∈ V ∖ {v} by simp [vertex, distinct]166  have reached := joined with V ∖ {v}, start, closed167  simp at reached168169-- An edge at v that is not a loop has its other end elsewhere in V.170theorem edge.other_end (V leftEnd rightEnd e v : Set)171  requires ends : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V172  requires loop : leftEnd(e) ≠ rightEnd(e)173  requires atV : leftEnd(e) = v ∨ rightEnd(e) = v174  shows ∃ a ∈ V, a ≠ v ∧ ((leftEnd(e) = v ∧ rightEnd(e) = a) ∨175    (leftEnd(e) = a ∧ rightEnd(e) = v))176proof177  cases atV with atLeft | atRight178  . refine ⟨rightEnd(e), ends.right, ?_, ?_⟩179    . cc180    . left181      exact ⟨atLeft, rfl⟩182  . refine ⟨leftEnd(e), ends.left, ?_, ?_⟩183    . cc184    . right185      exact ⟨rfl, atRight⟩186187theorem Disjoint.singleton_of_fresh (A x : Set)188  requires fresh : ¬x ∈ A189  shows Disjoint(A, {x})190proof191  simp [Disjoint.iff, fresh]192193-- An edge with the two distinct ends v and a has odd degree exactly there.194theorem degreeIn.single_parity_ends (leftEnd rightEnd e v a : Set)195  requires shape : (leftEnd(e) = v ∧ rightEnd(e) = a) ∨196    (leftEnd(e) = a ∧ rightEnd(e) = v)197  requires distinct : a ≠ v198  shows ∀ w, (Even(degreeIn(leftEnd, rightEnd, {e}, w)) ↔ (w ≠ v ∧ w ≠ a))199proof200  intro w201  have loop : leftEnd(e) ≠ rightEnd(e)202    rcases shape with ⟨l, r⟩ | ⟨l, r⟩203    . rw [l, r]204      cc205    . rw [l, r]206      cc207  have single := degreeIn.single_parity with loop, w208  rcases shape with ⟨l, r⟩ | ⟨l, r⟩209  . rw [l, r] at single210    exact single211  . rw [l, r] at single212    tauto213214-- A path from a to b closed by an edge va and an edge vb is even: at each215-- vertex the three degrees have an even sum.216theorem EvenEdgeSet.of_path_two_edges (V leftEnd rightEnd Q e f v a b : Set)217  requires finite : Finite(Q)218  requires fresh : ¬e ∈ Q ∧ ¬f ∈ Q ∧ e ≠ f219  requires shapeE : (leftEnd(e) = v ∧ rightEnd(e) = a) ∨220    (leftEnd(e) = a ∧ rightEnd(e) = v)221  requires shapeF : (leftEnd(f) = v ∧ rightEnd(f) = b) ∨222    (leftEnd(f) = b ∧ rightEnd(f) = v)223  requires distinct : a ≠ v ∧ b ≠ v224  requires path : ∀ w ∈ V,225    (Even(degreeIn(leftEnd, rightEnd, Q, w)) ↔ (w = a ↔ w = b))226  shows EvenEdgeSet(V, leftEnd, rightEnd, (Q ∪ {e}) ∪ {f})227proof228  obtain ⟨eFresh, fFresh, different⟩ := fresh229  obtain ⟨notA, notB⟩ := distinct230  have apartE := Disjoint.singleton_of_fresh with eFresh231  have fOutside : ¬f ∈ Q ∪ {e} by simp [fFresh, different]232  have apartF := Disjoint.singleton_of_fresh with fOutside233  have finiteE : Finite(Q ∪ {e}) := Finite.union with finite, Finite.singleton234  have parityE := degreeIn.single_parity_ends with shapeE, notA235  have parityF := degreeIn.single_parity_ends with shapeF, notB236  constructor237  . exact Finite.union with finiteE, Finite.singleton238  . intros w hw239    rw [(degreeIn.union_disjoint with finiteE, Finite.singleton, apartF),240      (degreeIn.union_disjoint with finite, Finite.singleton, apartE),241      Even.add_iff, Even.add_iff, (path with w, hw), (parityE with w),242      (parityF with w)]243    have notBothA : ¬(w = v ∧ w = a)244      intro both245      have same : a = v by cc246      exact notA with same247    have notBothB : ¬(w = v ∧ w = b)248      intro both249      have same : b = v by cc250      exact notB with same251    tauto252253-- A vertex of degree other than 0 and 2 in an even set gives a proper254-- nonempty even subset: a loop by itself, or else an edge e = va at v, a255-- second edge f = vb of the cut at the component of a away from v, and a256-- path from a to b avoiding v, which together have degree two at v.257theorem EvenEdgeSet.smaller_of_degree (V leftEnd rightEnd C v : Set)258  requires finiteVertices : Finite(V)259  requires ends : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V260  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)261  requires vertex : v ∈ V262  requires notZero : degreeIn(leftEnd, rightEnd, C, v) ≠ 0263  requires notTwo : degreeIn(leftEnd, rightEnd, C, v) ≠ 2264  shows ∃ B ⊆ C, B ≠ ∅ ∧ B ≠ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, B)265proof266  have finite := even.left267  by_cases loops : ∃ g ∈ C, leftEnd(g) = rightEnd(g)268  . -- A loop is an even set by itself, of degree 0 or 2 at v.269    obtain ⟨g, hg, loop⟩ := loops270    refine ⟨{g}, (singleton.subset_iff.backward with hg),271      singleton.ne_empty, ?_, (EvenEdgeSet.loop with loop)⟩272    intro same273    rw ← same at notZero, notTwo274    by_cases atV : leftEnd(g) = v275    . have right : rightEnd(g) = v by cc276      exact notTwo with (degreeIn.loop with atV, right)277    . have right : rightEnd(g) ≠ v by cc278      exact notZero with (degreeIn.absent with atV, right)279  . have noLoop : ∀ g ∈ C, leftEnd(g) ≠ rightEnd(g)280      intros g hg same281      exact loops with ⟨g, hg, same⟩282    -- An edge e at v, with other end a.283    have inhabited : incidentEnds(leftEnd, rightEnd, C, v) ≠ ∅284      intro empty285      apply notZero286      unfold degreeIn287      rw [empty, cardinality.empty]288    obtain ⟨p, hp⟩ := Nonempty.of_ne_empty with inhabited289    obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp290    have sides := (incidentEnds.pair.forward with hp).right291    have atV : leftEnd(e) = v ∨ rightEnd(e) = v by tauto292    have loopE := noLoop with e, he293    obtain ⟨a, aIn, aNotV, shapeE⟩ :=294      edge.other_end with (ends with e, he), loopE, atV295    -- The component A of a in the edges avoiding v, which v lies outside.296    have subsetS := avoiding.subset at leftEnd, rightEnd, C, v297    have finiteS := Finite.subset with finite, subsetS298    have endsS := ends_in.subset with ends, subsetS299    have closed := componentBy.closed at V, leftEnd, rightEnd,300      avoiding(leftEnd, rightEnd, C, v), a with endsS301    have aInA := componentBy.self at V, leftEnd, rightEnd,302      avoiding(leftEnd, rightEnd, C, v), a with aIn303    have vOut : ¬v ∈ componentBy(V, leftEnd, rightEnd,304        avoiding(leftEnd, rightEnd, C, v), a)305      intro member306      exact avoiding.not_joined with ends, aIn, aNotV, member.right307    -- The cut at A holds e, so it holds a second edge f.308    have eCrosses : e ∈ crossing(leftEnd, rightEnd, C,309        componentBy(V, leftEnd, rightEnd, avoiding(leftEnd, rightEnd, C, v), a))310      refine ⟨he, ?_⟩311      rcases shapeE with ⟨l, r⟩ | ⟨l, r⟩312      . right313        rw [l, r]314        exact ⟨aInA, vOut⟩315      . left316        rw [l, r]317        exact ⟨aInA, vOut⟩318    have notSingle := EvenEdgeSet.crossing_ne_singleton at V, leftEnd,319      rightEnd, C, componentBy(V, leftEnd, rightEnd,320        avoiding(leftEnd, rightEnd, C, v), a), e321      with finiteVertices, even, componentBy.subset322    have second : ∃ f ∈ crossing(leftEnd, rightEnd, C,323        componentBy(V, leftEnd, rightEnd,324          avoiding(leftEnd, rightEnd, C, v), a)), f ≠ e325      by_contra none326      apply notSingle327      ext g328      rw singleton.membership329      constructor330      . intro hg331        by_contra other332        exact none with ⟨g, hg, other⟩333      . intro same334        rw same335        exact eCrosses336    obtain ⟨f, fCrosses, fNotE⟩ := second337    have hf : f ∈ C := fCrosses.left338    have fSides := fCrosses.right339    -- f is at v, since A is closed under the edges avoiding v, and its other340    -- end b lies in A.341    have fAtV : leftEnd(f) = v ∨ rightEnd(f) = v342      by_contra away343      have both : leftEnd(f) ≠ v ∧ rightEnd(f) ≠ v by tauto344      have balanced := closed with f, ⟨hf, both⟩345      tauto346    have loopF := noLoop with f, hf347    obtain ⟨b, bIn, bNotV, shapeF⟩ :=348      edge.other_end with (ends with f, hf), loopF, fAtV349    have bInA : b ∈ componentBy(V, leftEnd, rightEnd,350        avoiding(leftEnd, rightEnd, C, v), a)351      rcases shapeF with ⟨l, r⟩ | ⟨l, r⟩352      . rw [l, r] at fSides353        tauto354      . rw [l, r] at fSides355        tauto356    -- A path from a to b through the edges avoiding v.357    have pathExists : ∃ Q ⊆ avoiding(leftEnd, rightEnd, C, v), ∀ w ∈ V,358        (Even(degreeIn(leftEnd, rightEnd, Q, w)) ↔ (w = a ↔ w = b))359      by_cases same : a = b360      . refine ⟨∅, empty.subset, ?_⟩361        intros w hw362        rw [degreeIn.empty, same]363        simp [Even.zero]364      . have joined := componentBy.joined with bInA365        obtain ⟨Q, inS, path⟩ :=366          Joined.path with finiteS, endsS, same, joined367        refine ⟨Q, inS, ?_⟩368        intros w hw369        rw (path with w, hw)370        have notBoth : ¬(w = a ∧ w = b)371          intro both372          have equal : a = b by cc373          exact same with equal374        tauto375    obtain ⟨Q, QinS, path⟩ := pathExists376    have finiteQ := Finite.subset with finiteS, QinS377    have eFresh : ¬e ∈ Q378      intro inQ379      have away := (QinS with e, inQ).right380      tauto381    have fFresh : ¬f ∈ Q382      intro inQ383      have away := (QinS with f, inQ).right384      tauto385    have eNotF : e ≠ f by cc386    have evenB := EvenEdgeSet.of_path_two_edges with finiteQ,387      ⟨eFresh, fFresh, eNotF⟩, shapeE, shapeF, ⟨aNotV, bNotV⟩, path388    have QsubC := Subset.transitive with QinS, subsetS389    have QeSub : Q ∪ {e} ⊆ C := Subset.union2_iff.backward390      with ⟨QsubC, (singleton.subset_iff.backward with he)⟩391    have BsubC : (Q ∪ {e}) ∪ {f} ⊆ C := Subset.union2_iff.backward392      with ⟨QeSub, (singleton.subset_iff.backward with hf)⟩393    refine ⟨(Q ∪ {e}) ∪ {f}, BsubC, ?_, ?_, evenB⟩394    . intro empty395      have inB : e ∈ (Q ∪ {e}) ∪ {f} by simp396      rw empty at inB397      simp at inB398    . -- The degree at v is two in the new set and not in C.399      intro same400      apply notTwo401      rw ← same402      have apartE := Disjoint.singleton_of_fresh with eFresh403      have fOutside : ¬f ∈ Q ∪ {e} by simp [fFresh, fNotE]404      have apartF := Disjoint.singleton_of_fresh with fOutside405      have finiteQe : Finite(Q ∪ {e}) :=406        Finite.union with finiteQ, Finite.singleton407      rw [(degreeIn.union_disjoint with finiteQe, Finite.singleton, apartF),408        (degreeIn.union_disjoint with finiteQ, Finite.singleton, apartE),409        (avoiding.degree with QinS), (degreeIn.end with loopE, atV),410        (degreeIn.end with loopF, fAtV)]411      compute412413-- A nonempty even edge set is a cycle or has a proper nonempty even subset.414theorem EvenEdgeSet.cycle_or_smaller (V leftEnd rightEnd C : Set)415  requires finiteVertices : Finite(V)416  requires ends : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V417  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)418  requires nonempty : C ≠ ∅419  shows Cycle(V, leftEnd, rightEnd, C) ∨420    (∃ B ⊆ C, B ≠ ∅ ∧ B ≠ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, B))421proof422  by_cases degrees : ∀ v ∈ V, degreeIn(leftEnd, rightEnd, C, v) = 0 ∨423    degreeIn(leftEnd, rightEnd, C, v) = 2424  . by_cases joined : ∀ e ∈ C, ∀ f ∈ C,425      Joined(leftEnd, rightEnd, C, leftEnd(e), leftEnd(f))426    . left427      exact ⟨nonempty, even, degrees, joined⟩428    . right429      have found : ∃ e ∈ C, ∃ f ∈ C,430          ¬Joined(leftEnd, rightEnd, C, leftEnd(e), leftEnd(f))431        by_contra none432        apply joined433        intros e he f hf434        by_contra apart435        exact none with ⟨e, he, f, hf, apart⟩436      obtain ⟨e, he, f, hf, apart⟩ := found437      exact EvenEdgeSet.smaller_of_apart with ends, even, ⟨he, hf⟩, apart438  . right439    have found : ∃ v ∈ V, degreeIn(leftEnd, rightEnd, C, v) ≠ 0 ∧440        degreeIn(leftEnd, rightEnd, C, v) ≠ 2441      by_contra none442      apply degrees443      intros v hv444      by_contra neither445      have both : degreeIn(leftEnd, rightEnd, C, v) ≠ 0 ∧446          degreeIn(leftEnd, rightEnd, C, v) ≠ 2 by tauto447      exact none with ⟨v, hv, both⟩448    obtain ⟨v, hv, notZero, notTwo⟩ := found449    exact EvenEdgeSet.smaller_of_degree450      with finiteVertices, ends, even, hv, notZero, notTwo451452-- A proper subset of a finite set is strictly smaller.453theorem cardinality.proper (B C : Set)454  requires finite : Finite(C)455  requires subset : B ⊆ C456  requires proper : B ≠ C457  shows cardinality(B) < cardinality(C)458proof459  have missing : ∃ a ∈ C, ¬a ∈ B460    by_contra none461    apply proper462    apply Subset.antisymmetric463    . exact subset464    . intros a ha465      by_contra outside466      exact none with ⟨a, ha, outside⟩467  obtain ⟨a, ha, outside⟩ := missing468  exact cardinality.strict with finite, subset, ha, outside469470-- Every nonempty even edge set contains a cycle: by induction on the number471-- of edges, a nonempty even set is a cycle or has a smaller nonempty even472-- subset.473theorem EvenEdgeSet.cycle_of_size (V leftEnd rightEnd F : Set, n : Nat)474  requires finiteVertices : Finite(V)475  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V476  shows ∀ C ⊆ F, cardinality(C) ≤ n → C ≠ ∅ →477    EvenEdgeSet(V, leftEnd, rightEnd, C) →478    ∃ D ⊆ C, Cycle(V, leftEnd, rightEnd, D)479proof480  induction n481  | zero =>482    intros C bound size nonempty even483    have finiteC := even.left484    have zero : cardinality(C) = 0 by arith485    exfalso486    exact nonempty with (cardinality.eq_empty_of_zero with finiteC, zero)487  | succ(k) using ih =>488    intros C bound size nonempty even489    have finiteC := even.left490    have endsC := ends_in.subset with ends, bound491    have split := EvenEdgeSet.cycle_or_smaller492      with finiteVertices, endsC, even, nonempty493    cases split with cycle | smaller494    . exact ⟨C, Subset.reflexive, cycle⟩495    . obtain ⟨B, inC, nonemptyB, proper, evenB⟩ := smaller496      have finiteB := evenB.left497      have less := cardinality.proper with finiteC, inC, proper498      have smallerSize : cardinality(B) ≤ k by arith499      obtain ⟨D, inB, cycle⟩ := ih with B,500        (Subset.transitive with inC, bound), smallerSize, nonemptyB, evenB501      exact ⟨D, (Subset.transitive with inB, inC), cycle⟩502503theorem EvenEdgeSet.contains_cycle (V leftEnd rightEnd F : Set)504  requires finiteVertices : Finite(V)505  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V506  requires even : EvenEdgeSet(V, leftEnd, rightEnd, F)507  requires nonempty : F ≠ ∅508  shows ∃ C ⊆ F, Cycle(V, leftEnd, rightEnd, C)509proof510  have finite := even.left511  have bound : cardinality(F) ≤ cardinality(F) by arith512  exact EvenEdgeSet.cycle_of_size513    at V, leftEnd, rightEnd, F, cardinality(F)514    with finiteVertices, ends, F, Subset.reflexive, bound, nonempty, even515516-- Section: Decomposition.517518-- Splitting an even edge set into cycles: remove a cycle and split the519-- rest, which is even as its symmetric difference with the cycle is the520-- whole set. The empty set splits into no cycles.521theorem cycleDecomposition.empty (V leftEnd rightEnd C : Set)522  requires empty : C = ∅523  shows ∃ D, Finite(D) ∧ (∀ K ∈ D, Cycle(V, leftEnd, rightEnd, K)) ∧524    (∀ K ∈ D, ∀ B ∈ D, K ≠ B → Disjoint(K, B)) ∧ ⋃(D) = C525proof526  refine ⟨∅, Finite.empty, ?_, ?_, ?_⟩527  . intros K hK528    simp at hK529  . intros K hK530    simp at hK531  . rw [union.empty, empty]532533theorem EvenEdgeSet.decomposition_of_size (V leftEnd rightEnd F : Set, n : Nat)534  requires finiteVertices : Finite(V)535  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V536  shows ∀ C ⊆ F, cardinality(C) ≤ n →537    EvenEdgeSet(V, leftEnd, rightEnd, C) →538    ∃ D, Finite(D) ∧ (∀ K ∈ D, Cycle(V, leftEnd, rightEnd, K)) ∧539      (∀ K ∈ D, ∀ B ∈ D, K ≠ B → Disjoint(K, B)) ∧ ⋃(D) = C540proof541  induction n542  | zero =>543    intros C bound size even544    have finiteC := even.left545    have zero : cardinality(C) = 0 by arith546    exact cycleDecomposition.empty547      with (cardinality.eq_empty_of_zero with finiteC, zero)548  | succ(k) using ih =>549    intros C bound size even550    have finiteC := even.left551    by_cases empty : C = ∅552    . exact cycleDecomposition.empty with empty553    . have endsC := ends_in.subset with ends, bound554      obtain ⟨K, inC, cycle⟩ :=555        EvenEdgeSet.contains_cycle with finiteVertices, endsC, even, empty556      -- The rest C ∖ K is even and smaller.557      have restSubset := difference.subset_left at C, K558      have restFinite := Finite.subset with finiteC, restSubset559      have restored : K △ (C ∖ K) = C by ext x; simp560      have evenWhole : EvenEdgeSet(V, leftEnd, rightEnd, K △ (C ∖ K))561        rw restored562        exact even563      have evenRest := EvenEdgeSet.of_symmetricDifference564        with cycle.right.left, restFinite, evenWhole565      have less : cardinality(C ∖ K) < cardinality(C)566        obtain ⟨a, ha⟩ := Nonempty.of_ne_empty with cycle.left567        have outside : ¬a ∈ C ∖ K by simp [ha]568        exact cardinality.strict with finiteC, restSubset, (inC with a, ha),569          outside570      have smallerSize : cardinality(C ∖ K) ≤ k by arith571      obtain ⟨D, finiteD, cycles, apart, covers⟩ := ih with C ∖ K,572        (Subset.transitive with restSubset, bound), smallerSize, evenRest573      -- Adjoin K to the decomposition of the rest, which it misses.574      have inRest : ∀ B ∈ D, B ⊆ C ∖ K575        intros B hB576        rw ← covers577        exact union.subset_of_member with hB578      have apartK : ∀ B ∈ D, Disjoint(B, K)579        intros B hB580        exact Disjoint.of_subset_left with Disjoint.difference_left,581          (inRest with B, hB)582      refine ⟨D ∪ {K}, (Finite.union with finiteD, Finite.singleton),583        ?_, ?_, ?_⟩584      . intros B hB585        simp at hB586        rcases hB with inD | rfl587        . exact cycles with B, inD588        . exact cycle589      . intros B hB A hA different590        simp at hB, hA591        rcases hB with inD | rfl592        . rcases hA with inD2 | rfl593          . exact apart with B, inD, A, inD2, different594          . exact apartK with B, inD595        . rcases hA with inD2 | rfl596          . exact Disjoint.symmetric with (apartK with A, inD2)597          . exfalso598            exact different with rfl599      . rw [union.union2, union.singleton, covers]600        ext x601        have fromK : x ∈ K → x ∈ C := inC with x602        simp [difference.membership]603604theorem EvenEdgeSet.cycle_decomposition (V leftEnd rightEnd F : Set)605  requires finiteVertices : Finite(V)606  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V607  requires even : EvenEdgeSet(V, leftEnd, rightEnd, F)608  shows ∃ D, Finite(D) ∧ (∀ C ∈ D, Cycle(V, leftEnd, rightEnd, C)) ∧609    (∀ C ∈ D, ∀ B ∈ D, C ≠ B → Disjoint(C, B)) ∧ ⋃(D) = F610proof611  have finite := even.left612  have bound : cardinality(F) ≤ cardinality(F) by arith613  exact EvenEdgeSet.decomposition_of_size614    at V, leftEnd, rightEnd, F, cardinality(F)615    with finiteVertices, ends, F, Subset.reflexive, bound, even616