CubicPathwidth.T4.Lift

Source file CubicPathwidth/T4/Lift.lean of the Lean project (how it is built).

import CubicPathwidth.T4.ProcessDefs
import CubicPathwidth.T2.Reduction
import CubicPathwidth.T2.ReductionPieces

/-!
# Lemma 4.5 (`lem:reduction`) in state form ("reductions are paid once") and the second case
of Lemma 9.11 (`lem:basic`)

In the paper: Lemma 4.5 (`lem:reduction`), and Lemma 9.11 (`lem:basic`).

Fix a good state `(F, B)` with torso `H = tgraph G F B`. Along any sequence of steps
from `(F, B)` to `(F_t, B_t)` we keep (`reach_invariant`):

* the deleted set `D = F \ F_t` lies in `B`, and `B_t ⊆ B \ D`;
* writing `K = restrictG H (B \ D)` (the torso `H` with the deleted vertices
  removed), `T2.GoodCore K B_t` holds: every component of the removed part
  `K[univ \ B_t]` has at most two attachment vertices in `B_t` and carries a
  `T2.Piece` structure (a width-two tree decomposition hanging from its
  attachment). These are the invariants (I1), (I2) of the manuscript.

The torso of `K` over `B_t` is a subgraph of the current torso
`tgraph G F_t B_t` (`tgraph_restrict_le`), so a vertex of torso degree at most two
in the current state has degree at most two in it, and `T2.goodCore_erase` applies.
A deletion removes one vertex from `K` (`goodCore_delete`, using `Piece.erase_vertex`).

Lifting (`lift_core`): a decomposition of the final torso is a decomposition of
the torso of `K` over the final core; `liftTorso`, `torso_attachment_bag` and
`insert_components` insert the pieces (width `12 √n` each, paid once); finally the
deleted set `D` is added to every bag and the result is relabelled onto `B`
(`hasPathwidth_of_bagPath`).
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2 SectionDecomposition

variable {n : ℕ}

/-! ## Restricting a graph to a vertex set -/

/-- `H` with only the edges having both ends in `U`. -/
def restrictG (H : SimpleGraph (Fin n)) (U : Finset (Fin n)) : SimpleGraph (Fin n) where
  Adj u v := H.Adj u v ∧ u ∈ U ∧ v ∈ U
  symm := ⟨fun _ _ h => ⟨h.1.symm, h.2.2, h.2.1⟩⟩
  loopless := ⟨fun _ h => H.irrefl h.1⟩

/-! ## Isolated vertices -/

theorem component_isolated {K : SimpleGraph (Fin n)} {W T : Finset (Fin n)}
    (hT : T ∈ components K W) {x : Fin n} (hx : x ∈ T) (hiso : ∀ u, ¬ K.Adj x u) :
    T = {x} := by
  obtain ⟨_, _, hconn⟩ := mem_components K hT
  refine (hconn.2 {x} (by simpa using hx) ?_ ⟨x, by simp⟩).symm
  intro a ha z _ hadj
  rw [Finset.mem_singleton] at ha
  subst ha
  exact absurd hadj (hiso z)

theorem attachment_isolated (K : SimpleGraph (Fin n)) (B : Finset (Fin n)) {x : Fin n}
    (hiso : ∀ u, ¬ K.Adj x u) : attachment K B {x} = ∅ := by
  apply Finset.eq_empty_of_forall_notMem
  intro a ha
  obtain ⟨_, u, hu, hau⟩ := (mem_attachment K).mp ha
  rw [Finset.mem_singleton] at hu
  subst hu
  exact hiso a hau.symm

theorem piece_isolated (K : SimpleGraph (Fin n)) {x : Fin n} (hiso : ∀ u, ¬ K.Adj x u) :
    Piece K {x} ∅ := by
  have h := Piece.node (G := K) (v := x) (T := ∅) (A := ∅) (by simp)
    (fun u hu => absurd hu (hiso u)) (Piece.empty _)
  simpa using h

/-- A core outside which every vertex is isolated is good. -/
theorem goodCore_of_isolated {K : SimpleGraph (Fin n)} {B : Finset (Fin n)}
    (h : ∀ x, x ∉ B → ∀ u, ¬ K.Adj x u) : GoodCore K B := by
  intro T hT
  obtain ⟨x, hx⟩ := (mem_components K hT).2.2.1
  have hxB : x ∉ B := (Finset.mem_sdiff.mp ((mem_components K hT).1 hx)).2
  rw [component_isolated hT hx (h x hxB), attachment_isolated K B (h x hxB)]
  exact ⟨by simp, piece_isolated K (h x hxB)⟩

