-- The dual obstruction computation: a left-kernel vector of the
-- compatibility system gives at each edge a vector orthogonal to its value,
-- the odd ends regroup over the vertices into an even set, and so no
-- left-kernel vector sees an odd right-hand side.
-- 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.DoubleCover.Obstruction
import CompatibilitySystem

-- Parity of a subset of 3 through its three membership bits.
theorem EvenSet.three_bits (X Y : Set)
  requires inside : X ⊆ 3
  shows EvenSet(X ∩ Y) ↔
    (((0 ∈ X ∧ 0 ∈ Y) ↔ (1 ∈ X ∧ 1 ∈ Y)) ↔ ¬(2 ∈ X ∧ 2 ∈ Y))
proof
  have apart : 0 ≠ 1 ∧ 1 ≠ 2 ∧ 0 ≠ 2 by simp
  have cover : X ∩ Y ⊆ ({0} ∪ {1}) ∪ {2}
    intros z hz
    have hz3 := inside with z, hz.left
    rw membership.three at hz3
    simp
  rw EvenSet.of_three with apart, cover
  simp [intersection.membership]

theorem subset_three.empty_iff (X : Set)
  requires inside : X ⊆ 3
  shows X = ∅ ↔ (¬0 ∈ X ∧ ¬1 ∈ X ∧ ¬2 ∈ X)
proof
  constructor
  . intro empty
    rw empty
    simp
  . intro bits
    ext z
    constructor
    . intro hz
      have hz3 := inside with z, hz
      rw membership.three at hz3
      exfalso
      rcases hz3 with rfl | rfl | rfl
      . exact bits.left with hz
      . exact bits.right.left with hz
      . exact bits.right.right with hz
    . intro hz
      simp at hz

theorem subset_three.eq_iff (X Y : Set)
  requires insideX : X ⊆ 3
  requires insideY : Y ⊆ 3
  shows X = Y ↔ ((0 ∈ X ↔ 0 ∈ Y) ∧ (1 ∈ X ↔ 1 ∈ Y) ∧ (2 ∈ X ↔ 2 ∈ Y))
proof
  constructor
  . intro same
    rw same
    tauto
  . intro bits
    ext z
    by_cases hz : z ∈ 3
    . rw membership.three at hz
      rcases hz with rfl | rfl | rfl
      . exact bits.left
      . exact bits.right.left
      . exact bits.right.right
    . have notX : ¬z ∈ X
        intro h
        exact hz with (insideX with z, h)
      have notY : ¬z ∈ Y
        intro h
        exact hz with (insideY with z, h)
      tauto

-- The vertex computation of the paper, in the two-element field with three
-- coordinates: at a vertex the three vectors h(e), h(f), h(g) = h(e) △ h(f)
-- are each orthogonal to the matching value, and the values are nonzero and
-- distinct with value(g) = value(e) △ value(f). Then h(e) · value(f) is odd
-- exactly when an odd number of the three h are nonzero.
theorem vertex.parity (he hf hg ve vf vg : Set)
  requires insideE : he ⊆ 3
  requires insideF : hf ⊆ 3
  requires valueE : ve ⊆ 3
  requires valueF : vf ⊆ 3
  requires sumH : hg = he △ hf
  requires sumV : vg = ve △ vf
  requires nonzeroE : ve ≠ ∅
  requires nonzeroF : vf ≠ ∅
  requires distinct : ve ≠ vf
  requires orthogonalE : EvenSet(he ∩ ve)
  requires orthogonalF : EvenSet(hf ∩ vf)
  requires orthogonalG : EvenSet(hg ∩ vg)
  shows EvenSet(he ∩ vf) ↔ ((he ≠ ∅ ↔ hf ≠ ∅) ↔ hg = ∅)
proof
  have insideG : hg ⊆ 3
    rw sumH
    exact symmetricDifference.subset with insideE, insideF
  have bitsG : ∀ i, (i ∈ hg ↔ ¬(i ∈ he ↔ i ∈ hf))
    intro i
    rw sumH
    exact symmetricDifference.membership
  have bitsV : ∀ i, (i ∈ vg ↔ ¬(i ∈ ve ↔ i ∈ vf))
    intro i
    rw sumV
    exact symmetricDifference.membership
  have g0 := bitsG with 0
  have g1 := bitsG with 1
  have g2 := bitsG with 2
  have v0 := bitsV with 0
  have v1 := bitsV with 1
  have v2 := bitsV with 2
  rw EvenSet.three_bits with insideE at orthogonalE
  rw EvenSet.three_bits with insideF at orthogonalF
  rw EvenSet.three_bits with insideG at orthogonalG
  rw EvenSet.three_bits with insideE
  rw subset_three.empty_iff with valueE at nonzeroE
  rw subset_three.empty_iff with valueF at nonzeroF
  rw subset_three.eq_iff with valueE, valueF at distinct
  rw [subset_three.empty_iff with insideE, subset_three.empty_iff with insideF,
    subset_three.empty_iff with insideG]
  tauto

-- The vector h(e) of a left-kernel vector y at the edge e.
def rowSet (y e : Set) : Set := { i ∈ 3 | (e, i) ∈ y }

theorem rowSet.subset (y e : Set)
  shows rowSet(y, e) ⊆ 3
proof
  intros i hi
  exact hi.left

theorem rowSet.finite (y e : Set)
  shows Finite(rowSet(y, e))
proof
  exact Finite.subset with Finite.natural, rowSet.subset

