CubicPathwidth.Alg.Proofs2.L4Connector

Source file CubicPathwidth/Alg/Proofs2/L4Connector.lean of the Lean project (how it is built).

Statements of the paper formalised here: Lemma A.33.

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.C3Connector

/-!
# L4: `ConnectorLemma10` (Lemma A.33, `lem:connector-linear`) for the port's connector order

Main theorem: `connectorLemma10 : ConnectorLemma10`.

Structure (all helpers in namespace `CubicPathwidth.Alg.L4`):
* counts of items inside a set (`cntIn`, strict monotonicity, additivity over
  separated lists);
* incidence lists `inc` of `connectorIncidence` (membership, total size bound);
* the DFS `connDfs` (completion, closure, connectivity of its members);
* the outer scan `connOuter` (components are closed, connected, pairwise disjoint,
  cover `Qs`);
* the greedy loop `connectorGreedy.loop` (completion, Perm, and the prefix count
  `p ≤ c(p) + 1` along the greedy order);
* the excess identity `connectorExcess = |C| - #items inside C`;
* the main induction over the sorted list of components (prefix sums of sorted
  excesses are at most `max 0 (total)`), and the Perm part.
-/

namespace CubicPathwidth.Alg
namespace L4

/-- Adjacency in the hypergraph with hyperedges `items`. -/
def Adj (items : List (List Nat)) (x y : Nat) : Prop := ∃ e ∈ items, x ∈ e ∧ y ∈ e

/-- Reachability in the hypergraph `items`. -/
def Reach (items : List (List Nat)) (x y : Nat) : Prop :=
  Relation.ReflTransGen (Adj items) x y

/-- Number of items contained in the set `L` (the count `c(j)` of Lemma A.33 (`lem:connector-linear`)). -/
def cntIn (items : List (List Nat)) (L : List Nat) : Nat :=
  items.countP fun e => subsetB e L

theorem subsetB_iff {S B : List Nat} : subsetB S B = true ↔ ∀ z ∈ S, z ∈ B := by
  simp [subsetB]

theorem cntIn_eq_filter (items : List (List Nat)) (L : List Nat) :
    cntIn items L = (items.filter fun e => subsetB e L).length := by
  unfold cntIn; rw [List.countP_eq_length_filter]

theorem cntIn_congr {items : List (List Nat)} {L L' : List Nat}
    (h : ∀ z, z ∈ L ↔ z ∈ L') : cntIn items L = cntIn items L' := by
  unfold cntIn
  apply List.countP_congr
  intro e _
  simp only [subsetB_iff]
  exact ⟨fun h' z hz => (h z).1 (h' z hz), fun h' z hz => (h z).2 (h' z hz)⟩

theorem cntIn_le_length (items : List (List Nat)) (L : List Nat) :
    cntIn items L ≤ items.length := List.countP_le_length

theorem cntIn_strict {items : List (List Nat)} {L L' e : List Nat}
    (hLL : ∀ z ∈ L, z ∈ L') (he : e ∈ items) (heL' : ∀ z ∈ e, z ∈ L')
    (heL : ¬ ∀ z ∈ e, z ∈ L) : cntIn items L < cntIn items L' := by
  rw [cntIn_eq_filter, cntIn_eq_filter]
  have hsub : List.Sublist (items.filter fun e => subsetB e L)
      (items.filter fun e => subsetB e L') :=
    List.monotone_filter_right items (fun a ha => by
      rw [subsetB_iff] at ha ⊢
      exact fun z hz => hLL z (ha z hz))
  have hmem : e ∈ items.filter fun e => subsetB e L' :=
    List.mem_filter.2 ⟨he, subsetB_iff.2 heL'⟩
  have hnot : e ∉ items.filter fun e => subsetB e L := by
    intro h
    rw [List.mem_filter] at h
    exact heL (subsetB_iff.1 h.2)
  refine lt_of_le_of_ne hsub.length_le (fun h => hnot ?_)
  rw [hsub.eq_of_length h]
  exact hmem

theorem countP_or_add {α : Type} (p q : α → Bool) : ∀ l : List α,
    (∀ x ∈ l, p x = true → q x = false) →
      l.countP (fun x => p x || q x) = l.countP p + l.countP q
  | [], _ => by simp
  | a :: l, h => by
    have ih := countP_or_add p q l (fun x hx => h x (List.mem_cons_of_mem _ hx))
    have ha := h a List.mem_cons_self
    simp only [List.countP_cons]
    rw [ih]
    cases hp : p a <;> cases hq : q a <;> simp_all <;> omega

/-- Items inside a union of two separated sets: additivity of the count. -/
theorem cntIn_append {items : List (List Nat)} {X Y : List Nat}
    (hne : ∀ e ∈ items, e ≠ []) (hXY : ∀ x ∈ X, x ∉ Y)
    (hsplit : ∀ e ∈ items, (∀ z ∈ e, z ∈ X ++ Y) → (∀ z ∈ e, z ∈ X) ∨ (∀ z ∈ e, z ∈ Y)) :
    cntIn items (X ++ Y) = cntIn items X + cntIn items Y := by
  unfold cntIn
  have key : items.countP (fun e => subsetB e (X ++ Y)) =
      items.countP (fun e => subsetB e X || subsetB e Y) := by
    apply List.countP_congr
    intro e he
    simp only [Bool.or_eq_true, subsetB_iff]
    constructor
    · intro h
      rcases hsplit e he (fun z hz => h z hz) with h1 | h1
      · exact Or.inl h1
      · exact Or.inr h1
    · rintro (h | h) z hz
      · exact List.mem_append_left _ (h z hz)
      · exact List.mem_append_right _ (h z hz)
  rw [key]
  apply countP_or_add
  intro e he h1
  rw [Bool.eq_false_iff]
  intro h2
  obtain ⟨z, hz⟩ : ∃ z, z ∈ e := List.exists_mem_of_ne_nil _ (hne e he)
  exact hXY z (subsetB_iff.1 h1 z hz) (subsetB_iff.1 h2 z hz)


/-! ## Incidence lists -/

theorem mem_inc_inner (e : List Nat) (k : Nat) : ∀ (m : Std.HashMap Nat (List Nat))
    (y k' : Nat),
    k' ∈ (e.foldl (fun (m : Std.HashMap Nat (List Nat)) x => m.insert x (m.getD x [] ++ [k])) m).getD y [] ↔
      k' ∈ m.getD y [] ∨ (y ∈ e ∧ k' = k) := by
  induction e with
  | nil => intro m y k'; simp
  | cons x e ih =>
    intro m y k'
    rw [List.foldl_cons, ih]
    by_cases hxy : x = y
    · subst hxy
      simp only [Std.HashMap.getD_insert, beq_self_eq_true, ite_true, List.mem_append,
        List.mem_cons, List.mem_singleton]
      tauto
    · have hne : (x == y) = false := by simpa using hxy
      have hyx : y ≠ x := fun h => hxy h.symm
      simp only [Std.HashMap.getD_insert, hne, Bool.false_eq_true, ite_false, List.mem_cons]
      simp [hyx]

theorem mem_inc_outer (L : List (List Nat × Nat)) : ∀ (m : Std.HashMap Nat (List Nat))
    (y k' : Nat),
    k' ∈ (L.foldl (fun (m : Std.HashMap Nat (List Nat)) (p : List Nat × Nat) =>
      p.1.foldl (fun (m : Std.HashMap Nat (List Nat)) x => m.insert x (m.getD x [] ++ [p.2])) m) m).getD y []
      ↔ k' ∈ m.getD y [] ∨ ∃ p ∈ L, y ∈ p.1 ∧ k' = p.2 := by
  induction L with
  | nil => intro m y k'; simp
  | cons p L ih =>
    intro m y k'
    rw [List.foldl_cons, ih, mem_inc_inner]
    constructor
    · rintro ((h | ⟨h1, h2⟩) | ⟨q, hq, h1, h2⟩)
      · exact Or.inl h
      · exact Or.inr ⟨p, List.mem_cons_self, h1, h2⟩
      · exact Or.inr ⟨q, List.mem_cons_of_mem _ hq, h1, h2⟩
    · rintro (h | ⟨q, hq, h1, h2⟩)
      · exact Or.inl (Or.inl h)
      · rcases List.mem_cons.1 hq with rfl | hq
        · exact Or.inl (Or.inr ⟨h1, h2⟩)
        · exact Or.inr ⟨q, hq, h1, h2⟩

/-- Membership in the incidence list: `k ∈ inc y ↔ y ∈ items[k]`. -/
theorem inc_mem (Qs : List Nat) (items : List (List Nat)) (y k : Nat) :
    k ∈ (connectorIncidence Qs items).getD y [] ↔ y ∈ items.getD k [] := by
  unfold connectorIncidence
  rw [mem_inc_outer]
  simp only [Std.HashMap.getD_empty, List.not_mem_nil, false_or]
  constructor
  · rintro ⟨p, hp, hy, rfl⟩
    have h1 := List.mem_zipIdx_iff_getElem?.1 hp
    rw [List.getD_eq_getElem?_getD, h1]
    simpa using hy
  · intro hy
    have hk : k < items.length := by
      by_contra h
      push_neg at h
      rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none h] at hy
      simp at hy
    refine ⟨(items[k], k), List.mem_zipIdx_iff_getElem?.2 (by simp [List.getElem?_eq_getElem hk]), ?_, rfl⟩
    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hk] at hy
    simpa using hy

/-- An element of `items.getD k []` lying in it makes that list an item. -/
theorem getD_mem_of_mem {items : List (List Nat)} {k y : Nat}
    (h : y ∈ items.getD k []) : items.getD k [] ∈ items := by
  rw [List.getD_eq_getElem?_getD] at h ⊢
  cases hk : items[k]? with
  | none => simp [hk] at h
  | some e => exact List.mem_of_getElem? hk

/-- Size of the incidence lists restricted to `c`. -/
def sumInc (c : List Nat) (m : Std.HashMap Nat (List Nat)) : Nat :=
  (c.map fun x => (m.getD x []).length).sum