/-! ## Deleting a vertex keeps pieces -/

/-- Removing an isolated (in the new graph) vertex `w ∉ T` from the attachment of a
piece. -/
theorem Piece.erase_vertex {K K' : SimpleGraph (Fin n)} {w : Fin n}
    (hle : ∀ x y, K'.Adj x y → K.Adj x y) (hw : ∀ u, ¬ K'.Adj w u)
    {T A : Finset (Fin n)} (h : Piece K T A) : w ∉ T → Piece K' T (A.erase w) := by
  induction h with
  | empty A => intro _; exact Piece.empty _
  | union _ _ ih₁ ih₂ =>
    intro hwT
    rw [Finset.mem_union, not_or] at hwT
    exact Piece.union (ih₁ hwT.1) (ih₂ hwT.2)
  | @node v T A hcard hv _ ih =>
    intro hwT
    have hwv : w ≠ v := fun h => hwT (h ▸ Finset.mem_insert_self _ _)
    have hwT' : w ∉ T := fun h => hwT (Finset.mem_insert_of_mem h)
    have hc := ih hwT'
    rw [Finset.erase_insert_of_ne (Ne.symm hwv)] at hc
    refine Piece.node ?_ ?_ hc
    · exact (Finset.card_le_card
        (Finset.insert_subset_insert v (Finset.erase_subset w A))).trans hcard
    · intro u hu
      rcases hv u (hle _ _ hu) with h | h
      · exact Or.inl h
      · right
        refine Finset.mem_erase.mpr ⟨?_, h⟩
        rintro rfl
        exact hw v hu.symm
  | mono _ hAA' ih =>
    intro hwT
    exact Piece.mono (ih hwT) (Finset.erase_subset_erase w hAA')

/-- Deleting a core vertex `w` (all its edges removed) keeps a good core good. -/
theorem goodCore_delete {K K' : SimpleGraph (Fin n)} {B : Finset (Fin n)} {w : Fin n}
    (hK : ∀ x y, K'.Adj x y ↔ K.Adj x y ∧ x ≠ w ∧ y ≠ w) (hB : GoodCore K B)
    (hwB : w ∈ B) : GoodCore K' (B.erase w) := by
  have hiso : ∀ u, ¬ K'.Adj w u := fun u h => ((hK w u).mp h).2.1 rfl
  intro T hT
  obtain ⟨hTU, hTcl, hTconn⟩ := mem_components K' hT
  by_cases hwT : w ∈ T
  · rw [component_isolated hT hwT hiso, attachment_isolated K' _ hiso]
    exact ⟨by simp, piece_isolated K' hiso⟩
  · have hmem : ∀ t ∈ T, t ≠ w ∧ t ∉ B := by
      intro t ht
      have hne : t ≠ w := fun h => hwT (h ▸ ht)
      refine ⟨hne, fun htB => ?_⟩
      exact (Finset.mem_sdiff.mp (hTU ht)).2 (Finset.mem_erase.mpr ⟨hne, htB⟩)
    have hTsub : T ⊆ Finset.univ \ B := fun t ht =>
      Finset.mem_sdiff.mpr ⟨Finset.mem_univ _, (hmem t ht).2⟩
    have hcl : ClosedIn K (Finset.univ \ B) T := by
      intro t ht z hz hadj
      have hzw : z ≠ w := fun h => (Finset.mem_sdiff.mp hz).2 (h ▸ hwB)
      apply hTcl t ht z
      · exact Finset.mem_sdiff.mpr ⟨Finset.mem_univ _,
          fun h => (Finset.mem_sdiff.mp hz).2 (Finset.mem_of_mem_erase h)⟩
      · exact (hK t z).mpr ⟨hadj, (hmem t ht).1, hzw⟩
    have hconn : SectionConnected K T := by
      refine ⟨hTconn.1, fun S hS hSc hSne => hTconn.2 S hS ?_ hSne⟩
      intro a ha z hz hadj
      exact hSc a ha z hz ((hK a z).mp hadj).1
    have hTmem : T ∈ components K (Finset.univ \ B) := by
      obtain ⟨t, ht⟩ := hTconn.1
      rw [← component_eq_of_connected K hTsub hcl hconn ht]
      exact mem_components_of_mem K (hTsub ht)
    have hatt : attachment K' (B.erase w) T = (attachment K B T).erase w := by
      ext a
      rw [Finset.mem_erase, mem_attachment, mem_attachment, Finset.mem_erase]
      constructor
      · rintro ⟨⟨haw, haB⟩, u, hu, hau⟩
        exact ⟨haw, haB, u, hu, ((hK a u).mp hau).1⟩
      · rintro ⟨haw, haB, u, hu, hau⟩
        exact ⟨⟨haw, haB⟩, u, hu, (hK a u).mpr ⟨hau, haw, (hmem u hu).1⟩⟩
    rw [hatt]
    obtain ⟨hc, hp⟩ := hB T hTmem
    exact ⟨(Finset.card_erase_le).trans hc,
      Piece.erase_vertex (fun x y h => ((hK x y).mp h).1) hiso hp hwT⟩

/-! ## The torso of the restricted torso is a subgraph of the current torso -/

/-- A component of `G[F \ B]` meeting a component of `G[W]`, `F \ B ⊆ W`, lies in it. -/
theorem comp_subset_comp {G : SimpleGraph (Fin n)} {X W S S' : Finset (Fin n)}
    (hXW : X ⊆ W) (hS : S ∈ components G X) (hS' : S' ∈ components G W)
    {s : Fin n} (hsS : s ∈ S) (hsS' : s ∈ S') : S ⊆ S' := by
  obtain ⟨hSX, _, hSconn⟩ := mem_components G hS
  rcases connected_subset_or_disjoint G (hSX.trans hXW) hSconn (mem_components G hS').2.1
    with h | h
  · exact h
  · exact False.elim (Finset.disjoint_left.mp h hsS hsS')

theorem tgraph_restrict_le {G : SimpleGraph (Fin n)} {F B D Bt : Finset (Fin n)}
    (hBF : B ⊆ F) (hDB : D ⊆ B) (hBt : Bt ⊆ B \ D) {x y : Fin n}
    (h : (tgraph (restrictG (tgraph G F B) (B \ D)) Finset.univ Bt).Adj x y) :
    (tgraph G (F \ D) Bt).Adj x y := by
  have hFB : F \ B ⊆ (F \ D) \ Bt := by
    intro u hu
    obtain ⟨huF, huB⟩ := Finset.mem_sdiff.mp hu
    refine Finset.mem_sdiff.mpr ⟨Finset.mem_sdiff.mpr ⟨huF, fun huD => huB (hDB huD)⟩, ?_⟩
    intro huBt
    exact huB (Finset.mem_sdiff.mp (hBt huBt)).1
  -- an `H`-edge from a component `S'` of `G[W]` ends next to `S'`
  have hprop : ∀ S' ∈ components G ((F \ D) \ Bt), ∀ u ∈ S', ∀ z,
      (tgraph G F B).Adj u z → ∃ s ∈ S', G.Adj z s := by
    intro S' hS' u hu z hadj
    obtain ⟨hS'W, hS'cl, _⟩ := mem_components G hS'
    obtain ⟨_, _, _, hG | ⟨S, hS, huS, hzS⟩⟩ := hadj
    · exact ⟨u, hu, hG.symm⟩
    · obtain ⟨_, s1, hs1, hus1⟩ := (mem_attachment G).mp huS
      have hs1W : s1 ∈ (F \ D) \ Bt := hFB ((mem_components G hS).1 hs1)
      have hs1S' : s1 ∈ S' := hS'cl u hu s1 hs1W hus1
      have hsub := comp_subset_comp hFB hS hS' hs1 hs1S'
      obtain ⟨_, s2, hs2, hzs2⟩ := (mem_attachment G).mp hzS
      exact ⟨s2, hsub hs2, hzs2⟩
  obtain ⟨hne, hx, hy, hxy⟩ := h
  refine ⟨hne, hx, hy, ?_⟩
  rcases hxy with ⟨hH, _, _⟩ | ⟨T, hT, hxT, hyT⟩
  · obtain ⟨_, _, _, hG | ⟨S, hS, hxS, hyS⟩⟩ := hH
    · exact Or.inl hG
    · right
      obtain ⟨s, hs⟩ := (mem_components G hS).2.2.1
      have hsW := hFB ((mem_components G hS).1 hs)
      have hS'mem := mem_components_of_mem G hsW
      have hsub := comp_subset_comp hFB hS hS'mem hs (mem_component_self G hsW)
      refine ⟨_, hS'mem, ?_, ?_⟩
      · obtain ⟨_, u, hu, hxu⟩ := (mem_attachment G).mp hxS
        exact (mem_attachment G).mpr ⟨hx, u, hsub hu, hxu⟩
      · obtain ⟨_, u, hu, hyu⟩ := (mem_attachment G).mp hyS
        exact (mem_attachment G).mpr ⟨hy, u, hsub hu, hyu⟩
  · right
    obtain ⟨hTU, _, hTconn⟩ := mem_components _ hT
    obtain ⟨_, a, haT, hxa⟩ := (mem_attachment _).mp hxT
    obtain ⟨_, b, hbT, hyb⟩ := (mem_attachment _).mp hyT
    have hmemW : ∀ z, z ∈ B \ D → z ∉ Bt → z ∈ (F \ D) \ Bt := by
      intro z hz hzBt
      obtain ⟨hzB, hzD⟩ := Finset.mem_sdiff.mp hz
      exact Finset.mem_sdiff.mpr ⟨Finset.mem_sdiff.mpr ⟨hBF hzB, hzD⟩, hzBt⟩
    have haW : a ∈ (F \ D) \ Bt :=
      hmemW a hxa.2.2 (Finset.mem_sdiff.mp (hTU haT)).2
    set S' := component G ((F \ D) \ Bt) a with hS'def
    have hS'mem : S' ∈ components G ((F \ D) \ Bt) := mem_components_of_mem G haW
    have hcl : ClosedIn (restrictG (tgraph G F B) (B \ D)) (Finset.univ \ Bt) S' := by
      intro u hu z hz hadj
      have hzW := hmemW z hadj.2.2 (Finset.mem_sdiff.mp hz).2
      obtain ⟨s, hs, hzs⟩ := hprop S' hS'mem u hu z hadj.1
      exact (mem_components G hS'mem).2.1 s hs z hzW hzs.symm
    have hTS' : T ⊆ S' := by
      rcases connected_subset_or_disjoint _ hTU hTconn hcl with h | h
      · exact h
      · exact False.elim (Finset.disjoint_left.mp h haT (mem_component_self G haW))
    refine ⟨S', hS'mem, ?_, ?_⟩
    · obtain ⟨s, hs, hxs⟩ := hprop S' hS'mem a (hTS' haT) x hxa.1.symm
      exact (mem_attachment G).mpr ⟨hx, s, hs, hxs⟩
    · obtain ⟨s, hs, hys⟩ := hprop S' hS'mem b (hTS' hbT) y hyb.1.symm
      exact (mem_attachment G).mpr ⟨hy, s, hs, hys⟩

/-! ## The invariant along a sequence of steps -/

open Classical in

theorem coreTorso_degree_le {K G : SimpleGraph (Fin n)} {Ft Bt : Finset (Fin n)}
    (hle : ∀ x y, (tgraph K Finset.univ Bt).Adj x y → (tgraph G Ft Bt).Adj x y)
    (i : Fin Bt.card) :
    (coreTorso K Finset.univ Bt).degree i ≤ tdeg G Ft Bt (enumerate Bt i) := by
  unfold tdeg
  rw [← SimpleGraph.card_neighborFinset_eq_degree, ← SimpleGraph.card_neighborFinset_eq_degree]
  calc ((coreTorso K Finset.univ Bt).neighborFinset i).card
      = (((coreTorso K Finset.univ Bt).neighborFinset i).image (enumerate Bt)).card :=
        (Finset.card_image_of_injective _ (enumerate Bt).injective).symm
    _ ≤ _ := by
        apply Finset.card_le_card
        intro z hz
        obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hz
        rw [SimpleGraph.mem_neighborFinset] at hj ⊢
        exact hle _ _ ((coreTorso_adj_iff K Finset.univ Bt i j).mp hj)

/-- The invariants (I1), (I2) along any sequence of steps from a state with `B ⊆ F`. -/
theorem reach_invariant {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (hBF : B ⊆ F)
    {t : Finset (Fin n) × Finset (Fin n)} (h : Reach G (F, B) t) :
    ∃ D ⊆ B, t.1 = F \ D ∧ t.2 ⊆ B \ D ∧
      GoodCore (restrictG (tgraph G F B) (B \ D)) t.2 := by
  induction h with
  | refl =>
    refine ⟨∅, Finset.empty_subset _, by simp, by simp, ?_⟩
    simp only [Finset.sdiff_empty]
    apply goodCore_of_isolated
    intro x hx u hadj
    exact hx hadj.2.1
  | tail _ hs ih =>
    obtain ⟨D, hDB, h1, h2, hgood⟩ := ih
    cases hs with
    | @reduce Fb Bb v hv hdeg =>
      simp only at h1 h2 hgood ⊢
      refine ⟨D, hDB, h1, (Finset.erase_subset _ _).trans h2, ?_⟩
      obtain ⟨i, hi⟩ := (mem_iff_enumerate Bb v).mp hv
      have hle : ∀ x y, (tgraph (restrictG (tgraph G F B) (B \ D)) Finset.univ Bb).Adj x y →
          (tgraph G Fb Bb).Adj x y := by
        intro x y hxy
        rw [h1]
        exact tgraph_restrict_le hBF hDB h2 hxy
      have hd := coreTorso_degree_le hle i
      rw [hi] at hd
      have := goodCore_erase (restrictG (tgraph G F B) (B \ D)) hgood (i := i) (by omega)
      rwa [hi] at this
    | @delete Fb Bb w hw =>
      simp only at h1 h2 hgood ⊢
      have hwBD := h2 hw
      obtain ⟨hwB, hwD⟩ := Finset.mem_sdiff.mp hwBD
      refine ⟨insert w D, Finset.insert_subset hwB hDB, ?_, ?_, ?_⟩
      · rw [h1]
        ext x
        simp only [Finset.mem_erase, Finset.mem_sdiff, Finset.mem_insert]
        tauto
      · intro x hx
        obtain ⟨hxw, hxB⟩ := Finset.mem_erase.mp hx
        have := h2 hxB
        simp only [Finset.mem_sdiff, Finset.mem_insert] at this ⊢
        tauto
      · apply goodCore_delete (K := restrictG (tgraph G F B) (B \ D)) _ hgood hw
        intro x y
        simp only [restrictG, Finset.mem_sdiff, Finset.mem_insert]
        tauto

/-! ## Relabelling a bag sequence onto a subset -/

theorem hasPathwidth_of_bagPath {m : ℕ} (Q : SimpleGraph (Fin m)) (e : Fin m ↪ Fin n)
    (P : BagPath (Fin n)) {w : ℝ} (hP : P.WidthAtMost w)
    (hv : ∀ i, ∃ k, k ≤ P.lastIndex ∧ e i ∈ P.bag k)
    (he : ∀ i j, Q.Adj i j → ∃ k, k ≤ P.lastIndex ∧ e i ∈ P.bag k ∧ e j ∈ P.bag k) :
    HasPathwidthAtMost Q w := by
  classical
  let P' : BagPath (Fin m) := {
    lastIndex := P.lastIndex
    bag := fun k => Finset.univ.filter (fun i => e i ∈ P.bag k)
    interval := by
      intro i j k hij hjk hk v hv
      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hv ⊢
      exact P.interval i j k hij hjk hk (e v) hv }
  have hv' : ∀ v, ∃ i, i ≤ P'.lastIndex ∧ v ∈ P'.bag i := by
    intro v
    obtain ⟨k, hk, hmem⟩ := hv v
    exact ⟨k, hk, by simpa [P'] using hmem⟩
  have he' : ∀ u v, Q.Adj u v → ∃ i, i ≤ P'.lastIndex ∧ u ∈ P'.bag i ∧ v ∈ P'.bag i := by
    intro u v huv
    obtain ⟨k, hk, hu, hv⟩ := he u v huv
    exact ⟨k, hk, by simpa [P'] using hu, by simpa [P'] using hv⟩
  refine ⟨P'.toDecomposition Q hv' he', BagPath.toDecomposition_width _ _ _ _ ?_⟩
  intro k hk
  refine le_trans ?_ (hP k hk)
  have : (Finset.univ.filter (fun i => e i ∈ P.bag k)).card ≤ (P.bag k).card := by
    rw [← Finset.card_image_of_injective _ e.injective]
    apply Finset.card_le_card
    intro z hz
    obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hz
    exact (Finset.mem_filter.mp hi).2
  exact_mod_cast this

theorem mem_hold_bag (P : BagPath (Fin n)) (X : Finset (Fin n)) (k : ℕ) (v : Fin n) :
    v ∈ (P.hold X).bag k ↔ v ∈ P.bag k ∨ v ∈ X := by
  simp [BagPath.hold]

/-- Same bags, fewer edges. -/
def PathDecomposition.ofLE {m : ℕ} {Q Q' : SimpleGraph (Fin m)}
    (hle : ∀ i j, Q.Adj i j → Q'.Adj i j) (D : PathDecomposition Q') : PathDecomposition Q where
  lastIndex := D.lastIndex
  bag := D.bag
  vertex_covered := D.vertex_covered
  edge_covered := fun i j h => D.edge_covered i j (hle i j h)
  interval := D.interval

/-! ## Lifting -/

theorem card_le_n (T : Finset (Fin n)) : (T.card : ℝ) ≤ n := by
  have := Finset.card_le_univ T
  simp only [Fintype.card_fin] at this
  exact_mod_cast this

/-- Lifting a decomposition of the final torso to the torso of `(F, B)`, when the
invariant holds with deleted set `D`. -/
theorem lift_core {G : SimpleGraph (Fin n)} {F B D B' : Finset (Fin n)}
    (hBF : B ⊆ F) (hDB : D ⊆ B) (hB' : B' ⊆ B \ D)
    (hgood : GoodCore (restrictG (tgraph G F B) (B \ D)) B') {p : ℝ}
    (hp : HasPathwidthAtMost (coreTorso G (F \ D) B') p) :
    HasPathwidthAtMost (coreTorso G F B)
      ((D.card : ℝ) + p + 12 * Real.sqrt (n : ℝ) + 1) := by
  classical
  set K := restrictG (tgraph G F B) (B \ D) with hK
  obtain ⟨Dec, hDec⟩ := hp
  have hle : ∀ i j, (coreTorso K Finset.univ B').Adj i j →
      (coreTorso G (F \ D) B').Adj i j := by
    intro i j hij
    rw [coreTorso_adj_iff] at hij ⊢
    exact tgraph_restrict_le hBF hDB hB' hij
  let Dec2 : PathDecomposition (coreTorso K Finset.univ B') := PathDecomposition.ofLE hle Dec
  have hDec2 : Dec2.WidthAtMost p := hDec
  have hP := liftTorso_width K Finset.univ B' Dec2 hDec2
  have hattach : ∀ T ∈ components K (Finset.univ \ B'), (attachment K B' T).card ≤ 2 :=
    fun T hT => (hgood T hT).1
  have hpieces : ∀ T ∈ components K (Finset.univ \ B'),
      ∃ Q : SectionDecomposition K T, Q.toBagPath.WidthAtMost (12 * Real.sqrt (n : ℝ)) := by
    intro T hT
    obtain ⟨Q, hQ⟩ := (hgood T hT).2.section_decomposition (by have := (hgood T hT).1; omega)
    exact ⟨Q, hQ.mono (by linarith [Real.sqrt_le_sqrt (card_le_n T)])⟩
  obtain ⟨R', hR'⟩ := insert_components K (Finset.subset_univ B')
    (liftTorso K Finset.univ B' Dec2) hP (by positivity) hpieces
    (fun T hT => torso_attachment_bag K Finset.univ B' Dec2 hT (hattach T hT))
  have hw := BagPath.hold_width R'.toBagPath D hR'
  apply hasPathwidth_of_bagPath (coreTorso G F B) (enumerate B) (R'.toBagPath.hold D)
    (hw.mono (le_of_eq (by ring)))
  · intro i
    obtain ⟨k, hk, hmem⟩ := R'.vertex_covered (enumerate B i) (Finset.mem_univ _)
    exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inl hmem)⟩
  · intro i j hij
    rw [coreTorso_adj_iff] at hij
    have hxB : enumerate B i ∈ B := (mem_iff_enumerate B _).mpr ⟨i, rfl⟩
    have hyB : enumerate B j ∈ B := (mem_iff_enumerate B _).mpr ⟨j, rfl⟩
    by_cases hx : enumerate B i ∈ D
    · obtain ⟨k, hk, hmem⟩ := R'.vertex_covered (enumerate B j) (Finset.mem_univ _)
      exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inr hx),
        (mem_hold_bag _ _ _ _).mpr (Or.inl hmem)⟩
    by_cases hy : enumerate B j ∈ D
    · obtain ⟨k, hk, hmem⟩ := R'.vertex_covered (enumerate B i) (Finset.mem_univ _)
      exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inl hmem),
        (mem_hold_bag _ _ _ _).mpr (Or.inr hy)⟩
    have hK' : K.Adj (enumerate B i) (enumerate B j) :=
      ⟨hij, Finset.mem_sdiff.mpr ⟨hxB, hx⟩, Finset.mem_sdiff.mpr ⟨hyB, hy⟩⟩
    obtain ⟨k, hk, hu, hv⟩ := R'.edge_covered _ (Finset.mem_univ _) _ (Finset.mem_univ _) hK'
    exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inl hu), (mem_hold_bag _ _ _ _).mpr (Or.inl hv)⟩

/-- (E2b) Lemma 4.5 (`lem:reduction`) in state form. -/
theorem liftClaim : LiftClaim := by
  intro n G F B F' B' p hgood hreach hp
  have hBF := hgood.subset
  obtain ⟨D, hDB, h1, h2, hgc⟩ := reach_invariant hBF hreach
  simp only at h1 h2 hgc
  subst h1
  rw [Finset.sdiff_sdiff_eq_self (hDB.trans hBF)]
  exact lift_core hBF hDB h2 hgc hp

/-! ## The second case of Lemma 9.11 (`lem:basic`) -/

theorem components_subset_of_closed {K : SimpleGraph (Fin n)} {W W' : Finset (Fin n)}
    (hWW' : W ⊆ W') (hcl : ClosedIn K W' W) {T : Finset (Fin n)}
    (hT : T ∈ components K W) : T ∈ components K W' := by
  obtain ⟨hTW, hTcl, hTconn⟩ := mem_components K hT
  obtain ⟨t, ht⟩ := hTconn.1
  have hcl' : ClosedIn K W' T := fun a ha z hz hadj =>
    hTcl a ha z (hcl a (hTW ha) z hz hadj) hadj
  rw [← component_eq_of_connected K (hTW.trans hWW') hcl' hTconn ht]
  exact mem_components_of_mem K (hWW' (hTW ht))

/-- The torso restricted to a set `C ⊆ B` is a subgraph of the torso. -/
theorem tgraph_sub_le {G : SimpleGraph (Fin n)} {F B C : Finset (Fin n)} (hCB : C ⊆ B)
    {x y : Fin n} (h : (tgraph G (F \ (B \ C)) C).Adj x y) : (tgraph G F B).Adj x y := by
  have hset : (F \ (B \ C)) \ C = F \ B := by
    ext u
    simp only [Finset.mem_sdiff]
    constructor
    · rintro ⟨⟨huF, huBC⟩, huC⟩
      exact ⟨huF, fun huB => huBC ⟨huB, huC⟩⟩
    · rintro ⟨huF, huB⟩
      exact ⟨⟨huF, fun h => huB h.1⟩, fun huC => huB (hCB huC)⟩
  obtain ⟨hne, hx, hy, hxy⟩ := h
  refine ⟨hne, hCB hx, hCB hy, ?_⟩
  rcases hxy with hG | ⟨S, hS, hxS, hyS⟩
  · exact Or.inl hG
  · right
    rw [hset] at hS
    refine ⟨S, hS, ?_, ?_⟩
    · obtain ⟨h1, h2⟩ := (mem_attachment G).mp hxS
      exact (mem_attachment G).mpr ⟨hCB h1, h2⟩
    · obtain ⟨h1, h2⟩ := (mem_attachment G).mp hyS
      exact (mem_attachment G).mpr ⟨hCB h1, h2⟩

/-- (E2c) The second case of Lemma 9.11 (`lem:basic`). -/
theorem kindTwo : KindTwoClaim := by
  intro n G F B C B'' v hgood hC hvC hreach hdisj
  classical
  have hBF := hgood.subset
  obtain ⟨hCB, hCcl, _⟩ := mem_components (tgraph G F B) hC
  have hvB := hCB hvC
  obtain ⟨D, hDB, h1, h2, hgc⟩ := reach_invariant hBF hreach
  simp only at h1 h2 hgc
  have hD : D = {v} := by
    ext x
    rw [Finset.mem_singleton]
    constructor
    · intro hx
      by_contra hxv
      have : x ∈ F.erase v := Finset.mem_erase.mpr ⟨hxv, hBF (hDB hx)⟩
      rw [h1] at this
      exact (Finset.mem_sdiff.mp this).2 hx
    · rintro rfl
      by_contra hxD
      have : x ∈ F \ D := Finset.mem_sdiff.mpr ⟨hBF hvB, hxD⟩
      rw [← h1] at this
      exact (Finset.mem_erase.mp this).1 rfl
  subst hD
  set K := restrictG (tgraph G F B) (B \ {v}) with hK
  have hWsub : C.erase v ⊆ Finset.univ \ B'' := by
    intro u hu
    exact Finset.mem_sdiff.mpr ⟨Finset.mem_univ _,
      fun huB => Finset.disjoint_left.mp hdisj huB (Finset.mem_of_mem_erase hu)⟩
  have hWcl : ClosedIn K (Finset.univ \ B'') (C.erase v) := by
    intro u hu z _ hadj
    obtain ⟨hH, _, hzU⟩ := hadj
    obtain ⟨hzB, hzv⟩ := Finset.mem_sdiff.mp hzU
    refine Finset.mem_erase.mpr ⟨fun h => hzv (Finset.mem_singleton.mpr h), ?_⟩
    exact hCcl u (Finset.mem_of_mem_erase hu) z hzB hH
  have hparts : ∀ T ∈ components K (C.erase v),
      ∃ P : SectionDecomposition K T, P.toBagPath.WidthAtMost (12 * Real.sqrt (n : ℝ)) := by
    intro T hT
    have hT' := components_subset_of_closed hWsub hWcl hT
    have hTW := (mem_components K hT).1
    have hatt : attachment K B'' T = ∅ := by
      apply Finset.eq_empty_of_forall_notMem
      intro a ha
      obtain ⟨haB'', u, hu, hau⟩ := (mem_attachment K).mp ha
      have haC : a ∈ C := hCcl u (Finset.mem_of_mem_erase (hTW hu)) a
        (Finset.mem_sdiff.mp hau.2.1).1 hau.1.symm
      exact Finset.disjoint_left.mp hdisj haB'' haC
    have hpiece := (hgc T hT').2
    rw [hatt] at hpiece
    obtain ⟨Q, hQ⟩ := hpiece.section_decomposition (by simp)
    exact ⟨Q, hQ.mono (by linarith [Real.sqrt_le_sqrt (card_le_n T)])⟩
  obtain ⟨P, hP⟩ := section_of_components K (C.erase v)
    (show (-1 : ℝ) ≤ 12 * Real.sqrt (n : ℝ) by linarith [Real.sqrt_nonneg (n : ℝ)]) hparts
  have hw := BagPath.hold_width P.toBagPath {v} hP
  rw [Finset.card_singleton, Nat.cast_one] at hw
  apply hasPathwidth_of_bagPath (coreTorso G (F \ (B \ C)) C) (enumerate C)
    (P.toBagPath.hold {v}) hw
  · intro i
    by_cases hx : enumerate C i = v
    · exact ⟨0, Nat.zero_le _, (mem_hold_bag _ _ _ _).mpr (Or.inr (by simp [hx]))⟩
    · have hxC : enumerate C i ∈ C := (mem_iff_enumerate C _).mpr ⟨i, rfl⟩
      obtain ⟨k, hk, hmem⟩ := P.vertex_covered (enumerate C i)
        (Finset.mem_erase.mpr ⟨hx, hxC⟩)
      exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inl hmem)⟩
  · intro i j hij
    rw [coreTorso_adj_iff] at hij
    have hH := tgraph_sub_le hCB hij
    have hxC : enumerate C i ∈ C := (mem_iff_enumerate C _).mpr ⟨i, rfl⟩
    have hyC : enumerate C j ∈ C := (mem_iff_enumerate C _).mpr ⟨j, rfl⟩
    by_cases hx : enumerate C i = v
    · by_cases hy : enumerate C j = v
      · exact ⟨0, Nat.zero_le _, (mem_hold_bag _ _ _ _).mpr (Or.inr (by simp [hx])),
          (mem_hold_bag _ _ _ _).mpr (Or.inr (by simp [hy]))⟩
      obtain ⟨k, hk, hmem⟩ := P.vertex_covered (enumerate C j)
        (Finset.mem_erase.mpr ⟨hy, hyC⟩)
      exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inr (by simp [hx])),
        (mem_hold_bag _ _ _ _).mpr (Or.inl hmem)⟩
    by_cases hy : enumerate C j = v
    · obtain ⟨k, hk, hmem⟩ := P.vertex_covered (enumerate C i)
        (Finset.mem_erase.mpr ⟨hx, hxC⟩)
      exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inl hmem),
        (mem_hold_bag _ _ _ _).mpr (Or.inr (by simp [hy]))⟩
    have hKadj : K.Adj (enumerate C i) (enumerate C j) :=
      ⟨hH, Finset.mem_sdiff.mpr ⟨hCB hxC, by simpa using hx⟩,
        Finset.mem_sdiff.mpr ⟨hCB hyC, by simpa using hy⟩⟩
    obtain ⟨k, hk, hu, hv⟩ := P.edge_covered _ (Finset.mem_erase.mpr ⟨hx, hxC⟩) _
      (Finset.mem_erase.mpr ⟨hy, hyC⟩) hKadj
    exact ⟨k, hk, (mem_hold_bag _ _ _ _).mpr (Or.inl hu), (mem_hold_bag _ _ _ _).mpr (Or.inl hv)⟩

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.liftClaim
#print axioms CubicPathwidth.T4.kindTwo