-- The switch column of e: y meets it in {e} × (h(e) ∩ value(e)), so h(e) is
-- orthogonal to value(e).
theorem Obstructs.switch (V E leftEnd rightEnd F d y e : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires edge : e ∈ E
  requires obstruction : Obstructs(
    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,
    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)
  shows EvenSet(rowSet(y, e) ∩ flowValue(F, e))
proof
  have column : (e, 3) ∈ (V × 3) ∪ (E × {3})
    by simp [product.pair_membership, edge]
  have even := obstruction.right.left with (e, 3), column
  have finite : Finite(rowSet(y, e) ∩ flowValue(F, e)) :=
    Finite.subset with rowSet.finite, intersection.subset_left
  have block : cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
      E × 3, (e, 3)) ∩ y = {e} × (rowSet(y, e) ∩ flowValue(F, e))
    ext p
    constructor
    . intro hp
      obtain ⟨⟨row, entry⟩, hy⟩ := hp
      obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with row
      rw compatibilityMatrix.row with graph, hx, hj at entry
      have tag := membership.three.ne with hj
      rcases entry with h | h | h
      . exfalso
        have parts := orderedPair.injective with h
        apply tag
        cc
      . exfalso
        have parts := orderedPair.injective with h
        apply tag
        cc
      . have parts := orderedPair.injective with h.right
        have xe : x = e by cc
        rw xe at hy, h
        rw xe
        have inRow : j ∈ rowSet(y, e) ∩ flowValue(F, e) := ⟨⟨hj, hy⟩, h.left⟩
        exact product.pair with singleton.self, inRow
    . intro hp
      obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with hp
      have xe := singleton.membership.forward with hx
      rw xe
      obtain ⟨⟨hj3, hy⟩, value⟩ := hj
      have entry : ((e, j), (e, 3)) ∈
          compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=
        compatibilityMatrix.switch.backward with graph, edge, hj3, value
      exact ⟨⟨(product.pair with edge, hj3), entry⟩, hy⟩
  rw block at even
  unfold EvenSet at even
  rw cardinality.singleton_product with finite at even
  exact even

-- A vertex column (v, i) at the vertex v with edges e, f, g: y meets it in
-- the rows (e, i), (f, i), (g, i) it holds, so h(g) = h(e) △ h(f) at v.
theorem Obstructs.vertex (V E leftEnd rightEnd F d y v e f g i : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires vertex : v ∈ V
  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E
  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
    (leftEnd(g) = v ∨ rightEnd(g) = v)
  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g
  requires coordinate : i ∈ 3
  requires obstruction : Obstructs(
    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,
    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)
  shows i ∈ rowSet(y, g) ↔ ¬(i ∈ rowSet(y, e) ↔ i ∈ rowSet(y, f))
proof
  have column : (v, i) ∈ (V × 3) ∪ (E × {3})
    by simp [product.pair_membership, vertex, coordinate]
  have even := obstruction.right.left with (v, i), column
  have apartEF : (e, i) ≠ (f, i)
    intro same
    exact distinct.left with (orderedPair.injective with same).left
  have apartFG : (f, i) ≠ (g, i)
    intro same
    exact distinct.right.left with (orderedPair.injective with same).left
  have apartEG : (e, i) ≠ (g, i)
    intro same
    exact distinct.right.right with (orderedPair.injective with same).left
  have apart : (e, i) ≠ (f, i) ∧ (f, i) ≠ (g, i) ∧ (e, i) ≠ (g, i) :=
    ⟨apartEF, apartFG, apartEG⟩
  have tag := membership.three.ne with coordinate
  -- A row meeting the column (v, i) is (x, i) for an edge x at v, hence one
  -- of e, f, g.
  have inside : cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
      E × 3, (v, i)) ∩ y ⊆ ({(e, i)} ∪ {(f, i)}) ∪ {(g, i)}
    intros p hp
    obtain ⟨⟨row, entry⟩, _⟩ := hp
    obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with row
    rw compatibilityMatrix.row with graph, hx, hj at entry
    have located : (leftEnd(x) = v ∨ rightEnd(x) = v) ∧ j = i
      rcases entry with h | h | h
      . have parts := orderedPair.injective with h
        constructor
        . left
          cc
        . cc
      . have parts := orderedPair.injective with h
        constructor
        . right
          cc
        . cc
      . exfalso
        have parts := orderedPair.injective with h.right
        apply tag
        cc
    have cases := Cubic.among
      with cubic, vertex, edges, incident, distinct, hx, located.left
    rw located.right
    simp
  rw EvenSet.of_three with apart, inside at even
  have entryE : ((e, i), (v, i)) ∈
      compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=
    compatibilityMatrix.end with graph, edges.left, coordinate, incident.left
  have entryF : ((f, i), (v, i)) ∈
      compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=
    compatibilityMatrix.end
      with graph, edges.right.left, coordinate, incident.right.left
  have entryG : ((g, i), (v, i)) ∈
      compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=
    compatibilityMatrix.end
      with graph, edges.right.right, coordinate, incident.right.right
  have memberE : (e, i) ∈
      cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
        E × 3, (v, i)) ∩ y ↔ (e, i) ∈ y
    constructor
    . intro hp
      exact hp.right
    . intro hy
      exact ⟨⟨(product.pair with edges.left, coordinate), entryE⟩, hy⟩
  have memberF : (f, i) ∈
      cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
        E × 3, (v, i)) ∩ y ↔ (f, i) ∈ y
    constructor
    . intro hp
      exact hp.right
    . intro hy
      exact ⟨⟨(product.pair with edges.right.left, coordinate), entryF⟩, hy⟩
  have memberG : (g, i) ∈
      cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
        E × 3, (v, i)) ∩ y ↔ (g, i) ∈ y
    constructor
    . intro hp
      exact hp.right
    . intro hy
      exact ⟨⟨(product.pair with edges.right.right, coordinate), entryG⟩, hy⟩
  rw [memberE, memberF, memberG] at even
  unfold rowSet
  tauto

-- Parity of a set partitioned by a finite index: the members of S covered
-- by the indices of G, through a relation P pairing indices with members.
def covered (P S G : Set) : Set := { x ∈ S | ∃ i ∈ G, (i, x) ∈ P }

theorem covered.subset (P S G : Set)
  shows covered(P, S, G) ⊆ S