theorem sumInc_congr (c : List Nat) (m m' : Std.HashMap Nat (List Nat))
    (h : ∀ y ∈ c, m'.getD y [] = m.getD y []) : sumInc c m' = sumInc c m := by
  unfold sumInc
  congr 1
  apply List.map_congr_left
  intro y hy
  simp [h y hy]

theorem sumInc_insert (c : List Nat) (hc : c.Nodup) (m : Std.HashMap Nat (List Nat))
    (x k : Nat) :
    sumInc c (m.insert x (m.getD x [] ++ [k])) ≤ sumInc c m + (if x ∈ c then 1 else 0) := by
  induction c with
  | nil => simp [sumInc]
  | cons a c ih =>
    rw [List.nodup_cons] at hc
    unfold sumInc at ih ⊢
    simp only [List.map_cons, List.sum_cons]
    by_cases hax : a = x
    · subst hax
      have hrest : ∀ y ∈ c, (m.insert a (m.getD a [] ++ [k])).getD y [] = m.getD y [] := by
        intro y hy
        have hya : (a == y) = false := by
          simp only [beq_eq_false_iff_ne, ne_eq]
          exact fun h => hc.1 (h ▸ hy)
        rw [Std.HashMap.getD_insert, hya]; simp
      have hr := sumInc_congr c m _ hrest
      unfold sumInc at hr
      rw [Std.HashMap.getD_insert_self]
      have hmem : a ∉ c := hc.1
      simp only [List.mem_cons, true_or, if_true]
      simp only [List.length_append, List.length_singleton]
      omega
    · have hne : (x == a) = false := by simpa using (Ne.symm hax)
      rw [Std.HashMap.getD_insert, hne]
      simp only [Bool.false_eq_true, ite_false]
      have ih' := ih hc.2
      have hmem : x ∈ a :: c ↔ x ∈ c := by
        simp only [List.mem_cons]
        exact ⟨fun h => h.resolve_left (Ne.symm hax), fun h => Or.inr h⟩
      by_cases hxc : x ∈ c
      · have := hmem.2 hxc
        simp only [if_pos hxc] at ih' ⊢
        simp only [if_pos this]
        omega
      · have := mt hmem.1 hxc
        simp only [if_neg hxc] at ih' ⊢
        simp only [if_neg this]
        omega

theorem sumInc_fold (c : List Nat) (hc : c.Nodup) (k : Nat) (e : List Nat) :
    ∀ m : Std.HashMap Nat (List Nat),
      sumInc c (e.foldl (fun (m : Std.HashMap Nat (List Nat)) x => m.insert x (m.getD x [] ++ [k])) m)
        ≤ sumInc c m + e.length := by
  induction e with
  | nil => intro m; simp
  | cons x e ih =>
    intro m
    rw [List.foldl_cons]
    have h1 := ih (m.insert x (m.getD x [] ++ [k]))
    have h2 := sumInc_insert c hc m x k
    have h3 : (if x ∈ c then 1 else 0) ≤ 1 := by split_ifs <;> omega
    simp only [List.length_cons]
    omega

theorem sumInc_outer (c : List Nat) (hc : c.Nodup) (L : List (List Nat × Nat)) :
    ∀ m : Std.HashMap Nat (List Nat),
      sumInc c (L.foldl (fun (m : Std.HashMap Nat (List Nat)) (p : List Nat × Nat) =>
        p.1.foldl (fun (m : Std.HashMap Nat (List Nat)) x => m.insert x (m.getD x [] ++ [p.2])) m) m)
        ≤ sumInc c m + (L.map fun p => p.1.length).sum := by
  induction L with
  | nil => intro m; simp
  | cons p L ih =>
    intro m
    rw [List.foldl_cons]
    have h1 := ih (p.1.foldl (fun (m : Std.HashMap Nat (List Nat)) x => m.insert x (m.getD x [] ++ [p.2])) m)
    have h2 := sumInc_fold c hc p.2 p.1 m
    simp only [List.map_cons, List.sum_cons]
    omega

/-- The total incidence size is at most the total size of the items. -/
theorem sumInc_incidence (Qs : List Nat) (items : List (List Nat)) (c : List Nat)
    (hc : c.Nodup) : sumInc c (connectorIncidence Qs items) ≤ (items.map List.length).sum := by
  unfold connectorIncidence
  have h := sumInc_outer c hc items.zipIdx ∅
  have hz : ((items.zipIdx).map fun p => p.1.length).sum = (items.map List.length).sum := by
    congr 1
    have : (items.zipIdx).map (fun p => p.1.length) = items.map List.length := by
      apply List.ext_getElem
      · simp
      · intro i h1 h2
        simp
    exact this
  have h0 : sumInc c (∅ : Std.HashMap Nat (List Nat)) = 0 := by
    unfold sumInc; simp
  rw [h0, hz] at h
  simpa using h


/-! ## The DFS `connDfs` -/

/-- One inner step of `connDfs`: add `z` unless it is assigned already. -/
def dfsF (acc : List Nat × Std.HashSet Nat × List Nat) (z : Nat) :
    List Nat × Std.HashSet Nat × List Nat :=
  if acc.2.1.contains z then acc else (z :: acc.1, acc.2.1.insert z, z :: acc.2.2)

/-- Invariant of the DFS state `(stk, A, M)` (`A` assigned, `M` members, `stk` pending),
for the root `root`, the set `A0` assigned before the call, and the universe `all`. -/
structure DBase (items : List (List Nat)) (all : List Nat) (A0 : Std.HashSet Nat)
    (root : Nat) (stk : List Nat) (A : Std.HashSet Nat) (M : List Nat) : Prop where
  nodup : M.Nodup
  sub : ∀ w ∈ M, w ∈ all
  asg : ∀ w ∈ M, A.contains w = true
  stkM : ∀ w ∈ stk, w ∈ M
  reach : ∀ w ∈ M, Reach items root w
  base : ∀ w, A0.contains w = true → A.contains w = true
  asgA0 : ∀ w, A.contains w = true → A0.contains w = true ∨ w ∈ M
  freshA0 : ∀ w ∈ M, ¬ A0.contains w = true
  shape : ∃ T, M = T ++ [root]

/-- `DBase` together with the pending condition: an item through a member is either
pending on the stack or fully assigned. -/
def DInv (items : List (List Nat)) (all : List Nat) (A0 : Std.HashSet Nat) (root : Nat)
    (stk : List Nat) (A : Std.HashSet Nat) (M : List Nat) : Prop :=
  DBase items all A0 root stk A M ∧
    ∀ y ∈ M, ∀ e ∈ items, y ∈ e → y ∈ stk ∨ ∀ z ∈ e, A.contains z = true

theorem dfsF_facts {items : List (List Nat)} {all : List Nat} {A0 : Std.HashSet Nat}
    {root : Nat} (acc : List Nat × Std.HashSet Nat × List Nat)
    (h : DBase items all A0 root acc.1 acc.2.1 acc.2.2) {z : Nat} (hz : z ∈ all)
    (hr : Reach items root z) :
    DBase items all A0 root (dfsF acc z).1 (dfsF acc z).2.1 (dfsF acc z).2.2 ∧
    (∀ w ∈ acc.1, w ∈ (dfsF acc z).1) ∧
    (∀ w, acc.2.1.contains w = true → (dfsF acc z).2.1.contains w = true) ∧
    (∀ w ∈ acc.2.2, w ∈ (dfsF acc z).2.2) ∧
    (∀ w ∈ (dfsF acc z).2.2, w ∈ acc.2.2 ∨ w ∈ (dfsF acc z).1) ∧
    (dfsF acc z).1.length + acc.2.2.length = acc.1.length + (dfsF acc z).2.2.length ∧
    (dfsF acc z).2.1.contains z = true := by
  obtain ⟨s, A, M⟩ := acc
  dsimp only at h ⊢
  by_cases hA : A.contains z = true
  · have e : dfsF (s, A, M) z = (s, A, M) := by unfold dfsF; simp [hA]
    rw [e]
    exact ⟨h, fun w hw => hw, fun w hw => hw, fun w hw => hw, fun w hw => Or.inl hw, by simp,
      by simpa using hA⟩
  · have hA' : A.contains z = false := by simpa using hA
    have e : dfsF (s, A, M) z = (z :: s, A.insert z, z :: M) := by
      unfold dfsF; simp [hA']
    rw [e]
    dsimp only
    have hzM : z ∉ M := fun hm => by
      have := h.asg z hm
      rw [hA'] at this
      exact Bool.false_ne_true this
    have hD : DBase items all A0 root (z :: s) (A.insert z) (z :: M) := by
      refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
      · exact List.nodup_cons.2 ⟨hzM, h.nodup⟩
      · intro w hw
        rcases List.mem_cons.1 hw with rfl | hw
        · exact hz
        · exact h.sub w hw
      · intro w hw
        rcases List.mem_cons.1 hw with rfl | hw
        · rw [Std.HashSet.contains_insert]; simp
        · rw [Std.HashSet.contains_insert]; simp [h.asg w hw]
      · intro w hw
        rcases List.mem_cons.1 hw with rfl | hw
        · exact List.mem_cons_self
        · exact List.mem_cons_of_mem _ (h.stkM w hw)
      · intro w hw
        rcases List.mem_cons.1 hw with rfl | hw
        · exact hr
        · exact h.reach w hw
      · intro w hw
        rw [Std.HashSet.contains_insert]
        simp [h.base w hw]
      · intro w hw
        rw [Std.HashSet.contains_insert] at hw
        simp only [Bool.or_eq_true, beq_iff_eq] at hw
        rcases hw with rfl | hw
        · exact Or.inr List.mem_cons_self
        · rcases h.asgA0 w hw with h1 | h1
          · exact Or.inl h1
          · exact Or.inr (List.mem_cons_of_mem _ h1)
      · intro w hw hA0
        rcases List.mem_cons.1 hw with rfl | hw
        · have := h.base _ hA0
          rw [hA'] at this
          exact Bool.false_ne_true this
        · exact h.freshA0 w hw hA0
      · obtain ⟨T, hT⟩ := h.shape
        exact ⟨z :: T, by rw [hT]; simp⟩
    refine ⟨hD, fun w hw => List.mem_cons_of_mem _ hw, fun w hw => ?_,
      fun w hw => List.mem_cons_of_mem _ hw, fun w hw => ?_, ?_, ?_⟩
    · rw [Std.HashSet.contains_insert]; simp [hw]
    · rcases List.mem_cons.1 hw with rfl | hw
      · exact Or.inr List.mem_cons_self
      · exact Or.inl hw
    · simp only [List.length_cons]; omega
    · rw [Std.HashSet.contains_insert]; simp

/-- The inner fold over a list of elements. -/
theorem fold_dfsF {items : List (List Nat)} {all : List Nat} {A0 : Std.HashSet Nat}
    {root : Nat} : ∀ (L : List Nat) (acc : List Nat × Std.HashSet Nat × List Nat),
    (∀ z ∈ L, z ∈ all) → (∀ z ∈ L, Reach items root z) →
    DBase items all A0 root acc.1 acc.2.1 acc.2.2 →
    DBase items all A0 root (L.foldl dfsF acc).1 (L.foldl dfsF acc).2.1 (L.foldl dfsF acc).2.2 ∧
    (∀ w ∈ acc.1, w ∈ (L.foldl dfsF acc).1) ∧
    (∀ w, acc.2.1.contains w = true → (L.foldl dfsF acc).2.1.contains w = true) ∧
    (∀ w ∈ acc.2.2, w ∈ (L.foldl dfsF acc).2.2) ∧
    (∀ w ∈ (L.foldl dfsF acc).2.2, w ∈ acc.2.2 ∨ w ∈ (L.foldl dfsF acc).1) ∧
    (L.foldl dfsF acc).1.length + acc.2.2.length = acc.1.length + (L.foldl dfsF acc).2.2.length ∧
    (∀ z ∈ L, (L.foldl dfsF acc).2.1.contains z = true) := by
  intro L
  induction L with
  | nil =>
    intro acc _ _ h
    exact ⟨h, fun _ hw => hw, fun _ hw => hw, fun _ hw => hw, fun w hw => Or.inl hw, rfl,
      by simp⟩
  | cons x L ih =>
    intro acc hall hreach h
    rw [List.foldl_cons]
    obtain ⟨h1, h2, h3, h4, h5, h6, h7⟩ := dfsF_facts acc h (hall x List.mem_cons_self)
      (hreach x List.mem_cons_self)
    obtain ⟨i1, i2, i3, i4, i5, i6, i7⟩ := ih (dfsF acc x)
      (fun z hz => hall z (List.mem_cons_of_mem _ hz))
      (fun z hz => hreach z (List.mem_cons_of_mem _ hz)) h1
    refine ⟨i1, fun w hw => i2 w (h2 w hw), fun w hw => i3 w (h3 w hw),
      fun w hw => i4 w (h4 w hw), ?_, ?_, ?_⟩
    · intro w hw
      rcases i5 w hw with h8 | h8
      · rcases h5 w h8 with h9 | h9
        · exact Or.inl h9
        · exact Or.inr (i2 w h9)
      · exact Or.inr h8
    · omega
    · intro z hz
      rcases List.mem_cons.1 hz with rfl | hz
      · exact i3 _ h7
      · exact i7 z hz

/-- One outer step of `connDfs`: fold over the elements of the item `items.getD k []`. -/
def dfsK (items : List (List Nat)) (acc : List Nat × Std.HashSet Nat × List Nat) (k : Nat) :
    List Nat × Std.HashSet Nat × List Nat :=
  (items.getD k []).foldl dfsF acc

theorem dfsK_facts {items : List (List Nat)} {all : List Nat} {A0 : Std.HashSet Nat}
    {root : Nat} (hall : ∀ e ∈ items, ∀ z ∈ e, z ∈ all)
    (acc : List Nat × Std.HashSet Nat × List Nat)
    (h : DBase items all A0 root acc.1 acc.2.1 acc.2.2) (k y0 : Nat)
    (hy : y0 ∈ items.getD k []) (hy0 : y0 ∈ acc.2.2) :
    DBase items all A0 root (dfsK items acc k).1 (dfsK items acc k).2.1 (dfsK items acc k).2.2 ∧
    (∀ w ∈ acc.1, w ∈ (dfsK items acc k).1) ∧
    (∀ w, acc.2.1.contains w = true → (dfsK items acc k).2.1.contains w = true) ∧
    (∀ w ∈ acc.2.2, w ∈ (dfsK items acc k).2.2) ∧
    (∀ w ∈ (dfsK items acc k).2.2, w ∈ acc.2.2 ∨ w ∈ (dfsK items acc k).1) ∧
    (dfsK items acc k).1.length + acc.2.2.length = acc.1.length + (dfsK items acc k).2.2.length ∧
    (∀ z ∈ items.getD k [], (dfsK items acc k).2.1.contains z = true) := by
  have hmem : items.getD k [] ∈ items := getD_mem_of_mem hy
  have hreach0 : Reach items root y0 := h.reach y0 hy0
  have hL1 : ∀ z ∈ items.getD k [], z ∈ all := fun z hz => hall _ hmem z hz
  have hL2 : ∀ z ∈ items.getD k [], Reach items root z := fun z hz =>
    Relation.ReflTransGen.tail hreach0 ⟨_, hmem, hy, hz⟩
  unfold dfsK
  exact fold_dfsF (items.getD k []) acc hL1 hL2 h

theorem fold_ks {items : List (List Nat)} {all : List Nat} {A0 : Std.HashSet Nat}
    {root : Nat} (hall : ∀ e ∈ items, ∀ z ∈ e, z ∈ all) (y0 : Nat) :
    ∀ (ks : List Nat) (acc : List Nat × Std.HashSet Nat × List Nat),
    y0 ∈ acc.2.2 → DBase items all A0 root acc.1 acc.2.1 acc.2.2 →
    (∀ k ∈ ks, y0 ∈ items.getD k []) →
    DBase items all A0 root (ks.foldl (dfsK items) acc).1 (ks.foldl (dfsK items) acc).2.1
        (ks.foldl (dfsK items) acc).2.2 ∧
    (∀ w ∈ acc.1, w ∈ (ks.foldl (dfsK items) acc).1) ∧
    (∀ w, acc.2.1.contains w = true → (ks.foldl (dfsK items) acc).2.1.contains w = true) ∧
    (∀ w ∈ acc.2.2, w ∈ (ks.foldl (dfsK items) acc).2.2) ∧
    (∀ w ∈ (ks.foldl (dfsK items) acc).2.2, w ∈ acc.2.2 ∨ w ∈ (ks.foldl (dfsK items) acc).1) ∧
    (ks.foldl (dfsK items) acc).1.length + acc.2.2.length =
      acc.1.length + (ks.foldl (dfsK items) acc).2.2.length ∧
    (∀ k ∈ ks, ∀ z ∈ items.getD k [], (ks.foldl (dfsK items) acc).2.1.contains z = true) := by
  intro ks
  induction ks with
  | nil =>
    intro acc _ h _
    exact ⟨h, fun _ hw => hw, fun _ hw => hw, fun _ hw => hw, fun w hw => Or.inl hw, rfl,
      fun k hk => absurd hk List.not_mem_nil⟩
  | cons k ks ih =>
    intro acc hy0 h hks
    obtain ⟨g1, g2, g3, g4, g5, g6, g7⟩ := dfsK_facts hall acc h k y0 (hks k List.mem_cons_self) hy0
    have hy1 : y0 ∈ (dfsK items acc k).2.2 := g4 y0 hy0
    obtain ⟨i1, i2, i3, i4, i5, i6, i7⟩ := ih (dfsK items acc k) hy1 g1
      (fun k' hk' => hks k' (List.mem_cons_of_mem _ hk'))
    rw [List.foldl_cons]
    refine ⟨i1, fun w hw => i2 w (g2 w hw), fun w hw => i3 w (g3 w hw),
      fun w hw => i4 w (g4 w hw), ?_, ?_, ?_⟩
    · intro w hw
      rcases i5 w hw with h8 | h8
      · rcases g5 w h8 with h9 | h9
        · exact Or.inl h9
        · exact Or.inr (i2 w h9)
      · exact Or.inr h8
    · omega
    · intro k' hk' z hz
      rcases List.mem_cons.1 hk' with rfl | hk'
      · exact i3 z (g7 z hz)
      · exact i7 k' hk' z hz

/-- The pop step of `connDfs`: the root of the popped item is removed, its item-neighbours
are pushed (through `inc`) and all their elements are assigned. -/
theorem dfs_pop {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)}
    {all : List Nat} {A0 : Std.HashSet Nat} {root : Nat}
    (hall : ∀ e ∈ items, ∀ z ∈ e, z ∈ all)
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    {y0 : Nat} {rest : List Nat} {A : Std.HashSet Nat} {M : List Nat}
    (hD : DInv items all A0 root (y0 :: rest) A M) :
    DInv items all A0 root ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).1
        ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).2.1
        ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).2.2 ∧
    ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).1.length + M.length =
      rest.length + ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).2.2.length := by
  obtain ⟨hB, hpend⟩ := hD
  have hy0M : y0 ∈ M := hB.stkM y0 List.mem_cons_self
  have hBr : DBase items all A0 root rest A M :=
    { hB with stkM := fun w hw => hB.stkM w (List.mem_cons_of_mem _ hw) }
  obtain ⟨j1, j2, j3, j4, j5, j6, j7⟩ := fold_ks hall y0 (inc.getD y0 []) (rest, A, M) hy0M hBr
    (fun k hk => (hinc k y0).1 hk)
  refine ⟨⟨j1, ?_⟩, j6⟩
  intro y hy e he hye
  rcases j5 y hy with hyM | hyS
  · rcases hpend y hyM e he hye with h1 | h1
    · rcases List.mem_cons.1 h1 with rfl | h1
      · obtain ⟨k, rfl⟩ : ∃ k, items.getD k [] = e := by
          obtain ⟨k, hk, hke⟩ := List.mem_iff_getElem.1 he
          exact ⟨k, by rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hk]; simp [hke]⟩
        exact Or.inr (j7 k ((hinc k y).2 hye))
      · exact Or.inl (j2 y h1)
    · exact Or.inr (fun z hz => j3 z (h1 z hz))
  · exact Or.inl hyS

