CubicPathwidth.Alg.Proofs2.R8Attach

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T4.TorsoDyn

/-!
# R8: attachment invariant (`AttachInvariant`) of a legal record

Depends on the Stage 2 plan interfaces `TorsoSim`, `RecordMono`, `ComponentsConnected`
(taken as hypotheses), and on Stage 1 graph facts and the torso
lemmas `T4.Good.attachment_card_le`, `T4.tgraph_adj_iff`, `T4.mem_components_of_conn`.
`OpsRecordCongr` and `OpsRecordAppend` are part of the signature but not needed.
-/

namespace CubicPathwidth.Alg

open Graph

namespace R8

/-- Subgraph: nodes and adjacency of `H` are among those of `G`. -/
def SubG (H G : Graph) : Prop :=
  (∀ x ∈ H.nodes, x ∈ G.nodes) ∧ ∀ u w, H.Adj u w → G.Adj u w

theorem subG_trans {A B C : Graph} (h1 : SubG A B) (h2 : SubG B C) : SubG A C :=
  ⟨fun x hx => h2.1 x (h1.1 x hx), fun u w h => h2.2 u w (h1.2 u w h)⟩

theorem wf_removeNode {G : Graph} (hG : G.WF) (v : Nat) : (G.removeNode v).WF :=
  (removeNodeSpec G v hG).1

theorem wf_addEdge {G : Graph} (hG : G.WF) {u v : Nat} (huv : u ≠ v) :
    (G.addEdge u v).WF :=
  (addEdgeSpec G u v hG huv).1

theorem mem_of_adj {G : Graph} (hG : G.WF) {u v : Nat} (h : G.Adj u v) :
    u ∈ G.nodes ∧ v ∈ G.nodes :=
  ⟨(wfBasics G hG u v h).1, (wfBasics G hG u v h).2.1⟩

theorem length_le_of_nodup_sub {l₁ l₂ : List Nat} (h1 : l₁.Nodup) (h : ∀ x ∈ l₁, x ∈ l₂) :
    l₁.length ≤ l₂.length :=
  (List.Nodup.subperm h1 (fun x hx => h x hx)).length_le

theorem ne_of_nbrs_pair {G : Graph} (hG : G.WF) {v a b : Nat} (heq : G.nbrs v = [a, b]) :
    a ≠ b := by
  have hnd := hG.nbrs_nodup v
  rw [heq] at hnd
  intro h
  subst h
  simp at hnd

theorem pair_of_mem_two {l : List Nat} (hl : l.length ≤ 2) {a b : Nat} (ha : a ∈ l)
    (hb : b ∈ l) (hab : a ≠ b) : ∃ x y, l = [x, y] := by
  match l, hl, ha, hb with
  | [], _, ha, _ => simp at ha
  | [x], _, ha, hb =>
    simp at ha hb
    exact absurd (ha.trans hb.symm) hab
  | [x, y], _, _, _ => exact ⟨x, y, rfl⟩
  | x :: y :: z :: w, hl, _, _ => simp at hl

/-! ## `redStep` -/

theorem redStep_eq_pair {G : Graph} {v a b : Nat} (h : G.nbrs v = [a, b]) :
    redStep G v = (G.removeNode v).addEdge a b := by
  unfold redStep
  rw [h]

theorem redStep_eq_not_pair {G : Graph} {v : Nat} (h : ¬ ∃ a b, G.nbrs v = [a, b]) :
    redStep G v = G.removeNode v := by
  unfold redStep
  split
  · rename_i a b heq
    exact absurd ⟨a, b, heq⟩ h
  · rfl

theorem redStep_wf {G : Graph} (hG : G.WF) (v : Nat) : (redStep G v).WF := by
  by_cases h : ∃ a b, G.nbrs v = [a, b]
  · obtain ⟨a, b, hab⟩ := h
    rw [redStep_eq_pair hab]
    exact wf_addEdge (wf_removeNode hG v) (ne_of_nbrs_pair hG hab)
  · rw [redStep_eq_not_pair h]
    exact wf_removeNode hG v

theorem redStep_nodes_sub {G : Graph} (hG : G.WF) (v x : Nat) (hx : x ∈ (redStep G v).nodes) :
    x ∈ G.nodes := by
  by_cases h : ∃ a b, G.nbrs v = [a, b]
  · obtain ⟨a, b, hab⟩ := h
    rw [redStep_eq_pair hab] at hx
    have hne := ne_of_nbrs_pair hG hab
    rcases (addEdgeSpec (G.removeNode v) a b (wf_removeNode hG v) hne).2.1 x |>.1 hx with hx | hx | hx
    · exact ((removeNodeSpec G v hG).2.1 x).1 hx |>.1
    · have ha : a ∈ G.nbrs v := by rw [hab]; simp
      rw [hx]; exact (mem_of_adj hG ha).2
    · have hb : b ∈ G.nbrs v := by rw [hab]; simp
      rw [hx]; exact (mem_of_adj hG hb).2
  · rw [redStep_eq_not_pair h] at hx
    exact ((removeNodeSpec G v hG).2.1 x).1 hx |>.1