proof
  intros x hx
  exact hx.left

theorem covered.empty (P S : Set)
  shows covered(P, S, ∅) = ∅
proof
  ext x
  simp [covered.membership]

theorem covered.insert (P S G a : Set)
  shows covered(P, S, G ∪ {a}) = covered(P, S, G) ∪ fiber(P, S, a)
proof
  ext x
  have split : x ∈ covered(P, S, G) ∪ fiber(P, S, a) ↔
      (x ∈ covered(P, S, G) ∨ x ∈ fiber(P, S, a))
    by simp
  rw split
  constructor
  . intro hx
    obtain ⟨hs, i, hi, related⟩ := hx
    simp at hi
    rcases hi with inG | same
    . left
      exact ⟨hs, i, inG, related⟩
    . right
      rw same at related
      exact ⟨hs, related⟩
  . intro hx
    rcases hx with inG | inA
    . obtain ⟨hs, i, hi, related⟩ := inG
      have hi2 : i ∈ G ∪ {a} by simp [hi]
      exact ⟨hs, i, hi2, related⟩
    . have ha : a ∈ G ∪ {a} by simp
      exact ⟨inA.left, a, ha, inA.right⟩

-- When every member has one index, the part of a fresh index is disjoint
-- from the members covered so far.
theorem covered.disjoint (I P S G a : Set)
  requires unique : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ P → (j, x) ∈ P → i = j
  requires inside : G ⊆ I
  requires member : a ∈ I
  requires fresh : ¬a ∈ G
  shows Disjoint(covered(P, S, G), fiber(P, S, a))
proof
  apply Disjoint.iff.backward
  intros x hx hx2
  obtain ⟨_, i, hi, related⟩ := hx
  have same := unique with i, (inside with i, hi), a, member, x, related,
    hx2.right
  rw same at hi
  exact fresh with hi

theorem covered.parity (I S T P Q : Set)
  requires finiteIndex : Finite(I)
  requires finiteS : Finite(S)
  requires finiteT : Finite(T)
  requires uniqueP : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ P → (j, x) ∈ P → i = j
  requires uniqueQ : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ Q → (j, x) ∈ Q → i = j
  requires parts : ∀ i ∈ I, (EvenSet(fiber(P, S, i)) ↔ EvenSet(fiber(Q, T, i)))
  shows EvenSet(covered(P, S, I)) ↔ EvenSet(covered(Q, T, I))
proof
  induction finiteIndex with G a
  | empty =>
    rw [covered.empty, covered.empty]
  | insert using ih =>
    rw [covered.insert, covered.insert]
    have finiteGS : Finite(covered(P, S, G)) :=
      Finite.subset with finiteS, covered.subset
    have finiteGT : Finite(covered(Q, T, G)) :=
      Finite.subset with finiteT, covered.subset
    have finiteAS : Finite(fiber(P, S, a)) := fiber.finite with finiteS
    have finiteAT : Finite(fiber(Q, T, a)) := fiber.finite with finiteT
    have apartS := covered.disjoint at _, _, S, _, _
      with uniqueP, GSubset, aMember, aFresh
    have apartT := covered.disjoint at _, _, T, _, _
      with uniqueQ, GSubset, aMember, aFresh
    rw [(EvenSet.union_disjoint with finiteGS, finiteAS, apartS),
      (EvenSet.union_disjoint with finiteGT, finiteAT, apartT)]
    have part := parts with a, aMember
    tauto

-- Two finite sets partitioned by the same finite index set, with parts of
-- equal parity index by index, have the same parity.
theorem EvenSet.of_parts (I S T P Q : Set)
  requires finiteIndex : Finite(I)
  requires finiteS : Finite(S)
  requires finiteT : Finite(T)
  requires coverS : ∀ x ∈ S, ∃ i ∈ I, (i, x) ∈ P
  requires coverT : ∀ x ∈ T, ∃ i ∈ I, (i, x) ∈ Q
  requires uniqueP : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ P → (j, x) ∈ P → i = j
  requires uniqueQ : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ Q → (j, x) ∈ Q → i = j
  requires parts : ∀ i ∈ I, (EvenSet(fiber(P, S, i)) ↔ EvenSet(fiber(Q, T, i)))
  shows EvenSet(S) ↔ EvenSet(T)
proof
  have wholeS : covered(P, S, I) = S
    ext x
    constructor
    . intro hx
      exact hx.left
    . intro hx
      exact ⟨hx, (coverS with x, hx)⟩
  have wholeT : covered(Q, T, I) = T
    ext x
    constructor
    . intro hx
      exact hx.left
    . intro hx
      exact ⟨hx, (coverT with x, hx)⟩
  rw [← wholeS, ← wholeT]
  exact covered.parity
    with finiteIndex, finiteS, finiteT, uniqueP, uniqueQ, parts

-- The two index relations: a pair of I × X indexed by its first entry, and
-- an end indexed by its vertex.
def byFirst (I X : Set) : Set := { q ∈ I × X | fst(snd(q)) = fst(q) }

def atVertex (V E leftEnd rightEnd : Set) : Set :=
  { q ∈ V × (E × 2) | snd(q) ∈ incidentEnds(leftEnd, rightEnd, E, fst(q)) }

theorem byFirst.pair (I X i x : Set)
  shows (i, x) ∈ byFirst(I, X) ↔ (i ∈ I ∧ x ∈ X ∧ fst(x) = i)
proof
  simp [byFirst.membership, product.pair_membership, fst.pair, snd.pair]

-- A pair (e, j) of E × X is indexed by e.
theorem byFirst.of_pair (E X e j : Set)
  requires edge : e ∈ E
  requires member : (e, j) ∈ E × X
  shows (e, (e, j)) ∈ byFirst(E, E × X)
proof
  rw byFirst.pair
  exact ⟨edge, member, fst.pair⟩