theorem dinv_init {items : List (List Nat)} {all : List Nat} (A0 : Std.HashSet Nat)
    (root : Nat) (hr : root ∈ all) (hA0 : ¬ A0.contains root = true) :
    DInv items all A0 root [root] (A0.insert root) [root] := by
  refine ⟨⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩, ?_⟩
  · simp
  · intro w hw
    rw [List.mem_singleton] at hw
    rw [hw]; exact hr
  · intro w hw
    rw [List.mem_singleton] at hw
    rw [hw, Std.HashSet.contains_insert]; simp
  · intro w hw; exact hw
  · intro w hw
    rw [List.mem_singleton] at hw
    rw [hw]; exact Relation.ReflTransGen.refl
  · intro w hw
    rw [Std.HashSet.contains_insert]
    simp [hw]
  · intro w hw
    rw [Std.HashSet.contains_insert] at hw
    simp only [Bool.or_eq_true, beq_iff_eq] at hw
    rcases hw with rfl | hw
    · exact Or.inr (List.mem_singleton_self _)
    · exact Or.inl hw
  · intro w hw
    rw [List.mem_singleton] at hw
    rw [hw]; exact hA0
  · exact ⟨[], by simp⟩
  · intro y hy _ _ _
    exact Or.inl hy

/-- Completion of the DFS: from a state satisfying `DInv` with enough fuel
(`|stk| + |all| ≤ fuel + |M|`), `connDfs` empties its stack, and the invariant holds. -/
theorem dfs_complete {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)}
    {all : List Nat} {A0 : Std.HashSet Nat} {root : Nat}
    (hall : ∀ e ∈ items, ∀ z ∈ e, z ∈ all)
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k []) :
    ∀ (f : Nat) (stk : List Nat) (A : Std.HashSet Nat) (M : List Nat),
      DInv items all A0 root stk A M → stk.length + all.length ≤ f + M.length →
      (connectorComponents.connDfs items inc f stk A M).1 = [] ∧
      DInv items all A0 root (connectorComponents.connDfs items inc f stk A M).1
        (connectorComponents.connDfs items inc f stk A M).2.1
        (connectorComponents.connDfs items inc f stk A M).2.2 := by
  intro f
  induction f with
  | zero =>
    intro stk A M hD hpot
    have hMl : M.length ≤ all.length :=
      (List.subperm_of_subset hD.1.nodup (by intro w hw; exact hD.1.sub w hw)).length_le
    have hstk : stk = [] := List.eq_nil_of_length_eq_zero (by omega)
    subst hstk
    rw [connectorComponents.connDfs]
    exact ⟨rfl, hD⟩
  | succ f ih =>
    intro stk A M hD hpot
    cases stk with
    | nil =>
      rw [connectorComponents.connDfs]
      exact ⟨rfl, hD⟩
    | cons y0 rest =>
      have hpop := dfs_pop hall hinc hD
      have key : connectorComponents.connDfs items inc (f + 1) (y0 :: rest) A M =
          connectorComponents.connDfs items inc f
            ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).1
            ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).2.1
            ((inc.getD y0 []).foldl (dfsK items) (rest, A, M)).2.2 := by
        rw [connectorComponents.connDfs]
        try rfl
      rw [key]
      have hl := hpop.2
      simp only [List.length_cons] at hpot
      exact ih _ _ _ hpop.1 (by omega)


/-! ## The outer scan `connOuter` -/

/-- Invariant of the component list (newest first) and of the assigned set `A`: the
components are connected (from a root), closed under items, nodup, inside `all`,
pairwise disjoint, and `A` is exactly their union; `A` is closed under items. -/
structure OInv (items : List (List Nat)) (all : List Nat) (A : Std.HashSet Nat)
    (comps : List (List Nat)) : Prop where
  reach : ∀ c ∈ comps, ∃ r c', c = r :: c' ∧ ∀ w ∈ c, Reach items r w
  nodup : ∀ c ∈ comps, c.Nodup
  sub : ∀ c ∈ comps, ∀ y ∈ c, y ∈ all
  closed : ∀ c ∈ comps, ∀ y ∈ c, ∀ e ∈ items, y ∈ e → ∀ z ∈ e, z ∈ c
  disj : comps.Pairwise (fun c c' => ∀ y ∈ c, y ∉ c')
  closedA : ∀ e ∈ items, (∃ z ∈ e, A.contains z = true) → ∀ z ∈ e, A.contains z = true
  asgIff : ∀ w, A.contains w = true ↔ ∃ c ∈ comps, w ∈ c