theorem redStep_nodes_mem {G : Graph} (hG : G.WF) (v x : Nat) (hx : x ∈ G.nodes) (hxv : x ≠ v) :
    x ∈ (redStep G v).nodes := by
  have hK : x ∈ (G.removeNode v).nodes := ((removeNodeSpec G v hG).2.1 x).2 ⟨hx, hxv⟩
  by_cases h : ∃ a b, G.nbrs v = [a, b]
  · obtain ⟨a, b, hab⟩ := h
    rw [redStep_eq_pair hab]
    exact (addEdgeSpec (G.removeNode v) a b (wf_removeNode hG v) (ne_of_nbrs_pair hG hab)).2.1 x
      |>.2 (Or.inl hK)
  · rw [redStep_eq_not_pair h]
    exact hK

theorem redStep_adj_of {G : Graph} (hG : G.WF) (v u w : Nat) (hu : u ≠ v) (hw : w ≠ v)
    (h : G.Adj u w) : (redStep G v).Adj u w := by
  have hK : (G.removeNode v).Adj u w := (removeNodeSpec G v hG).2.2 u w |>.2 ⟨h, hu, hw⟩
  by_cases hp : ∃ a b, G.nbrs v = [a, b]
  · obtain ⟨a, b, hab⟩ := hp
    rw [redStep_eq_pair hab]
    exact (addEdgeSpec (G.removeNode v) a b (wf_removeNode hG v) (ne_of_nbrs_pair hG hab)).2.2 u w
      |>.2 (Or.inl hK)
  · rw [redStep_eq_not_pair hp]
    exact hK

theorem subG_addEdge {K : Graph} (hK : K.WF) {a b : Nat} (hab : a ≠ b) : SubG K (K.addEdge a b) :=
  ⟨fun x hx => (addEdgeSpec K a b hK hab).2.1 x |>.2 (Or.inl hx),
    fun u w h => (addEdgeSpec K a b hK hab).2.2 u w |>.2 (Or.inl h)⟩