theorem atVertex.pair (V E leftEnd rightEnd v p : Set)
  shows (v, p) ∈ atVertex(V, E, leftEnd, rightEnd) ↔
    (v ∈ V ∧ p ∈ E × 2 ∧ p ∈ incidentEnds(leftEnd, rightEnd, E, v))
proof
  simp [atVertex.membership, product.pair_membership, fst.pair, snd.pair]

theorem byFirst.unique (I X : Set)
  shows ∀ i ∈ I, ∀ j ∈ I, ∀ x,
    (i, x) ∈ byFirst(I, X) → (j, x) ∈ byFirst(I, X) → i = j
proof
  intros i hi j hj x hix hjx
  rw byFirst.pair at hix, hjx
  cc

-- Every pair of E × X is indexed by an edge.
theorem byFirst.cover (E X p : Set)
  requires member : p ∈ E × X
  shows ∃ e ∈ E, (e, p) ∈ byFirst(E, E × X)
proof
  obtain ⟨_, e, he, j, hj, rfl⟩ := product.membership.forward with member
  exact ⟨e, he, (byFirst.of_pair with he, member)⟩

-- An end lies at one vertex.
theorem incidentEnds.vertex_unique (leftEnd rightEnd E v w p : Set)
  requires first : p ∈ incidentEnds(leftEnd, rightEnd, E, v)
  requires second : p ∈ incidentEnds(leftEnd, rightEnd, E, w)
  shows v = w
proof
  obtain ⟨e, he, j, hj, rfl⟩ := incidentEnds.shape with first
  have sidesV := (incidentEnds.pair.forward with first).right
  have sidesW := (incidentEnds.pair.forward with second).right
  have apart : 0 ≠ 1 by simp
  rcases sidesV with ⟨h0, atL⟩ | ⟨h1, atR⟩
  . rcases sidesW with ⟨_, atL2⟩ | ⟨h1, _⟩
    . cc
    . exfalso
      apply apart
      cc
  . rcases sidesW with ⟨h0, _⟩ | ⟨_, atR2⟩
    . exfalso
      apply apart
      cc
    . cc

theorem atVertex.unique (V E leftEnd rightEnd : Set)
  shows ∀ v ∈ V, ∀ w ∈ V, ∀ p, (v, p) ∈ atVertex(V, E, leftEnd, rightEnd) →
    (w, p) ∈ atVertex(V, E, leftEnd, rightEnd) → v = w
proof
  intros v hv w hw p hvp hwp
  rw atVertex.pair at hvp, hwp
  exact incidentEnds.vertex_unique with hvp.right.right, hwp.right.right

-- Every end of E lies at a vertex of V.
theorem atVertex.cover (V E leftEnd rightEnd p : Set)
  requires ends : ∀ e ∈ E, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V
  requires member : p ∈ E × 2
  shows ∃ v ∈ V, (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)
proof
  obtain ⟨_, e, he, j, hj, rfl⟩ := product.membership.forward with member
  obtain ⟨vertexL, vertexR⟩ := ends with e, he
  have cases := membership.two.forward with hj
  rcases cases with rfl | rfl
  . refine ⟨leftEnd(e), vertexL, ?_⟩
    rw atVertex.pair
    refine ⟨vertexL, member, ?_⟩
    simp [incidentEnds.pair, he]
  . refine ⟨rightEnd(e), vertexR, ?_⟩
    rw atVertex.pair
    refine ⟨vertexR, member, ?_⟩
    simp [incidentEnds.pair, he]

-- The part of a set of pairs at the index v, through atVertex, is its
-- intersection with the ends at v.
theorem atVertex.fiber (V E leftEnd rightEnd S v : Set)
  requires vertex : v ∈ V
  requires pairs : S ⊆ E × 2
  shows fiber(atVertex(V, E, leftEnd, rightEnd), S, v) =
    S ∩ incidentEnds(leftEnd, rightEnd, E, v)
proof
  ext p
  constructor
  . intro hp
    have related := hp.right
    rw atVertex.pair at related
    exact ⟨hp.left, related.right.right⟩
  . intro hp
    have related : (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)
      rw atVertex.pair
      exact ⟨vertex, (pairs with p, hp.left), hp.right⟩
    exact ⟨hp.left, related⟩

-- Parity of a subset of a two-element set, and of an intersection with a
-- symmetric difference.
theorem EvenSet.of_two (S a b : Set)
  requires apart : a ≠ b
  requires inside : S ⊆ {a} ∪ {b}
  shows EvenSet(S) ↔ (¬a ∈ S ↔ ¬b ∈ S)
proof
  have whole : S ∩ ({a} ∪ {b}) = S := intersection.eq_left_of_subset with inside
  have freshB : ¬b ∈ {a} by simp
  have stepB := EvenSet.intersection_union_part
    at S, {a}, {b}, b with Finite.singleton, Subset.reflexive, freshB
  have stepA : EvenSet(S ∩ {a}) ↔ ¬a ∈ S
    rw intersection.commutative
    exact EvenSet.singleton_intersection
  rw whole at stepB
  rw [stepB, stepA]
  simp

theorem EvenSet.intersection_symmetricDifference (X A B : Set)
  requires finiteX : Finite(X)
  requires finiteA : Finite(A)
  requires finiteB : Finite(B)
  shows EvenSet(X ∩ (A △ B)) ↔ (EvenSet(X ∩ A) ↔ EvenSet(X ∩ B))
proof
  have step := dot.symmetricDifference with finiteA, finiteB, finiteX
  unfold dot at step
  unfold EvenSet
  rw [intersection.commutative, (intersection.commutative at X, A),
    (intersection.commutative at X, B)]
  exact step

-- The ends whose edge has a nonzero vector h, the vertices at which an odd
-- number of them meet, and the ends at those vertices.
def nonzeroEnds (E y : Set) : Set := { p ∈ E × 2 | rowSet(y, fst(p)) ≠ ∅ }