theorem oinv_add {items : List (List Nat)} {all : List Nat} {A : Std.HashSet Nat}
    {comps : List (List Nat)} {root : Nat} {Ad : Std.HashSet Nat} {M : List Nat}
    (hO : OInv items all A comps) (hD : DInv items all A root [] Ad M) :
    OInv items all Ad (M.reverse :: comps) := by
  obtain ⟨hB, hpend⟩ := hD
  obtain ⟨T, hT⟩ := hB.shape
  have hrev : M.reverse = root :: T.reverse := by rw [hT]; simp
  have hclM : ∀ y ∈ M, ∀ e ∈ items, y ∈ e → ∀ z ∈ e, z ∈ M := by
    intro y hy e he hye z hz
    rcases hpend y hy e he hye with h1 | h1
    · simp at h1
    · rcases hB.asgA0 z (h1 z hz) with h2 | h2
      · exfalso
        exact hB.freshA0 y hy (hO.closedA e he ⟨z, hz, h2⟩ y hye)
      · exact h2
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · intro c hc
    rcases List.mem_cons.1 hc with rfl | hc
    · exact ⟨root, T.reverse, hrev, fun w hw => hB.reach w (List.mem_reverse.1 hw)⟩
    · exact hO.reach c hc
  · intro c hc
    rcases List.mem_cons.1 hc with rfl | hc
    · exact List.nodup_reverse.2 hB.nodup
    · exact hO.nodup c hc
  · intro c hc
    rcases List.mem_cons.1 hc with rfl | hc
    · exact fun y hy => hB.sub y (List.mem_reverse.1 hy)
    · exact hO.sub c hc
  · intro c hc y hy e he hye z hz
    rcases List.mem_cons.1 hc with rfl | hc
    · exact List.mem_reverse.2 (hclM y (List.mem_reverse.1 hy) e he hye z hz)
    · exact hO.closed c hc y hy e he hye z hz
  · refine List.pairwise_cons.2 ⟨fun c' hc' y hy hyc => ?_, hO.disj⟩
    exact hB.freshA0 y (List.mem_reverse.1 hy) ((hO.asgIff y).2 ⟨c', hc', hyc⟩)
  · intro e he ⟨z0, hz0, hA⟩
    rcases hB.asgA0 z0 hA with h1 | h1
    · intro z hz
      exact hB.base z (hO.closedA e he ⟨z0, hz0, h1⟩ z hz)
    · intro z hz
      exact hB.asg z (hclM z0 h1 e he hz0 z hz)
  · intro w
    constructor
    · intro hw
      rcases hB.asgA0 w hw with h1 | h1
      · obtain ⟨c, hc, hwc⟩ := (hO.asgIff w).1 h1
        exact ⟨c, List.mem_cons_of_mem _ hc, hwc⟩
      · exact ⟨M.reverse, List.mem_cons_self, List.mem_reverse.2 h1⟩
    · rintro ⟨c, hc, hwc⟩
      rcases List.mem_cons.1 hc with rfl | hc
      · exact hB.asg w (List.mem_reverse.1 hwc)
      · exact hB.base w ((hO.asgIff w).2 ⟨c, hc, hwc⟩)