theorem addEdge_sub {H K : Graph} {a b a' b' : Nat} (hH : SubG H K) (hHW : H.WF) (hK : K.WF)
    (hab : a ≠ b) (hab' : a' ≠ b') (h1 : (a' = a ∧ b' = b) ∨ (a' = b ∧ b' = a)) :
    SubG (H.addEdge a' b') (K.addEdge a b) := by
  constructor
  · intro x hx
    rw [(addEdgeSpec H a' b' hHW hab').2.1 x] at hx
    rw [(addEdgeSpec K a b hK hab).2.1 x]
    rcases hx with hx | hx | hx
    · exact Or.inl (hH.1 x hx)
    · rcases h1 with h1 | h1
      · exact Or.inr (Or.inl (hx.trans h1.1))
      · exact Or.inr (Or.inr (hx.trans h1.1))
    · rcases h1 with h1 | h1
      · exact Or.inr (Or.inr (hx.trans h1.2))
      · exact Or.inr (Or.inl (hx.trans h1.2))
  · intro u w h
    rw [(addEdgeSpec H a' b' hHW hab').2.2 u w] at h
    rw [(addEdgeSpec K a b hK hab).2.2 u w]
    rcases h with h | ⟨hu, hw⟩ | ⟨hu, hw⟩
    · exact Or.inl (hH.2 u w h)
    · rcases h1 with h1 | h1
      · exact Or.inr (Or.inl ⟨hu.trans h1.1, hw.trans h1.2⟩)
      · exact Or.inr (Or.inr ⟨hu.trans h1.1, hw.trans h1.2⟩)
    · rcases h1 with h1 | h1
      · exact Or.inr (Or.inr ⟨hu.trans h1.2, hw.trans h1.1⟩)
      · exact Or.inr (Or.inl ⟨hu.trans h1.2, hw.trans h1.1⟩)

/-- Pair of neighbours in `G` contained in a list of length at most two. -/
theorem redStep_sub {G G' : Graph} (v : Nat) (hG : G.WF) (hG' : G'.WF) (hS : SubG G' G)
    (hl : (G.nbrs v).length ≤ 2) : SubG (redStep G' v) (redStep G v) := by
  have hnb : ∀ x ∈ G'.nbrs v, x ∈ G.nbrs v := fun x hx => hS.2 v x hx
  have hlen' : (G'.nbrs v).length ≤ 2 :=
    le_trans (length_le_of_nodup_sub (hG'.nbrs_nodup v) hnb) hl
  have hH : SubG (G'.removeNode v) (G.removeNode v) := by
    constructor
    · intro x hx
      have hx' := ((removeNodeSpec G' v hG').2.1 x).1 hx
      exact ((removeNodeSpec G v hG).2.1 x).2 ⟨hS.1 x hx'.1, hx'.2⟩
    · intro u w h
      have h' := (removeNodeSpec G' v hG').2.2 u w |>.1 h
      exact (removeNodeSpec G v hG).2.2 u w |>.2 ⟨hS.2 u w h'.1, h'.2.1, h'.2.2⟩
  have hKW : (G.removeNode v).WF := wf_removeNode hG v
  by_cases hp : ∃ a b, G.nbrs v = [a, b]
  · obtain ⟨a, b, hab⟩ := hp
    have hne : a ≠ b := ne_of_nbrs_pair hG hab
    rw [redStep_eq_pair hab]
    by_cases hp' : ∃ a' b', G'.nbrs v = [a', b']
    · obtain ⟨a', b', hab'⟩ := hp'
      rw [redStep_eq_pair hab']
      have hne' : a' ≠ b' := ne_of_nbrs_pair hG' hab'
      have ha' : a' ∈ G.nbrs v := hnb a' (by rw [hab']; simp)
      have hb' : b' ∈ G.nbrs v := hnb b' (by rw [hab']; simp)
      rw [hab] at ha' hb'
      simp only [List.mem_cons, List.not_mem_nil, or_false] at ha' hb'
      have h1 : (a' = a ∧ b' = b) ∨ (a' = b ∧ b' = a) := by
        rcases ha' with ha' | ha' <;> rcases hb' with hb' | hb'
        · exact absurd (ha'.trans hb'.symm) hne'
        · exact Or.inl ⟨ha', hb'⟩
        · exact Or.inr ⟨ha', hb'⟩
        · exact absurd (ha'.trans hb'.symm) hne'
      exact addEdge_sub hH (wf_removeNode hG' v) hKW hne hne' h1
    · rw [redStep_eq_not_pair hp']
      exact subG_trans hH (subG_addEdge hKW hne)
  · rw [redStep_eq_not_pair hp]
    by_cases hp' : ∃ a' b', G'.nbrs v = [a', b']
    · exfalso
      obtain ⟨a', b', hab'⟩ := hp'
      have hne' : a' ≠ b' := ne_of_nbrs_pair hG' hab'
      have ha' : a' ∈ G.nbrs v := hnb a' (by rw [hab']; simp)
      have hb' : b' ∈ G.nbrs v := hnb b' (by rw [hab']; simp)
      obtain ⟨x, y, hxy⟩ := pair_of_mem_two hl ha' hb' hne'
      exact hp ⟨x, y, hxy⟩
    · rw [redStep_eq_not_pair hp']
      exact hH

/-- Every reached adjacency is between nodes of the final graph. -/
theorem opsRecord_adj_mem (ops : List Op) : ∀ (G R : Graph), G.WF → OpsRecord G ops R →
    ∀ u v, R.Adj u v → u ∈ R.nodes := by
  induction ops with
  | nil =>
    intro G R hG hrec u v h
    have hs : SameGraph G R := hrec
    exact (hs.1 u).1 (mem_of_adj hG ((hs.2 u v).2 h)).1
  | cons o ops ih =>
    intro G R hG hrec u v h
    cases o with
    | red w nb =>
      unfold OpsRecord at hrec
      exact ih (redStep G w) R (redStep_wf hG w) hrec.2.2.2.2 u v h
    | del w =>
      unfold OpsRecord at hrec
      exact ih (G.removeNode w) R (wf_removeNode hG w) hrec.2 u v h

/-- Changing the end graph by `SameGraph`. -/
theorem opsRecord_end_congr (ops : List Op) : ∀ (F R R2 : Graph), OpsRecord F ops R →
    SameGraph R R2 → OpsRecord F ops R2 := by
  induction ops with
  | nil =>
    intro F R R2 h h2
    have hs : SameGraph F R := h
    show SameGraph F R2
    exact ⟨fun v => (hs.1 v).trans (h2.1 v), fun u v => (hs.2 u v).trans (h2.2 u v)⟩
  | cons o ops ih =>
    intro F R R2 h h2
    cases o with
    | red w nb =>
      unfold OpsRecord at h ⊢
      exact ⟨h.1, h.2.1, h.2.2.1, h.2.2.2.1, ih _ _ _ h.2.2.2.2 h2⟩
    | del w =>
      unfold OpsRecord at h ⊢
      exact ⟨h.1, ih _ _ _ h.2 h2⟩

/-- Replay of a legal record on a subgraph avoiding its deleted vertices. -/
theorem replay (ops : List Op) : ∀ (G G' R : Graph), G.WF → G'.WF → SubG G' G →
    (∀ w, Op.del w ∈ ops → w ∉ G'.nodes) → OpsRecord G ops R →
    ∃ ops' R', RedOnly ops' ∧ OpsRecord G' ops' R' ∧
      (∀ v ∈ R'.nodes, v ∈ R.nodes) ∧ (∀ u v, R'.Adj u v → R.Adj u v) ∧
      (∀ v ∈ R'.nodes, v ∈ G'.nodes) := by
  induction ops with
  | nil =>
    intro G G' R hG hG' hS _ hrec
    have hs : SameGraph G R := hrec
    refine ⟨[], G', fun o ho => by simp at ho, ?_, ?_, ?_, fun v hv => hv⟩
    · show SameGraph G' G'
      exact ⟨fun _ => Iff.rfl, fun _ _ => Iff.rfl⟩
    · intro v hv; exact (hs.1 v).1 (hS.1 v hv)
    · intro u v h; exact (hs.2 u v).1 (hS.2 u v h)
  | cons o ops ih =>
    intro G G' R hG hG' hS hdel hrec
    cases o with
    | red v nb =>
      unfold OpsRecord at hrec
      obtain ⟨hvG, hnd, hlen, hadj, hrest⟩ := hrec
      have hl : (G.nbrs v).length ≤ 2 :=
        le_trans (length_le_of_nodup_sub (hG.nbrs_nodup v) (fun x hx => (hadj x).2 hx)) hlen
      by_cases hvG' : v ∈ G'.nodes
      · have hnb' : (G'.nbrs v).length ≤ 2 :=
          le_trans (length_le_of_nodup_sub (hG'.nbrs_nodup v)
            (fun x hx => (hadj x).2 (hS.2 v x hx))) hlen
        have hdel' : ∀ w, Op.del w ∈ ops → w ∉ (redStep G' v).nodes := by
          intro w hw hmem
          exact hdel w (List.mem_cons_of_mem _ hw) (redStep_nodes_sub hG' v w hmem)
        obtain ⟨ops'', R', hred, hrec2, h1, h2, h3⟩ :=
          ih (redStep G v) (redStep G' v) R (redStep_wf hG v) (redStep_wf hG' v)
            (redStep_sub v hG hG' hS hl) hdel' hrest
        refine ⟨Op.red v (G'.nbrs v) :: ops'', R', ?_, ?_, h1, h2, ?_⟩
        · intro o ho
          rcases List.mem_cons.1 ho with rfl | ho
          · exact ⟨v, G'.nbrs v, rfl⟩
          · exact hred o ho
        · unfold OpsRecord
          exact ⟨hvG', hG'.nbrs_nodup v, hnb', fun x => Iff.rfl, hrec2⟩
        · intro x hx
          exact redStep_nodes_sub hG' v x (h3 x hx)
      · have hS1 : SubG G' (redStep G v) := by
          constructor
          · intro x hx
            have hxv : x ≠ v := by
              rintro rfl
              exact hvG' hx
            exact redStep_nodes_mem hG v x (hS.1 x hx) hxv
          · intro u w h
            have hu := mem_of_adj hG' h
            have huv : u ≠ v := by
              rintro rfl
              exact hvG' hu.1
            have hwv : w ≠ v := by
              rintro rfl
              exact hvG' hu.2
            exact redStep_adj_of hG v u w huv hwv (hS.2 u w h)
        exact ih (redStep G v) G' R (redStep_wf hG v) hG' hS1
          (fun w hw => hdel w (List.mem_cons_of_mem _ hw)) hrest
    | del w =>
      unfold OpsRecord at hrec
      obtain ⟨_, hrest⟩ := hrec
      have hwG' : w ∉ G'.nodes := hdel w (by simp)
      have hS1 : SubG G' (G.removeNode w) := by
        constructor
        · intro x hx
          have hxw : x ≠ w := by
            rintro rfl
            exact hwG' hx
          exact ((removeNodeSpec G w hG).2.1 x).2 ⟨hS.1 x hx, hxw⟩
        · intro u x h
          have hu := mem_of_adj hG' h
          have huw : u ≠ w := by
            rintro rfl
            exact hwG' hu.1
          have hxw : x ≠ w := by
            rintro rfl
            exact hwG' hu.2
          exact (removeNodeSpec G w hG).2.2 u x |>.2 ⟨hS.2 u x h, huw, hxw⟩
      exact ih (G.removeNode w) G' R (wf_removeNode hG w) hG' hS1
        (fun x hx => hdel x (List.mem_cons_of_mem _ hx)) hrest

theorem le_sum_mem : ∀ (l : List ℕ) (x : ℕ), x ∈ l → x ≤ l.sum
  | [], x, h => by simp at h
  | a :: l, x, h => by
    simp only [List.sum_cons]
    rcases List.mem_cons.1 h with rfl | h
    · omega
    · have := le_sum_mem l x h
      omega

/-! ## `undoAttach` -/

theorem mem_inner (C D : List Nat) (y : Nat) (l : List Nat) : ∀ acc : List Nat,
    y ∈ l.foldl (fun acc x => if C.contains x || D.contains x || acc.contains x then acc
      else acc ++ [x]) acc ↔ y ∈ acc ∨ (y ∈ l ∧ y ∉ C ∧ y ∉ D) := by
  induction l with
  | nil => intro acc; simp
  | cons z zs ih =>
    intro acc
    rw [List.foldl_cons]
    rw [ih]
    by_cases hc : (C.contains z || D.contains z || acc.contains z) = true
    · rw [if_pos hc]
      simp only [List.contains, List.elem_eq_mem, decide_eq_true_eq, Bool.or_eq_true] at hc
      simp only [List.mem_cons]
      constructor
      · rintro (h | ⟨h1, h2, h3⟩)
        · exact Or.inl h
        · exact Or.inr ⟨Or.inr h1, h2, h3⟩
      · rintro (h | ⟨h1 | h1, h2, h3⟩)
        · exact Or.inl h
        · subst h1
          rcases hc with (h | h) | h
          · exact absurd h h2
          · exact absurd h h3
          · exact Or.inl h
        · exact Or.inr ⟨h1, h2, h3⟩
    · rw [if_neg hc]
      have hzC : z ∉ C := fun h => hc (by simp [h])
      have hzD : z ∉ D := fun h => hc (by simp [h])
      by_cases hyz : y = z
      · subst hyz
        simp [hzC, hzD]
      · simp [hyz]

theorem mem_outer (F : Graph) (C D : List Nat) (y : Nat) : ∀ (l : List Nat) (acc : List Nat),
    y ∈ l.foldl (fun acc c => (F.nbrs c).foldl (fun acc x =>
      if C.contains x || D.contains x || acc.contains x then acc else acc ++ [x]) acc) acc ↔
      y ∈ acc ∨ ∃ c ∈ l, y ∈ F.nbrs c ∧ y ∉ C ∧ y ∉ D := by
  intro l
  induction l with
  | nil => intro acc; simp
  | cons c cs ih =>
    intro acc
    rw [List.foldl_cons, ih, mem_inner]
    simp only [List.mem_cons, exists_eq_or_imp]
    constructor
    · rintro ((h | ⟨h1, h2, h3⟩) | h)
      · exact Or.inl h
      · exact Or.inr (Or.inl ⟨h1, h2, h3⟩)
      · exact Or.inr (Or.inr h)
    · rintro (h | ⟨h1, h2, h3⟩ | h)
      · exact Or.inl (Or.inl h)
      · exact Or.inl (Or.inr ⟨h1, h2, h3⟩)
      · exact Or.inr h

theorem mem_undoAttach (F : Graph) (D C : List Nat) (x : Nat) :
    x ∈ undoAttach F D C ↔ ∃ c ∈ C, x ∈ F.nbrs c ∧ x ∉ C ∧ x ∉ D := by
  unfold undoAttach
  rw [mem_outer]
  simp

theorem nodup_inner (C D : List Nat) (l : List Nat) : ∀ acc : List Nat, acc.Nodup →
    (l.foldl (fun acc x => if C.contains x || D.contains x || acc.contains x then acc
      else acc ++ [x]) acc).Nodup := by
  induction l with
  | nil => intro acc h; simpa using h
  | cons z zs ih =>
    intro acc h
    rw [List.foldl_cons]
    by_cases hc : (C.contains z || D.contains z || acc.contains z) = true
    · rw [if_pos hc]
      exact ih acc h
    · rw [if_neg hc]
      apply ih
      apply List.Nodup.append h (List.nodup_singleton z)
      rw [List.disjoint_singleton]
      intro hz
      apply hc
      simp only [List.elem_eq_mem, decide_eq_true_eq, Bool.or_eq_true]
      exact Or.inr (by simpa using hz)

theorem nodup_undoAttach (F : Graph) (D C : List Nat) : (undoAttach F D C).Nodup := by
  unfold undoAttach
  have key : ∀ (l : List Nat) (acc : List Nat), acc.Nodup →
      (l.foldl (fun acc c => (F.nbrs c).foldl (fun acc x =>
        if C.contains x || D.contains x || acc.contains x then acc else acc ++ [x]) acc) acc).Nodup := by
    intro l
    induction l with
    | nil => intro acc h; simpa using h
    | cons c cs ih =>
      intro acc h
      rw [List.foldl_cons]
      apply ih
      exact nodup_inner C D (F.nbrs c) acc h
  exact key C [] List.nodup_nil


/-! ## The rest graph -/

/-- The predicate `v ∉ D ∧ v ∉ V(R)` defining the rest graph of `AttachInvariant`. -/
def restKeep (ops : List Op) (R : Graph) (v : Nat) : Bool :=
  !(deletedSet ops).contains v && !R.mem v

theorem restKeep_iff (ops : List Op) (R : Graph) (hR : R.WF) (y : Nat) :
    restKeep ops R y = true ↔ (y ∉ deletedSet ops ∧ y ∉ R.nodes) := by
  have hm : R.mem y = false ↔ y ∉ R.nodes := by
    rw [← hR.mem_iff y]
    cases R.mem y <;> simp
  unfold restKeep
  cases h2 : (deletedSet ops).contains y <;> cases h3 : R.mem y <;> simp_all

/-- Core of `AttachInvariant`, in the torso world of `TorsoSim`. -/
theorem attach_core (n : ℕ) (F R : Graph) (ops : List Op) (F1 B1 : Finset (Fin n))
    (hF : F.WF) (hR : R.WF) (hn : ∀ v ∈ F.nodes, v < n) (hOps : OpsRecord F ops R)
    (hgood : CubicPathwidth.T4.Good (F.toSimpleGraph n) F1 B1)
    (hF1 : ∀ x : Fin n, x ∈ F1 ↔ x.val ∈ F.nodes ∧ x.val ∉ deletedSet ops)
    (hB1 : ∀ x : Fin n, x ∈ B1 ↔ x.val ∈ R.nodes)
    (hadj : ∀ x y : Fin n,
      (CubicPathwidth.T4.tgraph (F.toSimpleGraph n) F1 B1).Adj x y ↔ R.Adj x.val y.val)
    (hConn : ComponentsConnected) (hMono : RecordMono) :
    ∀ C ∈ (F.induced (restKeep ops R)).components,
      (∀ x ∈ undoAttach F (deletedSet ops) C, x ∈ R.nodes) ∧
      (undoAttach F (deletedSet ops) C).length ≤ 2 ∧
      (∀ a b, undoAttach F (deletedSet ops) C = [a, b] → R.Adj a b) ∧
      Emptiable (F.induced C.contains) := by
  intro C hC
  have hHW : (F.induced (restKeep ops R)).WF := (inducedSpec F (restKeep ops R) hF).1
  have hHn := (inducedSpec F (restKeep ops R) hF).2.1
  have hHadj := (inducedSpec F (restKeep ops R) hF).2.2
  have hcomp := componentsSpec (F.induced (restKeep ops R)) hHW
  have hCnodes : ∀ y ∈ C, y ∈ F.nodes ∧ restKeep ops R y = true := by
    intro y hy
    have hmem : y ∈ (F.induced (restKeep ops R)).nodes :=
      hcomp.1.mem_iff.1 (List.mem_flatten.2 ⟨C, hC, hy⟩)
    exact (hHn y).1 hmem
  have hclos : ∀ y ∈ C, ∀ z, (F.induced (restKeep ops R)).Adj y z → z ∈ C :=
    fun y hy z h => hcomp.2.2 C hC y hy z h
  have hreach : ∀ y ∈ C, ∀ z ∈ C,
      Relation.ReflTransGen (F.induced (restKeep ops R)).Adj y z :=
    fun y hy z hz => hConn _ hHW C hC y hy z hz
  have hCne : C ≠ [] := hcomp.2.1 C hC
  -- the torso-side component
  obtain ⟨T, hTdef⟩ : ∃ T : Finset (Fin n), T = Finset.univ.filter (fun x => x.val ∈ C) :=
    ⟨_, rfl⟩
  have hTmem : ∀ x : Fin n, x ∈ T ↔ x.val ∈ C := by
    intro x; rw [hTdef]; simp
  have hSadj : ∀ x y : Fin n, (F.toSimpleGraph n).Adj x y ↔
      x ≠ y ∧ (F.Adj x.val y.val ∨ F.Adj y.val x.val) := by
    intro x y
    simp only [Graph.toSimpleGraph, SimpleGraph.fromRel_adj]
  have hSsymm : ∀ x y : Fin n, (F.toSimpleGraph n).Adj x y → F.Adj x.val y.val :=
    fun x y h => ((hSadj x y).1 h).2.elim id (fun h' => hF.symm _ _ h')
  have hUmem : ∀ x : Fin n, x ∈ F1 \ B1 ↔ (x.val ∈ F.nodes ∧ restKeep ops R x.val = true) := by
    intro x
    rw [Finset.mem_sdiff, hF1 x, hB1 x, restKeep_iff ops R hR]
    constructor
    · rintro ⟨⟨h1, h2⟩, h3⟩
      exact ⟨h1, h2, h3⟩
    · rintro ⟨h1, h2, h3⟩
      exact ⟨⟨h1, h2⟩, h3⟩
  have hTsub : T ⊆ F1 \ B1 := by
    intro x hx
    rw [hTmem] at hx
    exact (hUmem x).2 ⟨(hCnodes _ hx).1, (hCnodes _ hx).2⟩
  have hTcl : CubicPathwidth.ClosedIn (F.toSimpleGraph n) (F1 \ B1) T := by
    intro x hx w hw hwx
    have hxC := (hTmem x).1 hx
    have hFxw := hSsymm x w hwx
    have hwk := (hUmem w).1 hw
    have hHxw : (F.induced (restKeep ops R)).Adj x.val w.val :=
      (hHadj x.val w.val).2 ⟨hFxw, (hCnodes x.val hxC).2, hwk.2⟩
    exact (hTmem w).2 (hclos x.val hxC w.val hHxw)
  have hTconn : CubicPathwidth.SectionConnected (F.toSimpleGraph n) T := by
    refine ⟨?_, ?_⟩
    · obtain ⟨y0, hy0⟩ := List.exists_mem_of_ne_nil C hCne
      exact ⟨⟨y0, hn y0 (hCnodes y0 hy0).1⟩, (hTmem _).2 hy0⟩
    · intro S' hS'T hcl hS'ne
      obtain ⟨x0, hx0⟩ := hS'ne
      ext x
      constructor
      · intro hx
        exact hS'T hx
      · intro hxT
        have hx0C : x0.val ∈ C := (hTmem x0).1 (hS'T hx0)
        have hxC : x.val ∈ C := (hTmem x).1 hxT
        have key : ∀ z, Relation.ReflTransGen (F.induced (restKeep ops R)).Adj x0.val z →
            ∃ w ∈ S', w.val = z := by
          intro z hz
          induction hz with
          | refl => exact ⟨x0, hx0, rfl⟩
          | @tail b c _ hbc ih =>
            obtain ⟨w, hwS, hwb⟩ := ih
            have hwC : b ∈ C := by
              rw [← hwb]
              exact (hTmem w).1 (hS'T hwS)
            have hcC : c ∈ C := hclos b hwC c hbc
            have hcn : c < n := hn c (hCnodes c hcC).1
            have hFbc : F.Adj b c := ((hHadj b c).1 hbc).1
            have hbne : b ≠ c := by
              intro h
              subst h
              exact hHW.loopless _ hbc
            have hc'T : (⟨c, hcn⟩ : Fin n) ∈ T := (hTmem _).2 hcC
            have hwc' : w ≠ ⟨c, hcn⟩ := by
              intro h
              apply hbne
              have hv : w.val = c := congrArg Fin.val h
              rw [← hwb]
              exact hv
            have hSwc : (F.toSimpleGraph n).Adj w ⟨c, hcn⟩ :=
              (hSadj w ⟨c, hcn⟩).2 ⟨hwc', Or.inl (by rw [hwb]; exact hFbc)⟩
            exact ⟨⟨c, hcn⟩, hcl w hwS ⟨c, hcn⟩ hc'T hSwc, rfl⟩
        obtain ⟨w, hwS, hwx⟩ := key x.val (hreach x0.val hx0C x.val hxC)
        have hwx' : w = x := Fin.ext hwx
        rw [← hwx']
        exact hwS
  have hTcomp : T ∈ CubicPathwidth.components (F.toSimpleGraph n) (F1 \ B1) :=
    CubicPathwidth.T4.mem_components_of_conn (F.toSimpleGraph n) hTsub hTcl hTconn
  have hatt : (CubicPathwidth.attachment (F.toSimpleGraph n) B1 T).card ≤ 2 :=
    CubicPathwidth.T4.Good.attachment_card_le (F.toSimpleGraph n) hgood T hTcomp
  -- list facts about `undoAttach`
  have hLF : ∀ x ∈ undoAttach F (deletedSet ops) C, x ∈ F.nodes := by
    intro x hx
    obtain ⟨c, _, hxc, _, _⟩ := (mem_undoAttach F _ C x).1 hx
    exact (mem_of_adj hF hxc).2
  have hLR : ∀ x ∈ undoAttach F (deletedSet ops) C, x ∈ R.nodes := by
    intro x hx
    obtain ⟨c, hc, hxc, hxC, hxD⟩ := (mem_undoAttach F _ C x).1 hx
    by_contra hxR
    have hk : restKeep ops R x = true := (restKeep_iff ops R hR x).2 ⟨hxD, hxR⟩
    have hHcx : (F.induced (restKeep ops R)).Adj c x :=
      (hHadj c x).2 ⟨hxc, (hCnodes c hc).2, hk⟩
    exact hxC (hclos c hc x hHcx)
  have hLsub : ∀ x (hx : x ∈ undoAttach F (deletedSet ops) C),
      (⟨x, hn x (hLF x hx)⟩ : Fin n) ∈ CubicPathwidth.attachment (F.toSimpleGraph n) B1 T := by
    intro x hx
    obtain ⟨c, hc, hxc, hxC, _⟩ := (mem_undoAttach F _ C x).1 hx
    rw [CubicPathwidth.mem_attachment]
    refine ⟨(hB1 _).2 (hLR x hx), ⟨c, hn c (hCnodes c hc).1⟩, (hTmem _).2 hc, ?_⟩
    rw [hSadj]
    refine ⟨fun h => hxC ?_, Or.inr hxc⟩
    have hxc' : x = c := congrArg Fin.val h
    rw [hxc']
    exact hc
  refine ⟨fun x hx => hLR x hx, ?_, ?_, ?_⟩
  · have hsub : (undoAttach F (deletedSet ops) C).toFinset ⊆
        ((CubicPathwidth.attachment (F.toSimpleGraph n) B1 T).image Fin.val) := by
      intro x hx
      rw [List.mem_toFinset] at hx
      rw [Finset.mem_image]
      exact ⟨⟨x, hn x (hLF x hx)⟩, hLsub x hx, rfl⟩
    rw [← List.toFinset_card_of_nodup (nodup_undoAttach F (deletedSet ops) C)]
    exact (Finset.card_le_card hsub).trans ((Finset.card_image_le).trans hatt)
  · intro a b hab
    have hnd := nodup_undoAttach F (deletedSet ops) C
    rw [hab] at hnd
    have hne : a ≠ b := by
      simp at hnd
      exact hnd
    have ha : a ∈ undoAttach F (deletedSet ops) C := by rw [hab]; simp
    have hb : b ∈ undoAttach F (deletedSet ops) C := by rw [hab]; simp
    have hne' : (⟨a, hn a (hLF a ha)⟩ : Fin n) ≠ ⟨b, hn b (hLF b hb)⟩ :=
      fun h => hne (congrArg Fin.val h)
    have hadjT := (CubicPathwidth.T4.tgraph_adj_iff (F.toSimpleGraph n) F1 B1 _ _).2
      ⟨hne', (hB1 _).2 (hLR a ha), (hB1 _).2 (hLR b hb),
        Or.inr ⟨T, hTcomp, hLsub a ha, hLsub b hb⟩⟩
    exact (hadj _ _).1 hadjT
  · have hG'W : (F.induced C.contains).WF := (inducedSpec F C.contains hF).1
    have hG'n := (inducedSpec F C.contains hF).2.1
    have hG'a := (inducedSpec F C.contains hF).2.2
    have hsubG : (∀ x ∈ (F.induced C.contains).nodes, x ∈ F.nodes) ∧
        ∀ u w, (F.induced C.contains).Adj u w → F.Adj u w :=
      ⟨fun x hx => ((hG'n x).1 hx).1, fun u w h => ((hG'a u w).1 h).1⟩
    have hdel : ∀ w, Op.del w ∈ ops → w ∉ (F.induced C.contains).nodes := by
      intro w hw hwG
      have hwC : w ∈ C := by
        have := ((hG'n w).1 hwG).2
        simpa using this
      have hwD : w ∈ deletedSet ops := List.mem_filterMap.2 ⟨Op.del w, hw, rfl⟩
      exact ((restKeep_iff ops R hR w).1 (hCnodes w hwC).2).1 hwD
    obtain ⟨ops', R', hred, hrec', h1, _, h3⟩ :=
      hMono F (F.induced C.contains) R ops hF hG'W hsubG.1 hsubG.2 hdel hOps
    have hempty : ∀ x ∈ R'.nodes, False := by
      intro x hx
      have hxG := h3 x hx
      have hxC : x ∈ C := by
        have := ((hG'n x).1 hxG).2
        simpa using this
      exact ((restKeep_iff ops R hR x).1 (hCnodes x hxC).2).2 (h1 x hx)
    have hsame : SameGraph R' Graph.empty := by
      constructor
      · intro x
        constructor
        · intro hx
          exact absurd hx (hempty x)
        · intro hx
          simp [Graph.empty] at hx
      · intro u v
        constructor
        · intro h
          exact absurd (opsRecord_adj_mem ops' _ R' hG'W hrec' u v h) (hempty u)
        · intro h
          simp [Graph.Adj, Graph.nbrs, Graph.empty] at h
    exact ⟨ops', hred, opsRecord_end_congr ops' _ R' Graph.empty hrec' hsame⟩

end R8

/-- `AttachInvariant` (`(I2)` of Lemma 4.5 (`lem:reduction`)), from the torso simulation, the record
monotonicity and the connectedness of components. -/
theorem attachInvariant_of (hSim : TorsoSim) (hMono : RecordMono) (hConn : ComponentsConnected)
    (hCongr : OpsRecordCongr) (hApp : OpsRecordAppend) : AttachInvariant := by
  intro F R ops hF hR hOps C hC
  have hn : ∀ v ∈ F.nodes, v < F.nodes.sum + 1 :=
    fun v hv => Nat.lt_succ_of_le (R8.le_sum_mem _ v hv)
  obtain ⟨hG0, hreach, hadj⟩ := hSim (F.nodes.sum + 1) F R ops hF hn hOps
  have hgood := CubicPathwidth.T4.Good.reach hG0 hreach
  exact R8.attach_core (F.nodes.sum + 1) F R ops _ _ hF hR hn hOps hgood
    (fun x => by simp) (fun x => by simp) hadj hConn hMono C hC

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.attachInvariant_of
#print axioms CubicPathwidth.Alg.R8.attach_core
#print axioms CubicPathwidth.Alg.R8.replay