predicate OddVertex (E leftEnd rightEnd y v : Set) :=
  ¬EvenSet(nonzeroEnds(E, y) ∩ incidentEnds(leftEnd, rightEnd, E, v))

def oddEnds (V E leftEnd rightEnd y : Set) : Set :=
  { p ∈ E × 2 | ∃ v ∈ V, p ∈ incidentEnds(leftEnd, rightEnd, E, v) ∧
    OddVertex(E, leftEnd, rightEnd, y, v) }

theorem nonzeroEnds.subset (E y : Set)
  shows nonzeroEnds(E, y) ⊆ E × 2
proof
  intros p hp
  exact hp.left

theorem oddEnds.subset (V E leftEnd rightEnd y : Set)
  shows oddEnds(V, E, leftEnd, rightEnd, y) ⊆ E × 2
proof
  intros p hp
  exact hp.left

-- At a cubic vertex with edges e, f, g the parity of the nonzero ends is
-- read off the three vectors.
theorem OddVertex.of_three (V E leftEnd rightEnd y v e f g : Set)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires vertex : v ∈ V
  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E
  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
    (leftEnd(g) = v ∨ rightEnd(g) = v)
  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g
  shows OddVertex(E, leftEnd, rightEnd, y, v) ↔
    ¬((¬rowSet(y, e) ≠ ∅ ↔ ¬rowSet(y, f) ≠ ∅) ↔ ¬rowSet(y, g) ≠ ∅)
proof
  obtain ⟨i, hi, j, hj, k, hk, apart, shape⟩ :=
    Cubic.ends_of_three with cubic, vertex, edges, incident, distinct
  have endE : (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp
  have endF : (f, j) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp
  have endG : (g, k) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp
  have pairE : (e, i) ∈ E × 2 := product.pair with edges.left, hi
  have pairF : (f, j) ∈ E × 2 := product.pair with edges.right.left, hj
  have pairG : (g, k) ∈ E × 2 := product.pair with edges.right.right, hk
  have inside : nonzeroEnds(E, y) ∩ incidentEnds(leftEnd, rightEnd, E, v) ⊆
      ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}
    rw ← shape
    intros p hp
    exact hp.right
  unfold OddVertex
  rw EvenSet.of_three with apart, inside
  simp [nonzeroEnds.membership, intersection.membership, pairE, pairF, pairG,
    endE, endF, endG, fst.pair]

-- The vertex computation for an obstruction: at v with the distinct edges
-- e, x, z, the vector of e is orthogonal to the value of x exactly when an
-- even number of the three vectors are nonzero.
theorem Obstructs.triple_parity (V E leftEnd rightEnd F d y v e x z : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)
  requires vertex : v ∈ V
  requires edges : e ∈ E ∧ x ∈ E ∧ z ∈ E
  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
    (leftEnd(x) = v ∨ rightEnd(x) = v) ∧
    (leftEnd(z) = v ∨ rightEnd(z) = v)
  requires distinct : e ≠ x ∧ x ≠ z ∧ e ≠ z
  requires obstruction : Obstructs(
    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,
    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)
  shows EvenSet(rowSet(y, e) ∩ flowValue(F, x)) ↔
    ¬OddVertex(E, leftEnd, rightEnd, y, v)
proof
  -- The three vectors sum to zero at v, and so do the three values.
  have sumH : rowSet(y, z) = rowSet(y, e) △ rowSet(y, x)
    ext i
    rw symmetricDifference.membership
    by_cases hi : i ∈ 3
    . exact Obstructs.vertex
        with graph, cubic, vertex, edges, incident, distinct, hi, obstruction
    . simp [rowSet, hi]
  have triple := flowValue.cubic_vertex
    with graph, cubic, cover, vertex, edges, incident, distinct
  have nonzeroE := flowValue.nonzero with cover, edges.left
  have nonzeroX := flowValue.nonzero with cover, edges.right.left
  have orthogonalE := Obstructs.switch with graph, edges.left, obstruction
  have orthogonalX :=
    Obstructs.switch with graph, edges.right.left, obstruction
  have orthogonalZ :=
    Obstructs.switch with graph, edges.right.right, obstruction
  have parity := vertex.parity
    at rowSet(y, e), rowSet(y, x), rowSet(y, z),
      flowValue(F, e), flowValue(F, x), flowValue(F, z)
    with rowSet.subset, rowSet.subset, flowValue.subset, flowValue.subset,
      sumH, triple.right, nonzeroE, nonzeroX, triple.left,
      orthogonalE, orthogonalX, orthogonalZ
  rw [parity,
    (OddVertex.of_three with cubic, vertex, edges, incident, distinct)]
  tauto

-- The same for any two distinct edges e, x at v.
theorem Obstructs.end_parity (V E leftEnd rightEnd F d y v e x : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)
  requires vertex : v ∈ V
  requires edge : e ∈ E
  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v
  requires other : x ∈ E ∧ x ≠ e ∧ (leftEnd(x) = v ∨ rightEnd(x) = v)
  requires obstruction : Obstructs(
    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,
    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)
  shows EvenSet(rowSet(y, e) ∩ flowValue(F, x)) ↔
    ¬OddVertex(E, leftEnd, rightEnd, y, v)