theorem connOuter_spec {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)}
    {all : List Nat} {fuel : Nat}
    (hall : ∀ e ∈ items, ∀ z ∈ e, z ∈ all)
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hfuel : all.length ≤ fuel) :
    ∀ (qs : List Nat) (A : Std.HashSet Nat) (comps : List (List Nat)),
      OInv items all A comps → (∀ y ∈ qs, y ∈ all) →
      ∃ (C : List (List Nat)) (A' : Std.HashSet Nat),
        connectorComponents.connOuter items inc all fuel qs A comps = C.reverse ∧
        OInv items all A' C ∧ (∀ c ∈ comps, c ∈ C) ∧ (∀ y ∈ qs, ∃ c ∈ C, y ∈ c) := by
  intro qs
  induction qs with
  | nil =>
    intro A comps hO _
    refine ⟨comps, A, ?_, hO, fun c hc => hc, fun y hy => by simp at hy⟩
    rw [connectorComponents.connOuter]
  | cons x qs ih =>
    intro A comps hO hqs
    have hxall : x ∈ all := hqs x List.mem_cons_self
    have hqs' : ∀ y ∈ qs, y ∈ all := fun y hy => hqs y (List.mem_cons_of_mem _ hy)
    rw [connectorComponents.connOuter]
    by_cases hx : A.contains x = true
    · rw [if_pos hx]
      obtain ⟨C, A', heq, hO', hsub, hcov⟩ := ih A comps hO hqs'
      refine ⟨C, A', heq, hO', hsub, ?_⟩
      intro y hy
      rcases List.mem_cons.1 hy with rfl | hy
      · obtain ⟨c, hc, hyc⟩ := (hO.asgIff y).1 hx
        exact ⟨c, hsub c hc, hyc⟩
      · exact hcov y hy
    · have hx' : ¬ A.contains x = true := hx
      rw [if_neg hx']
      have hpot : [x].length + all.length ≤ fuel + [x].length := by simp; omega
      obtain ⟨hempty, hDfin⟩ := dfs_complete hall hinc fuel [x] (A.insert x) [x]
        (dinv_init A x hxall hx') hpot
      generalize connectorComponents.connDfs items inc fuel [x] (A.insert x) [x] = r at hempty hDfin ⊢
      have hxM : x ∈ r.2.2 := by
        obtain ⟨T, hT⟩ := hDfin.1.shape
        rw [hT]; simp
      obtain ⟨C, A', heq, hO', hsub, hcov⟩ :=
        ih r.2.1 (r.2.2.reverse :: comps) (oinv_add hO (by rw [hempty] at hDfin; exact hDfin)) hqs'
      refine ⟨C, A', ?_, hO', fun c hc => hsub c (List.mem_cons_of_mem _ hc), ?_⟩
      · dsimp only
        rw [hempty]
        simp only [List.isEmpty_nil, ite_true]
        exact heq
      · intro y hy
        rcases List.mem_cons.1 hy with rfl | hy
        · exact ⟨_, hsub _ List.mem_cons_self, List.mem_reverse.2 hxM⟩
        · exact hcov y hy


/-! ## Pure list facts -/

theorem exists_getD {items : List (List Nat)} {e : List Nat} (he : e ∈ items) :
    ∃ k, items.getD k [] = e := by
  obtain ⟨k, hk, rfl⟩ := List.mem_iff_getElem.1 he
  exact ⟨k, by simp [List.getD_eq_getElem?_getD, hk]⟩

theorem add_cases (its : List Nat) (P : Nat → Bool) (z : Nat)
    (hf : its.filter (fun w => !P w) = [z]) (hl : its.length = 2) :
    z ∈ its ∧ P z = false ∧ (∀ w ∈ its, w = z ∨ P w = true) ∧ ∃ y ∈ its, P y = true := by
  obtain ⟨a, b, rfl⟩ := List.length_eq_two.1 hl
  cases ha : P a <;> cases hb : P b <;> simp_all [List.filter]

theorem discard_all (its : List Nat) (P : Nat → Bool) (hl : its.length ≤ 2)
    (hex : ∃ y ∈ its, P y = true)
    (hnot : ¬ ∃ z, its.filter (fun w => !P w) = [z] ∧ its.length = 2) :
    ∀ w ∈ its, P w = true := by
  match its, hl, hex, hnot with
  | [], _, ⟨y, hy, _⟩, _ => simp at hy
  | [a], _, hex, hnot =>
    obtain ⟨y, hy, hPy⟩ := hex
    simp only [List.mem_singleton] at hy
    subst hy
    intro w hw
    simp only [List.mem_singleton] at hw
    subst hw
    exact hPy
  | [a, b], _, hex, hnot =>
    intro w hw
    by_cases hPa : P a = true <;> by_cases hPb : P b = true
    · rcases List.mem_cons.1 hw with rfl | hw
      · exact hPa
      · rcases List.mem_cons.1 hw with rfl | hw
        · exact hPb
        · simp at hw
    · exfalso
      apply hnot
      have hPb' : P b = false := by simpa using hPb
      exact ⟨b, by simp [List.filter_cons, hPa, hPb'], rfl⟩
    · exfalso
      apply hnot
      have hPa' : P a = false := by simpa using hPa
      exact ⟨a, by simp [List.filter_cons, hPa', hPb], rfl⟩
    · exfalso
      obtain ⟨y, hy, hPy⟩ := hex
      have hPa' : P a = false := by simpa using hPa
      have hPb' : P b = false := by simpa using hPb
      rcases List.mem_cons.1 hy with rfl | hy
      · rw [hPa'] at hPy; exact Bool.false_ne_true hPy
      · rcases List.mem_cons.1 hy with rfl | hy
        · rw [hPb'] at hPy; exact Bool.false_ne_true hPy
        · simp at hy
  | _ :: _ :: _ :: _, hl, _, _ => simp at hl


/-! ## The greedy loop of `connectorGreedy` -/

theorem sumInc_le_of_sub (inc : Std.HashMap Nat (List Nat)) {l c : List Nat}
    (hl : l.Nodup) (hsub : ∀ z ∈ l, z ∈ c) : sumInc l inc ≤ sumInc c inc := by
  have hs : l.Subperm c := List.subperm_of_subset hl (by intro z hz; exact hsub z hz)
  obtain ⟨m, hpm, hsl⟩ := hs
  unfold sumInc
  have hpe := (hpm.map (fun x => (inc.getD x []).length)).sum_eq
  rw [← hpe]
  exact (hsl.map (fun x => (inc.getD x []).length)).sum_le_sum (fun _ _ => Nat.zero_le _)

/-- Invariant of the greedy loop for the component `c` (`present` is the set of the
elements of `ordRev`; the output is `ordRev.reverse`). -/
structure GInv (items : List (List Nat)) (inc : Std.HashMap Nat (List Nat)) (c : List Nat)
    (stk : List Nat) (P : Std.HashSet Nat) (ordRev : List Nat) : Prop where
  mem : ∀ z, P.contains z = true ↔ z ∈ ordRev
  nodup : ordRev.Nodup
  subc : ∀ z ∈ ordRev, z ∈ c
  pref : ∀ p, p ≤ ordRev.length → p ≤ cntIn items (ordRev.reverse.take p) + 1
  pend : ∀ y, P.contains y = true → ∀ k, y ∈ items.getD k [] →
    k ∈ stk ∨ ∀ z ∈ items.getD k [], P.contains z = true
  stkItem : ∀ k ∈ stk, ∃ y ∈ items.getD k [], P.contains y = true
  size : P.size = ordRev.length

theorem ginv_init {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)} {c : List Nat}
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k []) (start : Nat) (hstart : start ∈ c) :
    GInv items inc c ((inc.getD start []).reverse) ((∅ : Std.HashSet Nat).insert start) [start] := by
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · intro z
    rw [Std.HashSet.contains_insert]
    simp only [Bool.or_eq_true, beq_iff_eq, Std.HashSet.contains_empty, Bool.false_eq_true,
      or_false, List.mem_singleton]
    exact eq_comm
  · simp
  · intro z hz
    rw [List.mem_singleton] at hz
    rw [hz]; exact hstart
  · intro p hp
    simp only [List.length_singleton] at hp
    omega
  · intro y hy k hk
    rw [Std.HashSet.contains_insert] at hy
    simp only [Bool.or_eq_true, beq_iff_eq, Std.HashSet.contains_empty, Bool.false_eq_true,
      or_false] at hy
    subst hy
    exact Or.inl (List.mem_reverse.2 ((hinc k _).2 hk))
  · intro k hk
    refine ⟨start, ?_, ?_⟩
    · exact (hinc k start).1 (List.mem_reverse.1 hk)
    · rw [Std.HashSet.contains_insert]; simp
  · rw [Std.HashSet.size_insert, if_neg (by simp), Std.HashSet.size_empty]
    rfl

theorem ginv_add {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)} {c : List Nat}
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hcl : ∀ y ∈ c, ∀ e ∈ items, y ∈ e → ∀ z ∈ e, z ∈ c)
    {k : Nat} {rest : List Nat} {P : Std.HashSet Nat} {ordRev : List Nat} {z : Nat}
    (hG : GInv items inc c (k :: rest) P ordRev)
    (hf : (items.getD k []).filter (fun w => !P.contains w) = [z])
    (hl : (items.getD k []).length = 2) :
    GInv items inc c ((inc.getD z []).reverse ++ rest) (P.insert z) (z :: ordRev) := by
  obtain ⟨hzI, hPz, hcases, hex⟩ := add_cases (items.getD k []) (fun w => P.contains w) z hf hl
  replace hPz : P.contains z = false := hPz
  have hitem : items.getD k [] ∈ items := getD_mem_of_mem hzI
  have hzc : z ∈ c := by
    obtain ⟨y, hyI, hPy⟩ := hex
    have hyc : y ∈ c := hG.subc y ((hG.mem y).1 hPy)
    exact hcl y hyc _ hitem hyI z hzI
  have hznot : z ∉ ordRev := by
    intro h
    have := (hG.mem z).2 h
    rw [hPz] at this
    exact Bool.false_ne_true this
  have hnotP : ¬ P.contains z = true := by rw [hPz]; decide
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · intro w
    rw [Std.HashSet.contains_insert]
    simp only [Bool.or_eq_true, beq_iff_eq, List.mem_cons, hG.mem w]
    constructor
    · rintro (rfl | h)
      · exact Or.inl rfl
      · exact Or.inr h
    · rintro (rfl | h)
      · exact Or.inl rfl
      · exact Or.inr h
  · exact List.nodup_cons.2 ⟨hznot, hG.nodup⟩
  · intro w hw
    rcases List.mem_cons.1 hw with rfl | hw
    · exact hzc
    · exact hG.subc w hw
  · intro p hp
    have hLen : ordRev.reverse.length = ordRev.length := List.length_reverse
    have hL : (z :: ordRev).reverse = ordRev.reverse ++ [z] := by simp
    have hlt : cntIn items ordRev.reverse < cntIn items (ordRev.reverse ++ [z]) := by
      apply cntIn_strict (e := items.getD k []) (fun w hw => List.mem_append_left _ hw) hitem
      · intro w hw
        rcases hcases w hw with rfl | hPw
        · exact List.mem_append_right _ (List.mem_singleton_self _)
        · exact List.mem_append_left _ (List.mem_reverse.2 ((hG.mem w).1 hPw))
      · intro h
        exact hznot (List.mem_reverse.1 (h z hzI))
    rw [hL]
    simp only [List.length_cons] at hp
    by_cases hpo : p ≤ ordRev.length
    · rw [List.take_append_of_le_length (by rw [hLen]; exact hpo)]
      exact hG.pref p hpo
    · have hp' : p = ordRev.length + 1 := by omega
      rw [List.take_of_length_le (by simp; omega)]
      have hG' := hG.pref ordRev.length le_rfl
      rw [List.take_of_length_le (by simp)] at hG'
      subst hp'
      omega
  · intro y hy k' hk'
    rw [Std.HashSet.contains_insert] at hy
    simp only [Bool.or_eq_true, beq_iff_eq] at hy
    rcases hy with hyz | hy
    · exact Or.inl (List.mem_append_left _ (List.mem_reverse.2
        ((hinc k' z).2 (by rw [hyz]; exact hk'))))
    · rcases hG.pend y hy k' hk' with h | h
      · rcases List.mem_cons.1 h with rfl | h
        · right
          intro w hw
          rw [Std.HashSet.contains_insert]
          rcases hcases w hw with rfl | hPw
          · simp
          · simp [hPw]
        · exact Or.inl (List.mem_append_right _ h)
      · right
        intro w hw
        rw [Std.HashSet.contains_insert]
        simp [h w hw]
  · intro k' hk'
    rcases List.mem_append.1 hk' with h | h
    · rw [List.mem_reverse] at h
      refine ⟨z, (hinc k' z).1 h, ?_⟩
      rw [Std.HashSet.contains_insert]; simp
    · obtain ⟨y, hy, hPy⟩ := hG.stkItem k' (List.mem_cons_of_mem _ h)
      refine ⟨y, hy, ?_⟩
      rw [Std.HashSet.contains_insert]; simp [hPy]
  · rw [Std.HashSet.size_insert, if_neg (by rw [Std.HashSet.mem_iff_contains]; exact hnotP)]
    simp [hG.size]

theorem ginv_discard {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)} {c : List Nat}
    (hlen : ∀ e ∈ items, e.length ≤ 2)
    {k : Nat} {rest : List Nat} {P : Std.HashSet Nat} {ordRev : List Nat}
    (hG : GInv items inc c (k :: rest) P ordRev)
    (hnot : ¬ ∃ z, (items.getD k []).filter (fun w => !P.contains w) = [z] ∧
      (items.getD k []).length = 2) :
    GInv items inc c rest P ordRev := by
  refine ⟨hG.mem, hG.nodup, hG.subc, hG.pref, ?_, ?_, hG.size⟩
  · intro y hy k' hk'
    rcases hG.pend y hy k' hk' with h | h
    · rcases List.mem_cons.1 h with rfl | h
      · right
        obtain ⟨y0, hy0, hP0⟩ := hG.stkItem k' List.mem_cons_self
        exact discard_all (items.getD k' []) (fun w => P.contains w)
          (hlen _ (getD_mem_of_mem hk'))
          ⟨y0, hy0, hP0⟩ hnot
      · exact Or.inl h
    · exact Or.inr h
  · intro k' hk'
    obtain ⟨y, hy, hPy⟩ := hG.stkItem k' (List.mem_cons_of_mem _ hk')
    exact ⟨y, hy, hPy⟩

theorem filter_full {c : List Nat} {P : Std.HashSet Nat} (h : ∀ z ∈ c, P.contains z = true) :
    c.filter (fun z => !P.contains z) = [] :=
  List.filter_eq_nil_iff.2 (fun a ha => by simp [h a ha])

theorem greedy_full {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)}
    {c : List Nat} {stk : List Nat} {P : Std.HashSet Nat} {ordRev : List Nat}
    (hG : GInv items inc c stk P ordRev) (start : Nat) (hs : P.contains start = true)
    (hconn : ∀ w ∈ c, Reach items start w) (hstk : stk = []) :
    ∀ z ∈ c, P.contains z = true := by
  have hclosed : ∀ y, P.contains y = true → ∀ e ∈ items, y ∈ e → ∀ w ∈ e,
      P.contains w = true := by
    intro y hy e he hye w hw
    obtain ⟨k, rfl⟩ := exists_getD he
    rcases hG.pend y hy k hye with h | h
    · rw [hstk] at h; simp at h
    · exact h w hw
  have hreach : ∀ w, Reach items start w → P.contains w = true := by
    intro w hw
    unfold Reach at hw
    induction hw with
    | refl => exact hs
    | tail _ hadj ih =>
      obtain ⟨e, he, hye, hwe⟩ := hadj
      exact hclosed _ ih e he hye _ hwe
  intro z hz
  exact hreach z (hconn z hz)

theorem greedy_size {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)}
    {c : List Nat} {stk : List Nat} {P : Std.HashSet Nat} {ordRev : List Nat}
    (hG : GInv items inc c stk P ordRev) (hsz : c.length ≤ P.size) :
    ∀ z ∈ c, P.contains z = true := by
  have hsub : ordRev.Subperm c :=
    List.subperm_of_subset hG.nodup (by intro z hz; exact hG.subc z hz)
  have hperm : ordRev.Perm c := hsub.perm_of_length_le (by rw [hG.size] at hsz; exact hsz)
  intro z hz
  exact (hG.mem z).2 (hperm.symm.mem_iff.1 hz)

theorem greedy_loop_spec {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)}
    {c : List Nat} (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hlen : ∀ e ∈ items, e.length ≤ 2)
    (hcl : ∀ y ∈ c, ∀ e ∈ items, y ∈ e → ∀ z ∈ e, z ∈ c)
    (hnodup : c.Nodup) (start : Nat) (hconn : ∀ w ∈ c, Reach items start w) :
    ∀ (f : Nat) (stk : List Nat) (P : Std.HashSet Nat) (ordRev : List Nat) (fl : Bool),
      GInv items inc c stk P ordRev → P.contains start = true →
      stk.length + sumInc c inc ≤ f + sumInc ordRev inc →
      ∃ (O : List Nat) (F : Bool),
        connectorGreedy.loop items inc c
            (fun present ordRev fl => (ordRev.reverse ++ c.filter (fun z => !present.contains z), fl))
            f stk P ordRev fl = (O.reverse, F) ∧
        O.Nodup ∧ (∀ z ∈ O, z ∈ c) ∧ (∀ z ∈ c, z ∈ O) ∧
        (∀ p, p ≤ O.length → p ≤ cntIn items (O.reverse.take p) + 1) := by
  intro f
  induction f with
  | zero =>
    intro stk P ordRev fl hG hs hpot
    have hsub := sumInc_le_of_sub inc hG.nodup hG.subc
    have hstk : stk = [] := List.eq_nil_of_length_eq_zero (by omega)
    have hfull := greedy_full hG start hs hconn hstk
    refine ⟨ordRev, fl || decide (P.size < c.length), ?_, hG.nodup, hG.subc,
      fun z hz => (hG.mem z).1 (hfull z hz), hG.pref⟩
    rw [connectorGreedy.loop.eq_1]
    try dsimp only
    rw [filter_full hfull, List.append_nil]
  | succ f ih =>
    intro stk P ordRev fl hG hs hpot
    cases stk with
    | nil =>
      have hfull := greedy_full hG start hs hconn rfl
      refine ⟨ordRev, fl || decide (P.size < c.length), ?_, hG.nodup, hG.subc,
        fun z hz => (hG.mem z).1 (hfull z hz), hG.pref⟩
      rw [connectorGreedy.loop.eq_2]
      try dsimp only
      rw [filter_full hfull, List.append_nil]
    | cons k rest =>
      by_cases hsize : c.length ≤ P.size
      · have hfull := greedy_size hG hsize
        refine ⟨ordRev, fl, ?_, hG.nodup, hG.subc,
          fun z hz => (hG.mem z).1 (hfull z hz), hG.pref⟩
        rw [connectorGreedy.loop.eq_3, if_pos hsize]
        try dsimp only
        rw [filter_full hfull, List.append_nil]
      · rw [connectorGreedy.loop.eq_3, if_neg hsize]
        try dsimp only
        split
        · rename_i z hf hl
          have hsz : sumInc (z :: ordRev) inc = (inc.getD z []).length + sumInc ordRev inc := by
            unfold sumInc; simp [List.map_cons, List.sum_cons]
          have hpot' : ((inc.getD z []).reverse ++ rest).length + sumInc c inc ≤
              f + sumInc (z :: ordRev) inc := by
            rw [hsz]
            simp only [List.length_cons] at hpot
            simp only [List.length_append, List.length_reverse]
            omega
          have hs' : (P.insert z).contains start = true := by
            rw [Std.HashSet.contains_insert]; simp [hs]
          exact ih _ _ _ fl (ginv_add hinc hcl hG hf hl) hs' hpot'
        · rename_i hnot
          have hnot' : ¬ ∃ z, (items.getD k []).filter (fun w => !P.contains w) = [z] ∧
              (items.getD k []).length = 2 := by
            rintro ⟨z, h1, h2⟩
            exact hnot z h1 h2
          have hpot' : rest.length + sumInc c inc ≤ f + sumInc ordRev inc := by
            simp only [List.length_cons] at hpot
            omega
          exact ih _ _ _ fl (ginv_discard hlen hG hnot') hs hpot'

theorem greedy_out {items : List (List Nat)} {inc : Std.HashMap Nat (List Nat)}
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hlen : ∀ e ∈ items, e.length ≤ 2)
    (start : Nat) (c' : List Nat) (hnodup : (start :: c').Nodup)
    (hcl : ∀ y ∈ start :: c', ∀ e ∈ items, y ∈ e → ∀ z ∈ e, z ∈ start :: c')
    (hconn : ∀ w ∈ start :: c', Reach items start w)
    (hsum : sumInc (start :: c') inc ≤ (items.map List.length).sum) :
    (connectorGreedy items inc (start :: c')).1.Perm (start :: c') ∧
    ∀ p, p ≤ (connectorGreedy items inc (start :: c')).1.length →
      p ≤ cntIn items ((connectorGreedy items inc (start :: c')).1.take p) + 1 := by
  have hG := ginv_init (c := start :: c') hinc start List.mem_cons_self
  have hpot : ((inc.getD start []).reverse).length + sumInc (start :: c') inc ≤
      ((items.map List.length).sum + 1) + sumInc [start] inc := by
    have h1 : sumInc [start] inc = (inc.getD start []).length := by simp [sumInc]
    simp only [List.length_reverse]
    omega
  obtain ⟨O, F, heq, hnd, hsubc, hcov, hpref⟩ :=
    greedy_loop_spec hinc hlen hcl hnodup start hconn ((items.map List.length).sum + 1)
      ((inc.getD start []).reverse) ((∅ : Std.HashSet Nat).insert start) [start] false hG
      (by simp [Std.HashSet.contains_insert]) hpot
  have hres : connectorGreedy items inc (start :: c') = (O.reverse, F) := by
    unfold connectorGreedy
    exact heq
  rw [hres]
  dsimp only
  refine ⟨?_, ?_⟩
  · exact (List.perm_ext_iff_of_nodup (List.nodup_reverse.2 hnd) hnodup).2
      (fun a => ⟨fun h => hsubc a (List.mem_reverse.1 h), fun h => List.mem_reverse.2 (hcov a h)⟩)
  · intro p hp
    rw [List.length_reverse] at hp
    exact hpref p hp


/-! ## Components and excesses -/

theorem inner_getD (e : List Nat) (k x d : Nat) : ∀ (m : Std.HashMap Nat Nat),
    (e.foldl (fun (m : Std.HashMap Nat Nat) y => m.insert y k) m).getD x d =
      if x ∈ e then k else m.getD x d := by
  induction e with
  | nil => intro m; simp
  | cons y e ih =>
    intro m
    rw [List.foldl_cons, ih]
    by_cases hxy : y = x
    · subst hxy
      simp [Std.HashMap.getD_insert]
    · have hne : (y == x) = false := by simpa using hxy
      simp [Std.HashMap.getD_insert, hne, Ne.symm hxy]

theorem fold_idx_gen (j : Nat) (x d : Nat) : ∀ (L : List (List Nat × Nat)) (m : Std.HashMap Nat Nat),
    (∀ p ∈ L, x ∈ p.1 → p.2 = j) → (m.getD x d = j ∨ ∃ p ∈ L, x ∈ p.1) →
    (L.foldl (fun (m : Std.HashMap Nat Nat) (p : List Nat × Nat) =>
      p.1.foldl (fun (m : Std.HashMap Nat Nat) y => m.insert y p.2) m) m).getD x d = j := by
  intro L
  induction L with
  | nil =>
    intro m _ h
    rcases h with h | ⟨p, hp, _⟩
    · simpa using h
    · simp at hp
  | cons p L ih =>
    intro m hu h
    rw [List.foldl_cons]
    apply ih
    · intro q hq hxq
      exact hu q (List.mem_cons_of_mem _ hq) hxq
    · by_cases hxp : x ∈ p.1
      · left
        rw [inner_getD, if_pos hxp]
        exact hu p List.mem_cons_self hxp
      · rw [inner_getD, if_neg hxp]
        rcases h with h | ⟨q, hq, hxq⟩
        · exact Or.inl h
        · rcases List.mem_cons.1 hq with rfl | hq
          · exact absurd hxq hxp
          · exact Or.inr ⟨q, hq, hxq⟩

theorem fold_cnt (g : Nat → Nat) (i : Nat) : ∀ (hs : List Nat) (m : Std.HashMap Nat Nat),
    (hs.foldl (fun (m : Std.HashMap Nat Nat) x => m.insert (g x) (m.getD (g x) 0 + 1)) m).getD i 0 =
      m.getD i 0 + (hs.filter (fun x => g x == i)).length := by
  intro hs
  induction hs with
  | nil => intro m; simp
  | cons x hs ih =>
    intro m
    rw [List.foldl_cons, ih]
    by_cases hgi : g x = i
    · subst hgi
      simp [Std.HashMap.getD_insert, List.filter_cons]
      omega
    · have hne : (g x == i) = false := by simpa using hgi
      simp [Std.HashMap.getD_insert, hne, List.filter_cons, hgi]

theorem head_count (C : List Nat) (g : Nat → Nat) (i : Nat) : ∀ (L : List (List Nat)),
    (∀ e ∈ L, e ≠ []) → (∀ e ∈ L, ∀ h, e.head? = some h → (g h == i) = subsetB e C) →
    ((L.filterMap List.head?).filter (fun x => g x == i)).length =
      (L.filter (fun e => subsetB e C)).length := by
  intro L
  induction L with
  | nil => simp
  | cons e L ih =>
    intro hne hc
    have ih' := ih (fun e' he' => hne e' (List.mem_cons_of_mem _ he'))
      (fun e' he' h hh => hc e' (List.mem_cons_of_mem _ he') h hh)
    cases hh : e.head? with
    | none =>
      exfalso
      cases e with
      | nil => exact hne [] List.mem_cons_self rfl
      | cons a t => simp at hh
    | some h =>
      have hcond := hc e List.mem_cons_self h hh
      rw [List.filterMap_cons, hh, List.filter_cons, List.filter_cons, hcond]
      by_cases hb : subsetB e C = true
      · simp [hb, ih']
      · simp [hb, ih']

/-- The map `x ↦ index of the component containing x` built by `connectorExcess`. -/
def idxMapL (comps : List (List Nat)) : Std.HashMap Nat Nat :=
  comps.zipIdx.foldl (fun (m : Std.HashMap Nat Nat) (p : List Nat × Nat) =>
    p.1.foldl (fun (m : Std.HashMap Nat Nat) y => m.insert y p.2) m) ∅

/-- The counts `cnt` built by `connectorExcess` (heads of the items, by component index). -/
def cntMapL (items : List (List Nat)) (comps : List (List Nat)) : Std.HashMap Nat Nat :=
  (items.filterMap List.head?).foldl (fun (m : Std.HashMap Nat Nat) x =>
    m.insert ((idxMapL comps).getD x 0) (m.getD ((idxMapL comps).getD x 0) 0 + 1)) ∅

theorem connectorExcess_eq (items : List (List Nat)) (comps : List (List Nat)) :
    connectorExcess items comps = comps.zipIdx.map (fun p =>
      ((p.1.length : Nat) : ℤ) - (((cntMapL items comps).getD p.2 0 : Nat) : ℤ)) := rfl

/-- Index-form of `connectorExcess`: the component `c` has excess `|c| - #items in c`. -/
theorem excess_eq_gen (items : List (List Nat)) (comps : List (List Nat))
    (hne : ∀ e ∈ items, e ≠ [])
    (hdisj : comps.Pairwise (fun c c' => ∀ y ∈ c, y ∉ c'))
    (hcov : ∀ e ∈ items, ∀ z ∈ e, ∃ c ∈ comps, z ∈ c)
    (hclosed : ∀ c ∈ comps, ∀ y ∈ c, ∀ e ∈ items, y ∈ e → ∀ z ∈ e, z ∈ c) :
    connectorExcess items comps =
      comps.map (fun c => ((c.length : Nat) : ℤ) - ((cntIn items c : Nat) : ℤ)) := by
  -- disjointness of components by index
  have hdi : ∀ i j x, i ≠ j → x ∈ comps.getD i [] → x ∈ comps.getD j [] → False := by
    intro i j x hij hi hj
    rw [List.pairwise_iff_getElem] at hdisj
    by_cases hi' : i < comps.length
    · by_cases hj' : j < comps.length
      · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hi'] at hi
        rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hj'] at hj
        simp only [Option.getD_some] at hi hj
        rcases Nat.lt_or_gt_of_ne hij with h | h
        · exact hdisj i j hi' hj' h x hi hj
        · exact hdisj j i hj' hi' h x hj hi
      · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)] at hj
        simp at hj
    · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)] at hi
      simp at hi
  -- the index map
  have hidx : ∀ j, j < comps.length → ∀ x, x ∈ comps.getD j [] →
      (idxMapL comps).getD x 0 = j := by
    intro j hj x hx
    unfold idxMapL
    refine fold_idx_gen j x 0 comps.zipIdx ∅ ?_ (Or.inr ⟨(comps.getD j [], j), ?_, hx⟩)
    · intro p hp hxp
      have hp' : comps.getD p.2 [] = p.1 := by
        rw [List.getD_eq_getElem?_getD, List.mem_zipIdx_iff_getElem?.1 hp]
        simp
      by_contra hne'
      exact hdi p.2 j x hne' (by rw [hp']; exact hxp) hx
    · rw [List.mem_zipIdx_iff_getElem?, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hj]
      simp
  -- the counts
  have hcomp_mem : ∀ j, j < comps.length → comps.getD j [] ∈ comps := by
    intro j hj
    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hj]
    simpa using List.getElem_mem hj
  have hcnt : ∀ j, j < comps.length →
      (cntMapL items comps).getD j 0 = cntIn items (comps.getD j []) := by
    intro j hj
    have hC : comps.getD j [] ∈ comps := hcomp_mem j hj
    have hhead : ∀ e ∈ items, ∀ h, e.head? = some h →
        ((idxMapL comps).getD h 0 == j) = subsetB e (comps.getD j []) := by
      intro e he h hh
      have hmem : h ∈ e := by
        cases e with
        | nil => simp at hh
        | cons a t =>
          simp only [List.head?_cons, Option.some.injEq] at hh
          subst hh
          exact List.mem_cons_self
      apply Bool.eq_iff_iff.2
      rw [subsetB_iff, beq_iff_eq]
      constructor
      · intro hidxj
        obtain ⟨c, hc, hhc⟩ := hcov e he h hmem
        obtain ⟨k, hk, hck⟩ := List.mem_iff_getElem.1 hc
        have hget : comps.getD k [] = c := by
          rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hk]
          simpa using hck
        have hidxk : (idxMapL comps).getD h 0 = k := hidx k hk h (by rw [hget]; exact hhc)
        have hkj : k = j := by rw [← hidxk]; exact hidxj
        have hcC : h ∈ comps.getD j [] := by rw [← hkj, hget]; exact hhc
        intro z hz
        exact hclosed _ hC h hcC e he hmem z hz
      · intro hsub
        exact hidx j hj h (hsub h hmem)
    have hne' : ∀ e ∈ items, e ≠ [] := hne
    unfold cntMapL
    rw [fold_cnt (fun x => (idxMapL comps).getD x 0) j _ ∅]
    rw [Std.HashMap.getD_empty, zero_add, cntIn_eq_filter]
    exact head_count (comps.getD j []) (fun x => (idxMapL comps).getD x 0) j items hne' hhead
  rw [connectorExcess_eq]
  conv_rhs => rw [← List.zipIdx_map_fst 0 comps]
  rw [List.map_map]
  apply List.map_congr_left
  intro p hp
  have hp1 := List.mem_zipIdx_iff_getElem?.1 hp
  obtain ⟨hlt, _⟩ := List.getElem?_eq_some_iff.1 hp1
  have hpc : p.1 = comps.getD p.2 [] := by
    rw [List.getD_eq_getElem?_getD, hp1]
    simp
  show _ = ((p.1.length : Nat) : ℤ) - ((cntIn items p.1 : Nat) : ℤ)
  rw [hcnt p.2 hlt, ← hpc]


/-! ## The main induction over the sorted blocks -/

/-- Excess of a block: `|C| - #items inside C`. -/
def exOf (items : List (List Nat)) (C : List Nat) : ℤ := (C.length : ℤ) - (cntIn items C : ℤ)

theorem max_aux (a : ℤ) (L : List ℤ) (h : ∀ x ∈ L, a ≤ x) :
    a + max 0 L.sum ≤ max 0 (a + L.sum) := by
  rcases le_total a 0 with ha | ha
  · rcases le_total 0 L.sum with hs | hs
    · rw [max_eq_right hs]
      exact le_max_right _ _
    · rw [max_eq_left hs]
      linarith [le_max_left (0:ℤ) (a + L.sum)]
  · have hS : 0 ≤ L.sum := List.sum_nonneg (fun x hx => le_trans ha (h x hx))
    rw [max_eq_right hS, max_eq_right (by linarith : (0:ℤ) ≤ a + L.sum)]

theorem cntIn_nil {items : List (List Nat)} (hne : ∀ e ∈ items, e ≠ []) :
    cntIn items [] = 0 := by
  unfold cntIn
  rw [List.countP_eq_zero]
  intro e he h
  rw [subsetB_iff] at h
  obtain ⟨z, hz⟩ : ∃ z, z ∈ e := List.exists_mem_of_ne_nil _ (hne e he)
  exact List.not_mem_nil (h z hz)

/-- Items inside a union of pairwise separated closed blocks: additivity. -/
theorem cntIn_flatten {items : List (List Nat)} (hne : ∀ e ∈ items, e ≠ []) :
    ∀ (bs : List (List Nat)),
      (∀ C ∈ bs, ∀ e ∈ items, (∃ z ∈ e, z ∈ C) → ∀ w ∈ e, w ∈ C) →
      bs.Pairwise (fun C D => ∀ y ∈ C, y ∉ D) →
      cntIn items bs.flatten = (bs.map (cntIn items)).sum := by
  intro bs
  induction bs with
  | nil => intro _ _; simp [cntIn_nil hne]
  | cons B bs ih =>
    intro hcl hdisj
    have ih' := ih (fun C hC => hcl C (List.mem_cons_of_mem _ hC)) hdisj.of_cons
    rw [List.flatten_cons, List.map_cons, List.sum_cons, ← ih']
    apply cntIn_append hne
    · intro x hx hxF
      obtain ⟨l, hl, hxl⟩ := List.mem_flatten.1 hxF
      exact (List.pairwise_cons.1 hdisj).1 l hl x hx hxl
    · intro e he h
      by_cases hz : ∃ z ∈ e, z ∈ B
      · left
        obtain ⟨z, hze, hzB⟩ := hz
        exact fun w hw => hcl B List.mem_cons_self e he ⟨z, hze, hzB⟩ w hw
      · right
        intro w hw
        rcases List.mem_append.1 (h w hw) with h1 | h1
        · exact absurd ⟨w, hw, h1⟩ hz
        · exact h1

/-- The main induction (`lem:connector-linear`, proof of Equation (8.3) (`eq:cubic-connector`)): along a
list of blocks sorted by excess, every prefix `P` of the output satisfies
`|P| - c(P) ≤ max 0 (total excess) + 1`. -/
theorem mc_ind (items : List (List Nat)) (hne : ∀ e ∈ items, e ≠ []) (g : List Nat → List Nat) :
    ∀ bs : List (List Nat),
      (∀ C ∈ bs, (g C).Perm C ∧ (∀ p, p ≤ (g C).length → p ≤ cntIn items ((g C).take p) + 1) ∧
        (∀ e ∈ items, (∃ z ∈ e, z ∈ C) → ∀ w ∈ e, w ∈ C)) →
      bs.Pairwise (fun C D => ∀ y ∈ C, y ∉ D) →
      bs.Pairwise (fun C D => exOf items C ≤ exOf items D) →
      ∀ j, j ≤ (bs.map g).flatten.length →
        (j : ℤ) - (cntIn items ((bs.map g).flatten.take j) : ℤ) ≤
          max 0 ((bs.map (exOf items)).sum) + 1 := by
  intro bs
  induction bs with
  | nil =>
    intro _ _ _ j hj
    have hj0 : j = 0 := by simp at hj; exact hj
    subst hj0
    simp
  | cons B bs ih =>
    intro hgr hdisj hsorted j hj
    obtain ⟨hperm, hpref, hclB⟩ := hgr B List.mem_cons_self
    have ih' := ih (fun C hC => hgr C (List.mem_cons_of_mem _ hC)) hdisj.of_cons
      hsorted.of_cons
    have hhead : ∀ D ∈ bs, exOf items B ≤ exOf items D := (List.pairwise_cons.1 hsorted).1
    have hF : ∀ x ∈ (bs.map g).flatten, ∃ D ∈ bs, x ∈ D := by
      intro x hx
      obtain ⟨l, hl, hxl⟩ := List.mem_flatten.1 hx
      obtain ⟨D, hD, rfl⟩ := List.mem_map.1 hl
      exact ⟨D, hD, (hgr D (List.mem_cons_of_mem _ hD)).1.mem_iff.1 hxl⟩
    have hsumeq : (((B :: bs).map (exOf items)).sum) = exOf items B + (bs.map (exOf items)).sum := by
      simp [List.map_cons, List.sum_cons]
    rw [List.map_cons, List.flatten_cons] at hj ⊢
    rw [hsumeq]
    by_cases hj1 : j ≤ (g B).length
    · rw [List.take_append_of_le_length hj1]
      have h1 := hpref j hj1
      have h2 : (j : ℤ) ≤ (cntIn items ((g B).take j) : ℤ) + 1 := by exact_mod_cast h1
      have h3 : (0 : ℤ) ≤ max 0 (exOf items B + (bs.map (exOf items)).sum) := le_max_left _ _
      linarith
    · push_neg at hj1
      set k := j - (g B).length with hk
      have hjk : j = (g B).length + k := by omega
      have hk_le : k ≤ ((bs.map g).flatten).length := by
        rw [List.length_append] at hj; omega
      have htake : ((g B) ++ (bs.map g).flatten).take j = (g B) ++ ((bs.map g).flatten).take k := by
        rw [List.take_append, List.take_of_length_le (le_of_lt hj1), hk]
      rw [htake]
      have hdisjP : ∀ x ∈ g B, x ∉ ((bs.map g).flatten).take k := by
        intro x hx hxT
        obtain ⟨D, hD, hxD⟩ := hF x (List.mem_of_mem_take hxT)
        have hxB : x ∈ B := (hperm.mem_iff).1 hx
        exact (List.pairwise_cons.1 hdisj).1 D hD x hxB hxD
      have hsplit : ∀ e ∈ items, (∀ z ∈ e, z ∈ g B ++ ((bs.map g).flatten).take k) →
          (∀ z ∈ e, z ∈ g B) ∨ (∀ z ∈ e, z ∈ ((bs.map g).flatten).take k) := by
        intro e he h
        by_cases hz : ∃ z ∈ e, z ∈ g B
        · left
          obtain ⟨z, hze, hzg⟩ := hz
          have hzB : z ∈ B := hperm.mem_iff.1 hzg
          have hall := hclB e he ⟨z, hze, hzB⟩
          intro w hw
          rcases List.mem_append.1 (h w hw) with h1 | h1
          · exact h1
          · exfalso
            obtain ⟨D, hD, hwD⟩ := hF w (List.mem_of_mem_take h1)
            exact (List.pairwise_cons.1 hdisj).1 D hD w (hall w hw) hwD
        · right
          intro w hw
          rcases List.mem_append.1 (h w hw) with h1 | h1
          · exact absurd ⟨w, hw, h1⟩ hz
          · exact h1
      have hcnt := cntIn_append (items := items) (X := g B)
        (Y := ((bs.map g).flatten).take k) hne hdisjP hsplit
      rw [hcnt, cntIn_congr (fun z => hperm.mem_iff)]
      have hIH := ih' k hk_le
      have hlen : (g B).length = B.length := hperm.length_eq
      have hA := max_aux (exOf items B) ((bs.map (exOf items))) (by
        intro x hx
        obtain ⟨D, hD, rfl⟩ := List.mem_map.1 hx
        exact hhead D hD)
      have hex : exOf items B = (B.length : ℤ) - (cntIn items B : ℤ) := rfl
      have hmain : (j : ℤ) - ((cntIn items B + cntIn items (((bs.map g).flatten).take k) : Nat) : ℤ) =
          exOf items B + ((k : ℤ) - (cntIn items (((bs.map g).flatten).take k) : ℤ)) := by
        rw [hex, hjk, hlen]
        push_cast
        ring_nf
      rw [hmain]
      linarith [hA, hIH]


/-! ## Assembly -/

/-- The components of the connector (the list computed inside `connectorOrderF`). -/
def compsOf (Qs : List Nat) (items : List (List Nat)) : List (List Nat) :=
  connectorComponents Qs items (connectorIncidence Qs items)

theorem compsOf_props {Qs : List Nat} {items : List (List Nat)}
    (hitems : ∀ e ∈ items, ∀ z ∈ e, z ∈ Qs) :
    (∀ c ∈ compsOf Qs items, ∃ r c', c = r :: c' ∧ ∀ w ∈ c, Reach items r w) ∧
    (∀ c ∈ compsOf Qs items, c.Nodup) ∧
    (∀ c ∈ compsOf Qs items, ∀ y ∈ c, y ∈ Qs) ∧
    (∀ c ∈ compsOf Qs items, ∀ y ∈ c, ∀ e ∈ items, y ∈ e → ∀ z ∈ e, z ∈ c) ∧
    (compsOf Qs items).Pairwise (fun c c' => ∀ y ∈ c, y ∉ c') ∧
    (∀ x ∈ Qs, ∃ c ∈ compsOf Qs items, x ∈ c) := by
  have hO0 : OInv items Qs (∅ : Std.HashSet Nat) [] :=
    ⟨by simp, by simp, by simp, by simp, List.Pairwise.nil,
      fun e _ h => by obtain ⟨z, _, hz⟩ := h; simp at hz,
      fun w => by simp⟩
  have hinc : ∀ k y, k ∈ (connectorIncidence Qs items).getD y [] ↔ y ∈ items.getD k [] :=
    fun k y => inc_mem Qs items y k
  obtain ⟨C, A', heq, hO, hsub, hcov⟩ :=
    connOuter_spec (fuel := Qs.length + (items.map List.length).sum + 1) hitems hinc
      (by omega) Qs ∅ [] hO0 (fun y hy => hy)
  have hcomps : compsOf Qs items = C.reverse := by
    unfold compsOf connectorComponents
    exact heq
  rw [hcomps]
  refine ⟨fun c hc => hO.reach c (List.mem_reverse.1 hc),
    fun c hc => hO.nodup c (List.mem_reverse.1 hc),
    fun c hc => hO.sub c (List.mem_reverse.1 hc),
    fun c hc => hO.closed c (List.mem_reverse.1 hc), ?_, fun x hx => ?_⟩
  · exact List.pairwise_reverse.2 (List.Pairwise.imp (fun h y hyb hya => h y hya hyb) hO.disj)
  · obtain ⟨c, hc, hxc⟩ := hcov x hx
    exact ⟨c, List.mem_reverse.2 hc, hxc⟩

theorem exOf_sum (items : List (List Nat)) : ∀ L : List (List Nat),
    (L.map (exOf items)).sum = ((L.map List.length).sum : ℤ) - ((L.map (cntIn items)).sum : ℤ) := by
  intro L
  induction L with
  | nil => simp
  | cons C L ih =>
    simp only [List.map_cons, List.sum_cons, ih, exOf]
    push_cast
    ring

theorem cntIn_all {items : List (List Nat)} {Qs : List Nat}
    (h : ∀ e ∈ items, ∀ z ∈ e, z ∈ Qs) : cntIn items Qs = items.length := by
  unfold cntIn
  apply List.countP_eq_length.2
  intro e he
  rw [subsetB_iff]
  exact fun z hz => h e he z hz

theorem connectorOrder_eq (Qs : List Nat) (items : List (List Nat)) :
    connectorOrder Qs items =
      ((((List.range (compsOf Qs items).length).zip
          (connectorExcess items (compsOf Qs items))).mergeSort
            (fun a b => decide (a.2 ≤ b.2))).map
        (fun p => (connectorGreedy items (connectorIncidence Qs items)
          ((compsOf Qs items).getD p.1 [])).1)).flatten := by
  unfold connectorOrder connectorOrderF compsOf
  dsimp only
  rw [List.flatMap_map]
  rfl

/-- Greedy order of one block. -/
def gOf (items : List (List Nat)) (Qs : List Nat) (C : List Nat) : List Nat :=
  (connectorGreedy items (connectorIncidence Qs items) C).1

/-- The sorted list of (component index, excess). -/
def orderedOf (Qs : List Nat) (items : List (List Nat)) : List (Nat × Int) :=
  ((List.range (compsOf Qs items).length).zip
    (connectorExcess items (compsOf Qs items))).mergeSort (fun a b => decide (a.2 ≤ b.2))

/-- The blocks of the connector, sorted by excess. -/
def blocksOf (Qs : List Nat) (items : List (List Nat)) : List (List Nat) :=
  (orderedOf Qs items).map (fun p => (compsOf Qs items).getD p.1 [])

theorem connectorOrder_eq' (Qs : List Nat) (items : List (List Nat)) :
    connectorOrder Qs items = ((blocksOf Qs items).map (gOf items Qs)).flatten := by
  rw [connectorOrder_eq, blocksOf, List.map_map]
  rfl

theorem connector_main (Qs : List Nat) (items : List (List Nat)) (hQ : Qs.Nodup)
    (hitems : ∀ e ∈ items, e.Nodup ∧ 1 ≤ e.length ∧ e.length ≤ 2 ∧ ∀ z ∈ e, z ∈ Qs) :
    (connectorOrder Qs items).Perm Qs ∧
      ∀ j, j ≤ Qs.length →
        (j : ℤ) - ((items.filter fun e => subsetB e ((connectorOrder Qs items).take j)).length : ℤ)
          ≤ max 0 ((Qs.length : ℤ) - (items.length : ℤ)) + 1 := by
  have hitQ : ∀ e ∈ items, ∀ z ∈ e, z ∈ Qs := fun e he z hz => (hitems e he).2.2.2 z hz
  have hne : ∀ e ∈ items, e ≠ [] := by
    intro e he h
    have := (hitems e he).2.1
    rw [h] at this
    simp at this
  have hlen2 : ∀ e ∈ items, e.length ≤ 2 := fun e he => (hitems e he).2.2.1
  obtain ⟨hreach, hnodupC, hsubC, hclosedC, hdisjC, hcovC⟩ := compsOf_props hitQ
  have hexc := excess_eq_gen items (compsOf Qs items) hne hdisjC
    (fun e he z hz => hcovC z (hitQ e he z hz)) hclosedC
  have hexc_len : (connectorExcess items (compsOf Qs items)).length = (compsOf Qs items).length := by
    rw [hexc, List.length_map]
  -- the blocks are a permutation of the components
  have hnd_map : ((List.range (compsOf Qs items).length).zip
      (connectorExcess items (compsOf Qs items))).map (fun p => (compsOf Qs items).getD p.1 []) =
      compsOf Qs items := by
    have h1 : ((List.range (compsOf Qs items).length).zip
        (connectorExcess items (compsOf Qs items))).map Prod.fst =
        List.range (compsOf Qs items).length :=
      List.map_fst_zip (by simp [hexc_len])
    calc _ = (((List.range (compsOf Qs items).length).zip
          (connectorExcess items (compsOf Qs items))).map Prod.fst).map
            (fun i => (compsOf Qs items).getD i []) := by
          rw [List.map_map]; rfl
      _ = (List.range (compsOf Qs items).length).map (fun i => (compsOf Qs items).getD i []) := by
          rw [h1]
      _ = compsOf Qs items := by
          apply List.ext_getElem
          · simp
          · intro i h1 h2
            simp [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem h2]
  have hbl_perm : (blocksOf Qs items).Perm (compsOf Qs items) := by
    have h := ((List.mergeSort_perm ((List.range (compsOf Qs items).length).zip
      (connectorExcess items (compsOf Qs items))) (fun a b => decide (a.2 ≤ b.2))).map
      (fun p => (compsOf Qs items).getD p.1 []))
    rw [hnd_map] at h
    exact h
  have hbl_mem : ∀ C ∈ blocksOf Qs items, C ∈ compsOf Qs items :=
    fun C hC => hbl_perm.mem_iff.1 hC
  have hbl_disj : (blocksOf Qs items).Pairwise (fun C D => ∀ y ∈ C, y ∉ D) :=
    (List.Perm.pairwise_iff (fun {x y} h z hz hzx => h z hzx hz) hbl_perm).2 hdisjC
  -- excesses
  have hexc_getD : ∀ k, (connectorExcess items (compsOf Qs items)).getD k 0 =
      exOf items ((compsOf Qs items).getD k []) := by
    intro k
    rw [hexc]
    by_cases hk : k < (compsOf Qs items).length
    · rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getD_eq_getElem?_getD,
        List.getElem?_eq_getElem hk]
      simp [exOf]
    · rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getD_eq_getElem?_getD,
        List.getElem?_eq_none (by omega)]
      simp [exOf, cntIn_nil hne]
  have hval : ∀ p ∈ orderedOf Qs items, exOf items ((compsOf Qs items).getD p.1 []) = p.2 := by
    intro p hp
    have hp' : p ∈ (List.range (compsOf Qs items).length).zip
        (connectorExcess items (compsOf Qs items)) := (List.mergeSort_perm _ _).mem_iff.1 hp
    obtain ⟨k, hk, hkp⟩ := List.mem_iff_getElem.1 hp'
    have hkn : k < (connectorExcess items (compsOf Qs items)).length := by
      have h2 := hk
      rw [List.length_zip, List.length_range] at h2
      omega
    have e1 : p.1 = k := by rw [← hkp]; simp
    have e2 : p.2 = (connectorExcess items (compsOf Qs items)).getD k 0 := by
      rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hkn, ← hkp]
      simp
    rw [e1, e2, hexc_getD]
  have hsort : (orderedOf Qs items).Pairwise (fun a b => decide (a.2 ≤ b.2) = true) := by
    apply List.pairwise_mergeSort
    · intro a b c h1 h2
      simp only [decide_eq_true_eq] at h1 h2 ⊢
      exact le_trans h1 h2
    · intro a b
      simp only [Bool.or_eq_true, decide_eq_true_eq]
      exact le_total _ _
  have hbl_sorted : (blocksOf Qs items).Pairwise (fun C D => exOf items C ≤ exOf items D) := by
    unfold blocksOf
    rw [List.pairwise_map]
    exact hsort.imp_of_mem (fun {a b} ha hb hab => by
      show exOf items ((compsOf Qs items).getD a.1 []) ≤ exOf items ((compsOf Qs items).getD b.1 [])
      rw [hval a ha, hval b hb]
      simpa using hab)
  -- blocks: greedy orders
  have hblock : ∀ C ∈ compsOf Qs items, (gOf items Qs C).Perm C ∧
      ∀ p, p ≤ (gOf items Qs C).length → p ≤ cntIn items ((gOf items Qs C).take p) + 1 := by
    intro C hC
    obtain ⟨r, c', hCeq, hr⟩ := hreach C hC
    subst hCeq
    have hsum : sumInc (r :: c') (connectorIncidence Qs items) ≤ (items.map List.length).sum :=
      sumInc_incidence Qs items (r :: c') (hnodupC _ hC)
    exact greedy_out (fun k y => inc_mem Qs items y k) hlen2 r c' (hnodupC _ hC)
      (hclosedC _ hC) hr hsum
  have hgr : ∀ C ∈ blocksOf Qs items, (gOf items Qs C).Perm C ∧
      (∀ p, p ≤ (gOf items Qs C).length → p ≤ cntIn items ((gOf items Qs C).take p) + 1) ∧
      (∀ e ∈ items, (∃ z ∈ e, z ∈ C) → ∀ w ∈ e, w ∈ C) := by
    intro C hC
    obtain ⟨h1, h2⟩ := hblock C (hbl_mem C hC)
    refine ⟨h1, h2, fun e he hex w hw => ?_⟩
    obtain ⟨z, hz, hzC⟩ := hex
    exact hclosedC C (hbl_mem C hC) z hzC e he hz w hw
  have hmc := mc_ind items hne (gOf items Qs) (blocksOf Qs items) hgr hbl_disj hbl_sorted
  -- the output is a permutation of Qs
  have hnd : ((blocksOf Qs items).map (gOf items Qs)).flatten.Nodup := by
    rw [List.nodup_flatten]
    constructor
    · intro l hl
      obtain ⟨C, hC, rfl⟩ := List.mem_map.1 hl
      exact (hblock C (hbl_mem C hC)).1.nodup_iff.2 (hnodupC C (hbl_mem C hC))
    · rw [List.pairwise_map]
      exact hbl_disj.imp_of_mem (fun {C D} hC hD hCD => by
        intro a ha hb
        exact hCD a ((hblock C (hbl_mem C hC)).1.mem_iff.1 ha)
          ((hblock D (hbl_mem D hD)).1.mem_iff.1 hb))
  have hPerm : (connectorOrder Qs items).Perm Qs := by
    rw [connectorOrder_eq']
    exact (List.perm_ext_iff_of_nodup hnd hQ).2 (fun x => by
      rw [← connectorOrder_eq']
      exact connectorOrderMem Qs items hitQ x)
  have hlenFlat : ((blocksOf Qs items).map (gOf items Qs)).flatten.length = Qs.length := by
    rw [← connectorOrder_eq']
    exact hPerm.length_eq
  have hlenBl : ((blocksOf Qs items).map List.length).sum = Qs.length := by
    rw [← hlenFlat, List.length_flatten, List.map_map]
    congr 1
    apply List.map_congr_left
    intro C hC
    exact ((hblock C (hbl_mem C hC)).1.length_eq).symm
  -- sums of excesses
  have hcntFlat : cntIn items (blocksOf Qs items).flatten = cntIn items Qs := by
    apply cntIn_congr
    intro z
    rw [List.mem_flatten]
    constructor
    · rintro ⟨C, hC, hzC⟩
      exact hsubC C (hbl_mem C hC) z hzC
    · intro hz
      obtain ⟨c, hc, hzc⟩ := hcovC z hz
      exact ⟨c, hbl_perm.symm.mem_iff.1 hc, hzc⟩
  have hsumEx : ((blocksOf Qs items).map (exOf items)).sum =
      (Qs.length : ℤ) - (items.length : ℤ) := by
    rw [exOf_sum, hlenBl]
    have hc1 : ((blocksOf Qs items).map (cntIn items)).sum = items.length := by
      rw [← cntIn_flatten hne (blocksOf Qs items) (fun C hC => (hgr C hC).2.2) hbl_disj,
        hcntFlat, cntIn_all hitQ]
    rw [hc1]
  -- conclusion
  refine ⟨hPerm, fun j hj => ?_⟩
  rw [connectorOrder_eq', ← cntIn_eq_filter]
  have hjl : j ≤ ((blocksOf Qs items).map (gOf items Qs)).flatten.length := by
    rw [hlenFlat]; exact hj
  have h := hmc j hjl
  rw [hsumEx] at h
  exact h

end L4

theorem connectorLemma10 : ConnectorLemma10 := by
  intro Qs items hQ hitems
  exact L4.connector_main Qs items hQ hitems

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.connectorLemma10