proof
  obtain ⟨f, hf, g, hg, distinct, atF, atG⟩ :=
    Cubic.others with cubic, vertex, edge, incident
  have edges : e ∈ E ∧ f ∈ E ∧ g ∈ E := ⟨edge, hf, hg⟩
  have incident3 : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
      (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
      (leftEnd(g) = v ∨ rightEnd(g) = v) :=
    ⟨incident, atF, atG⟩
  have cases := Cubic.among with cubic, vertex, edges, incident3, distinct,
    other.left, other.right.right
  rcases cases with same | same | same
  . exfalso
    exact other.right.left with same
  . rw same
    exact Obstructs.triple_parity with graph, cubic, cover, vertex, edges,
      incident3, distinct, obstruction
  . rw same
    have edgesG : e ∈ E ∧ g ∈ E ∧ f ∈ E := ⟨edge, hg, hf⟩
    have incidentG : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
        (leftEnd(g) = v ∨ rightEnd(g) = v) ∧
        (leftEnd(f) = v ∨ rightEnd(f) = v) :=
      ⟨incident, atG, atF⟩
    have gf : g ≠ f by cc
    have distinctG : e ≠ g ∧ g ≠ f ∧ e ≠ f :=
      ⟨distinct.right.right, gf, distinct.left⟩
    exact Obstructs.triple_parity with graph, cubic, cover, vertex, edgesG,
      incidentG, distinctG, obstruction

-- The parts of the odd ends and of the nonzero ends at a vertex v: all three
-- ends or none, and the nonzero ends at v.
theorem oddEnds.fiber (V E leftEnd rightEnd y v : Set)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires vertex : v ∈ V
  shows EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd),
      oddEnds(V, E, leftEnd, rightEnd, y), v)) ↔
    ¬OddVertex(E, leftEnd, rightEnd, y, v)
proof
  have pairs : oddEnds(V, E, leftEnd, rightEnd, y) ⊆ E × 2 := oddEnds.subset
  rw atVertex.fiber with vertex, pairs
  by_cases odd : OddVertex(E, leftEnd, rightEnd, y, v)
  . -- Every end at v is odd, and there are three of them.
    have whole : oddEnds(V, E, leftEnd, rightEnd, y) ∩
        incidentEnds(leftEnd, rightEnd, E, v) =
        incidentEnds(leftEnd, rightEnd, E, v)
      ext p
      constructor
      . intro hp
        exact hp.right
      . intro hp
        have product := incidentEnds.subset_product at leftEnd, rightEnd, E, v
        have pair : p ∈ E × 2 := product with p, hp
        exact ⟨⟨pair, v, vertex, hp, odd⟩, hp⟩
    rw whole
    obtain ⟨e, he, f, hf, g, hg, distinct, atE, atF, atG⟩ :=
      Cubic.ends_at with cubic, vertex
    have edges : e ∈ E ∧ f ∈ E ∧ g ∈ E := ⟨he, hf, hg⟩
    have incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧
        (leftEnd(f) = v ∨ rightEnd(f) = v) ∧
        (leftEnd(g) = v ∨ rightEnd(g) = v) :=
      ⟨atE, atF, atG⟩
    obtain ⟨i, hi, j, hj, k, hk, apart, shape⟩ :=
      Cubic.ends_of_three with cubic, vertex, edges, incident, distinct
    have inside : incidentEnds(leftEnd, rightEnd, E, v) ⊆
        ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}
      rw shape
      exact Subset.reflexive
    rw [(EvenSet.of_three with apart, inside), shape]
    simp [odd]
  . -- No end at v is odd.
    have none : oddEnds(V, E, leftEnd, rightEnd, y) ∩
        incidentEnds(leftEnd, rightEnd, E, v) = ∅
      ext p
      constructor
      . intro hp
        obtain ⟨⟨_, w, hw, atW, oddW⟩, atV⟩ := hp
        have same := incidentEnds.vertex_unique with atV, atW
        rw same at odd
        exfalso
        exact odd with oddW
      . intro hp
        simp at hp
    rw none
    simp [EvenSet.empty, odd]

theorem nonzeroEnds.fiber (V E leftEnd rightEnd y v : Set)
  requires vertex : v ∈ V
  shows EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd), nonzeroEnds(E, y), v))
    ↔ ¬OddVertex(E, leftEnd, rightEnd, y, v)
proof
  have pairs : nonzeroEnds(E, y) ⊆ E × 2 := nonzeroEnds.subset
  rw atVertex.fiber with vertex, pairs
  unfold OddVertex
  tauto

-- The nonzero ends are even in number: each edge contributes both its ends
-- or neither.
theorem nonzeroEnds.even (E y : Set)
  requires finiteEdges : Finite(E)
  shows EvenSet(nonzeroEnds(E, y))
proof
  have finiteEnds : Finite(E × 2) :=
    Finite.product with finiteEdges, Finite.natural
  have finite : Finite(nonzeroEnds(E, y)) :=
    Finite.subset with finiteEnds, nonzeroEnds.subset
  have cover : ∀ p ∈ nonzeroEnds(E, y), ∃ e ∈ E, (e, p) ∈ byFirst(E, E × 2)
    intros p hp
    exact byFirst.cover with hp.left
  have coverEmpty : ∀ p ∈ ∅, ∃ e ∈ E, (e, p) ∈ byFirst(E, ∅)
    intros p hp
    simp at hp
  -- The part at e is both ends of e or neither.
  have parts : ∀ e ∈ E,
      (EvenSet(fiber(byFirst(E, E × 2), nonzeroEnds(E, y), e)) ↔
        EvenSet(fiber(byFirst(E, ∅), ∅, e)))
    intros e he
    have empty : fiber(byFirst(E, ∅), ∅, e) = ∅
      ext p
      constructor
      . intro hp
        exact hp.left
      . intro hp
        simp at hp
    rw empty
    simp [EvenSet.empty]
    by_cases nonzero : rowSet(y, e) ≠ ∅
    . have whole : fiber(byFirst(E, E × 2), nonzeroEnds(E, y), e) = {e} × 2
        ext p
        constructor
        . intro hp
          have related := hp.right
          rw byFirst.pair at related
          obtain ⟨_, x, hx, j, hj, rfl⟩ :=
            product.membership.forward with hp.left.left
          rw fst.pair at related
          rw related.right.right
          exact product.pair with singleton.self, hj
        . intro hp
          obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with hp
          have xe := singleton.membership.forward with hx
          rw xe
          have pair : (e, j) ∈ E × 2 := product.pair with he, hj
          have member : (e, j) ∈ nonzeroEnds(E, y)
            apply nonzeroEnds.membership.backward
            rw fst.pair
            exact ⟨pair, nonzero⟩
          exact ⟨member, (byFirst.of_pair with he, pair)⟩
      rw whole
      unfold EvenSet
      rw [(cardinality.singleton_product with (Finite.natural at 2)),
        (cardinality.natural at 2)]
      exact Even.two
    . have none : fiber(byFirst(E, E × 2), nonzeroEnds(E, y), e) = ∅
        ext p
        constructor
        . intro hp
          have related := hp.right
          rw byFirst.pair at related
          have value := hp.left.right
          rw related.right.right at value
          exfalso
          exact nonzero with value
        . intro hp
          simp at hp
      rw none
      exact EvenSet.empty
  have step := EvenSet.of_parts
    at E, nonzeroEnds(E, y), ∅, byFirst(E, E × 2), byFirst(E, ∅)
    with finiteEdges, finite, Finite.empty, cover, coverEmpty,
      byFirst.unique, byFirst.unique, parts
  rw step
  exact EvenSet.empty

-- At an edge e: the part of y ∩ side is {e} × (h(e) ∩ d(e)), whose parity
-- is h(e)·a + h(e)·b for base points a, b at the two ends of e; the part of
-- the odd ends holds the ends of e at odd vertices. Both parities agree.
theorem Obstructs.edge_parity (V E leftEnd rightEnd F d y e : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)
  requires base : FunctionBetween(d, E, 𝒫(3)) ∧ (∀ e ∈ E, ∃ a, ∃ b,
    BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧
    BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧ d(e) = a △ b)
  requires obstruction : Obstructs(
    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,
    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)
  requires edge : e ∈ E
  shows EvenSet(fiber(byFirst(E, E × 3), y ∩ compatibilitySide(E, d), e)) ↔
    EvenSet(fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e))
proof
  have ends := Graph.ends with graph
  obtain ⟨vertexL, vertexR⟩ := ends with e, edge
  have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp
  have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp
  -- The part of y ∩ side at e.
  have left : fiber(byFirst(E, E × 3), y ∩ compatibilitySide(E, d), e) =
      {e} × (rowSet(y, e) ∩ d(e))
    ext p
    constructor
    . intro hp
      obtain ⟨⟨hy, hside⟩, related⟩ := hp
      rw byFirst.pair at related
      obtain ⟨_, x, hx, i, hi, rfl⟩ :=
        product.membership.forward with related.right.left
      rw fst.pair at related
      have xe := related.right.right
      rw xe at hy, hside
      rw xe
      rw compatibilitySide.pair with edge, hi at hside
      have inRow : i ∈ rowSet(y, e) ∩ d(e) := ⟨⟨hi, hy⟩, hside⟩
      exact product.pair with singleton.self, inRow
    . intro hp
      obtain ⟨_, x, hx, i, hi, rfl⟩ := product.membership.forward with hp
      have xe := singleton.membership.forward with hx
      rw xe
      obtain ⟨⟨hi3, hy⟩, value⟩ := hi
      have hside : (e, i) ∈ compatibilitySide(E, d)
        rw compatibilitySide.pair with edge, hi3
        exact value
      have pair : (e, i) ∈ E × 3 := product.pair with edge, hi3
      exact ⟨⟨hy, hside⟩, (byFirst.of_pair with edge, pair)⟩
  have finiteRow : Finite(rowSet(y, e) ∩ d(e)) :=
    Finite.subset with rowSet.finite, intersection.subset_left
  have leftParity : EvenSet({e} × (rowSet(y, e) ∩ d(e))) ↔
      EvenSet(rowSet(y, e) ∩ d(e))
    unfold EvenSet
    rw cardinality.singleton_product with finiteRow
  rw [left, leftParity]
  -- d(e) is the sum of base points a = value(x) at the left end and
  -- b = value(z) at the right end.
  obtain ⟨a, b, baseA, baseB, sumD⟩ := base.right with e, edge
  obtain ⟨x, hx, xe, xv, rfl⟩ := baseA
  obtain ⟨z, hz, ze, zv, rfl⟩ := baseB
  rw sumD
  have finiteH := rowSet.finite at y, e
  have finiteX := flowValue.finite at F, x
  have finiteZ := flowValue.finite at F, z
  rw EvenSet.intersection_symmetricDifference with finiteH, finiteX, finiteZ
  have otherX : x ∈ E ∧ x ≠ e ∧
      (leftEnd(x) = leftEnd(e) ∨ rightEnd(x) = leftEnd(e)) := ⟨hx, xe, xv⟩
  have otherZ : z ∈ E ∧ z ≠ e ∧
      (leftEnd(z) = rightEnd(e) ∨ rightEnd(z) = rightEnd(e)) := ⟨hz, ze, zv⟩
  rw [(Obstructs.end_parity
      with graph, cubic, cover, vertexL, edge, atL, otherX, obstruction),
    (Obstructs.end_parity
      with graph, cubic, cover, vertexR, edge, atR, otherZ, obstruction)]
  -- The part of the odd ends at e: among (e, 0) and (e, 1).
  have apart : (e, 0) ≠ (e, 1)
    intro same
    have parts := orderedPair.injective with same
    have zeroOne : 0 ≠ 1 by simp
    exact zeroOne with parts.right
  have inside : fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e)
      ⊆ {(e, 0)} ∪ {(e, 1)}
    intros p hp
    have related := hp.right
    rw byFirst.pair at related
    obtain ⟨_, w, hw, j, hj, rfl⟩ :=
      product.membership.forward with related.right.left
    rw fst.pair at related
    have we := related.right.right
    have cases := membership.two.forward with hj
    rw we
    rcases cases with rfl | rfl
    . simp
    . simp
  rw EvenSet.of_two with apart, inside
  have end0 : (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, leftEnd(e))
    by simp [incidentEnds.pair, edge]
  have end1 : (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, rightEnd(e))
    by simp [incidentEnds.pair, edge]
  have zero : 0 ∈ 2 by simp [membership.two]
  have one : 1 ∈ 2 by simp [membership.two]
  have pair0 : (e, 0) ∈ E × 2 := product.pair with edge, zero
  have pair1 : (e, 1) ∈ E × 2 := product.pair with edge, one
  have member0 : (e, 0) ∈
      fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e) ↔
      OddVertex(E, leftEnd, rightEnd, y, leftEnd(e))
    constructor
    . intro hp
      obtain ⟨⟨_, w, hw, atW, oddW⟩, _⟩ := hp
      have same := incidentEnds.vertex_unique with atW, end0
      rw same at oddW
      exact oddW
    . intro odd
      exact ⟨⟨pair0, leftEnd(e), vertexL, end0, odd⟩,
        (byFirst.of_pair with edge, pair0)⟩
  have member1 : (e, 1) ∈
      fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e) ↔
      OddVertex(E, leftEnd, rightEnd, y, rightEnd(e))
    constructor
    . intro hp
      obtain ⟨⟨_, w, hw, atW, oddW⟩, _⟩ := hp
      have same := incidentEnds.vertex_unique with atW, end1
      rw same at oddW
      exact oddW
    . intro odd
      exact ⟨⟨pair1, rightEnd(e), vertexR, end1, odd⟩,
        (byFirst.of_pair with edge, pair1)⟩
  rw [member0, member1]
  tauto

-- The dual obstruction computation: a left-kernel vector y gives vectors
-- h(e) with h(g) = h(e) △ h(f) at each vertex and h(e) ⊥ value(e); then
-- h(e) · (base point at v) is odd exactly when v is an odd vertex, so y ∩
-- side has the parity of the odd ends, which regroup over the vertices into
-- the nonzero ends, an even set. So y · side is even and y does not obstruct.
theorem compatibility.unobstructed (V E leftEnd rightEnd F d : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires cubic : Cubic(V, E, leftEnd, rightEnd)
  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)
  requires base : FunctionBetween(d, E, 𝒫(3)) ∧ (∀ e ∈ E, ∃ a, ∃ b,
    BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧
    BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧ d(e) = a △ b)
  shows ¬(∃ y, Obstructs(compatibilityMatrix(V, E, leftEnd, rightEnd, F),
    E × 3, (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y))
proof
  intro obstructed
  obtain ⟨y, obstruction⟩ := obstructed
  have ends := Graph.ends with graph
  have rows := obstruction.left
  have finiteRows : Finite(E × 3) :=
    Finite.product with finiteEdges, Finite.natural
  have finiteEnds : Finite(E × 2) :=
    Finite.product with finiteEdges, Finite.natural
  have finiteSide : Finite(y ∩ compatibilitySide(E, d)) :=
    Finite.subset with (Finite.subset with finiteRows, rows),
      intersection.subset_left
  have finiteOdd : Finite(oddEnds(V, E, leftEnd, rightEnd, y)) :=
    Finite.subset with finiteEnds, oddEnds.subset
  have finiteNonzero : Finite(nonzeroEnds(E, y)) :=
    Finite.subset with finiteEnds, nonzeroEnds.subset
  -- Over the edges: y ∩ side has the parity of the odd ends.
  have coverSide : ∀ p ∈ y ∩ compatibilitySide(E, d), ∃ e ∈ E,
      (e, p) ∈ byFirst(E, E × 3)
    intros p hp
    exact byFirst.cover with (rows with p, hp.left)
  have coverOdd : ∀ p ∈ oddEnds(V, E, leftEnd, rightEnd, y), ∃ e ∈ E,
      (e, p) ∈ byFirst(E, E × 2)
    intros p hp
    exact byFirst.cover with hp.left
  have partsEdges : ∀ e ∈ E,
      (EvenSet(fiber(byFirst(E, E × 3), y ∩ compatibilitySide(E, d), e)) ↔
        EvenSet(fiber(byFirst(E, E × 2),
          oddEnds(V, E, leftEnd, rightEnd, y), e)))
    intros e he
    exact Obstructs.edge_parity
      with graph, cubic, cover, base, obstruction, he
  have stepEdges := EvenSet.of_parts
    at E, y ∩ compatibilitySide(E, d), oddEnds(V, E, leftEnd, rightEnd, y),
      byFirst(E, E × 3), byFirst(E, E × 2)
    with finiteEdges, finiteSide, finiteOdd, coverSide, coverOdd,
      byFirst.unique, byFirst.unique, partsEdges
  -- Over the vertices: the odd ends have the parity of the nonzero ends.
  have coverOddV : ∀ p ∈ oddEnds(V, E, leftEnd, rightEnd, y), ∃ v ∈ V,
      (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)
    intros p hp
    exact atVertex.cover with ends, hp.left
  have coverNonzeroV : ∀ p ∈ nonzeroEnds(E, y), ∃ v ∈ V,
      (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)
    intros p hp
    exact atVertex.cover with ends, hp.left
  have partsVertices : ∀ v ∈ V,
      (EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd),
        oddEnds(V, E, leftEnd, rightEnd, y), v)) ↔
      EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd), nonzeroEnds(E, y), v)))
    intros v hv
    rw [(oddEnds.fiber with cubic, hv), (nonzeroEnds.fiber with hv)]
  have stepVertices := EvenSet.of_parts
    at V, oddEnds(V, E, leftEnd, rightEnd, y), nonzeroEnds(E, y),
      atVertex(V, E, leftEnd, rightEnd), atVertex(V, E, leftEnd, rightEnd)
    with finiteVertices, finiteOdd, finiteNonzero, coverOddV, coverNonzeroV,
      atVertex.unique, atVertex.unique, partsVertices
  have even := nonzeroEnds.even at E, y with finiteEdges
  have evenOdd := stepVertices.backward with even
  have evenSide := stepEdges.backward with evenOdd
  exact obstruction.right.right with evenSide