MaxLeafFormal.DSTGraph

Source file MaxLeafFormal/DSTGraph.lean of the Lean project (how it is built).

Statements of the paper formalised here: Lemma D.11.14, Theorem 12.8.

import MaxLeafFormal.DSTCert
import MaxLeafFormal.MLS

/-!
# Directed Steiner Tree: `W_S ≥ W_A` (`lem:fa-dst-point`, `eq:fa-dst-W`)
The setting is that of `thm:fa-dst`: a root `r`, terminals `K`, non-terminals `U`.
-/

namespace MaxLeafFormal.DSTGraph

open Finset
open Antinorm8 (RTree)

variable {V : Type*} [Fintype V] [DecidableEq V]

/-! ### Definitions with explicit graph data -/

/-- `v` is reachable from `u` in the induced subdigraph `G[T]` (`u ∈ T`; length 0 allowed). -/
def ReachIn (G : Digraph V) (T : Finset V) (u v : V) : Prop :=
  u ∈ T ∧ Relation.ReflTransGen (fun a b => a ∈ T ∧ b ∈ T ∧ G.Adj a b) u v

/-- `\bar K_X = {r} ∪ K ∪ X` (the definition of `g` before `thm:fa-dst`). -/
def Kbar (r : V) (K X : Finset V) : Finset V := insert r (K ∪ X)

open Classical in
/-- `\bar K^r_X`: the vertices of `\bar K_X` reachable from `r` in `G[\bar K_X]`. -/
noncomputable def KbarR (G : Digraph V) (r : V) (K X : Finset V) : Finset V :=
  (Kbar r K X).filter (fun v => ReachIn G (Kbar r K X) r v)

/-- `\bar K_X \ \bar K^r_X`. -/
noncomputable def Dset (G : Digraph V) (r : V) (K X : Finset V) : Finset V :=
  Kbar r K X \ KbarR G r K X

open Classical in
/-- The strong component of `v` in `G[D]`. -/
noncomputable def scc (G : Digraph V) (D : Finset V) (v : V) : Finset V :=
  D.filter (fun w => ReachIn G D v w ∧ ReachIn G D w v)

open Classical in
/-- Source components of `G[D]`: strong components that no arc of `G[D]` enters from outside. -/
noncomputable def sourceComps (G : Digraph V) (D : Finset V) : Finset (Finset V) :=
  (D.image (scc G D)).filter (fun C => ∀ u ∈ D, ∀ v ∈ C, G.Adj u v → u ∈ C)

/-- The running-time exponent `g(X)` of a sample (defined before `thm:fa-dst`). -/
noncomputable def gDST (G : Digraph V) (r : V) (K X : Finset V) : ℕ :=
  (sourceComps G (Dset G r K X)).card

/-- The non-terminals `U = V \ ({r} ∪ K)`. -/
def nonterm (r : V) (K : Finset V) : Finset V := univ \ insert r K

/-- `S` is a Steiner set: every terminal is reachable from `r` in `G[{r} ∪ K ∪ S]`. -/
def Steiner (G : Digraph V) (r : V) (K S : Finset V) : Prop :=
  ∀ v ∈ K, ReachIn G (Kbar r K S) r v

/-- `S` is rooted: every vertex of `K ∪ S` is reachable from `r` in `G[{r} ∪ K ∪ S]`. -/
def Rooted (G : Digraph V) (r : V) (K S : Finset V) : Prop :=
  ∀ v ∈ K ∪ S, ReachIn G (Kbar r K S) r v

open Classical in
/-- The vertices of `S` reachable from `r` in `G[{r} ∪ K ∪ S]`. -/
noncomputable def reachPart (G : Digraph V) (r : V) (K S : Finset V) : Finset V :=
  S.filter (fun v => ReachIn G (Kbar r K S) r v)

/-- `W_S(y) = ∑_{X ⊆ S} y^{|X|} 2^{-g(X)}` (`def:fw-moments`, `eq:fa-dst-W`). -/
noncomputable def WS (G : Digraph V) (r : V) (K S : Finset V) (y : ℝ) : ℝ :=
  ∑ X ∈ S.powerset, y ^ X.card * (1 / 2 : ℝ) ^ gDST G r K X

/-- An out-arborescence of `G[N]` rooted at `r`: arcs `par u → u` for `u ∈ N \ {r}`. -/
structure OutArb (G : Digraph V) (r : V) (N : Finset V) where
  par : V → V
  height : V → ℕ
  par_mem : ∀ u ∈ N, u ≠ r → par u ∈ N
  par_adj : ∀ u ∈ N, u ≠ r → G.Adj (par u) u
  height_lt : ∀ u ∈ N, u ≠ r → height (par u) < height u

/-! ### Definitions on an arborescence; theorems -/

variable {G : Digraph V} {r : V} {K S : Finset V}

open Classical in
/-- `Ψ_A(X) = |{u ∈ K ∪ X : par(u) ∉ \bar K_X}|` (`lem:fa-dst-point`). -/
noncomputable def PsiG (A : OutArb G r (Kbar r K S)) (X : Finset V) : ℕ :=
  ((K ∪ X).filter (fun u => A.par u ∉ Kbar r K X)).card

/-- `W_A(y) = ∑_{X ⊆ S} y^{|X|} 2^{-Ψ_A(X)}` (`eq:fa-dst-W`). -/
noncomputable def WAg (A : OutArb G r (Kbar r K S)) (y : ℝ) : ℝ :=
  ∑ X ∈ S.powerset, y ^ X.card * (1 / 2 : ℝ) ^ PsiG A X

/-- No vertex of `S` is a leaf of `A`. -/
def NoSteinerLeafG (A : OutArb G r (Kbar r K S)) : Prop :=
  ∀ v ∈ S, ∃ u ∈ K ∪ S, A.par u = v

/-! ### Helper lemmas: reachability -/

theorem ReachIn.of_mem {T : Finset V} {u : V} (hu : u ∈ T) : ReachIn G T u u :=
  ⟨hu, Relation.ReflTransGen.refl⟩

theorem ReachIn.mem_right {T : Finset V} {u v : V} (h : ReachIn G T u v) : v ∈ T := by
  obtain ⟨hu, h⟩ := h
  induction h with
  | refl => exact hu
  | tail _ hbc _ => exact hbc.2.1

theorem ReachIn.tail_adj {T : Finset V} {u a b : V} (h : ReachIn G T u a) (hb : b ∈ T)
    (hab : G.Adj a b) : ReachIn G T u b :=
  ⟨h.1, h.2.tail ⟨h.mem_right, hb, hab⟩⟩

theorem ReachIn.trans {T : Finset V} {u v w : V} (h₁ : ReachIn G T u v)
    (h₂ : ReachIn G T v w) : ReachIn G T u w :=
  ⟨h₁.1, h₁.2.trans h₂.2⟩

/-- A set containing `u` and closed under the arcs inside `T` contains every vertex that `u`
reaches inside `T`. -/
theorem ReachIn.mem_of_closed {T Z : Finset V} {u v : V} (hu : u ∈ Z)
    (hZ : ∀ a ∈ Z, ∀ b ∈ T, G.Adj a b → b ∈ Z) (h : ReachIn G T u v) : v ∈ Z := by
  obtain ⟨-, h⟩ := h
  induction h with
  | refl => exact hu
  | tail _ hbc ih => exact hZ _ ih _ hbc.2.1 hbc.2.2

/-- The backward version of `ReachIn.mem_of_closed`. -/
theorem ReachIn.mem_of_back_closed {T Z : Finset V} {u v : V} (hv : v ∈ Z)
    (hZ : ∀ a ∈ T, ∀ b ∈ Z, G.Adj a b → a ∈ Z) (h : ReachIn G T u v) : u ∈ Z := by
  obtain ⟨-, h⟩ := h
  induction h using Relation.ReflTransGen.head_induction_on with
  | refl => exact hv
  | head hac _ ih => exact hZ _ hac.1 _ ih hac.2.2

theorem mem_Kbar {X : Finset V} {v : V} : v ∈ Kbar r K X ↔ v = r ∨ v ∈ K ∨ v ∈ X := by
  simp only [Kbar, Finset.mem_insert, Finset.mem_union]

theorem r_mem_Kbar {X : Finset V} : r ∈ Kbar r K X := Finset.mem_insert_self _ _

theorem mem_nonterm {v : V} : v ∈ nonterm r K ↔ v ≠ r ∧ v ∉ K := by
  simp [nonterm]

theorem mem_KbarR {X : Finset V} {v : V} :
    v ∈ KbarR G r K X ↔ v ∈ Kbar r K X ∧ ReachIn G (Kbar r K X) r v := by
  simp only [KbarR, Finset.mem_filter]

theorem mem_Dset {X : Finset V} {v : V} :
    v ∈ Dset G r K X ↔ v ∈ Kbar r K X ∧ ¬ ReachIn G (Kbar r K X) r v := by
  simp only [Dset, Finset.mem_sdiff, mem_KbarR]
  tauto

theorem mem_scc {D : Finset V} {v w : V} :
    w ∈ scc G D v ↔ w ∈ D ∧ ReachIn G D v w ∧ ReachIn G D w v := by
  simp only [scc, Finset.mem_filter]

theorem scc_self {D : Finset V} {v : V} (hv : v ∈ D) : v ∈ scc G D v :=
  mem_scc.2 ⟨hv, ReachIn.of_mem hv, ReachIn.of_mem hv⟩

theorem scc_eq_of_mem {D : Finset V} {v w : V} (h : w ∈ scc G D v) :
    scc G D w = scc G D v := by
  rw [mem_scc] at h
  ext x
  rw [mem_scc, mem_scc]
  constructor
  · rintro ⟨hx, h1, h2⟩
    exact ⟨hx, h.2.1.trans h1, h2.trans h.2.2⟩
  · rintro ⟨hx, h1, h2⟩
    exact ⟨hx, h.2.2.trans h1, h2.trans h.2.1⟩

theorem mem_sourceComps {D C : Finset V} :
    C ∈ sourceComps G D ↔
      (∃ v ∈ D, scc G D v = C) ∧ ∀ u ∈ D, ∀ v ∈ C, G.Adj u v → u ∈ C := by
  simp only [sourceComps, Finset.mem_filter, Finset.mem_image]

/-- A source component is closed under backward reachability (the vertex form of the
source condition). -/
theorem mem_of_mem_sourceComps {D C : Finset V} {u w : V} (hC : C ∈ sourceComps G D)
    (hw : w ∈ C) (h : ReachIn G D u w) : u ∈ C :=
  ReachIn.mem_of_back_closed hw (mem_sourceComps.1 hC).2 h

/-- Every vertex of `D_X` has a "top": a vertex of `D_X` that reaches it inside `D_X` and whose
parent lies outside `\bar K_X` (proof of `lem:fa-dst-point`). -/
theorem exists_top (A : OutArb G r (Kbar r K S)) {X : Finset V} (hX : X ⊆ S) :
    ∀ (n : ℕ) (v : V), v ∈ Dset G r K X → A.height v < n →
      ∃ u ∈ Dset G r K X, ReachIn G (Dset G r K X) u v ∧ A.par u ∉ Kbar r K X := by
  have hKS : Kbar r K X ⊆ Kbar r K S := by
    intro w hw
    rw [mem_Kbar] at hw ⊢
    rcases hw with h | h | h
    · exact Or.inl h
    · exact Or.inr (Or.inl h)
    · exact Or.inr (Or.inr (hX h))
  intro n
  induction n with
  | zero => intro v _ h; exact absurd h (Nat.not_lt_zero _)
  | succ n ih =>
    intro v hv hlt
    have hvK : v ∈ Kbar r K X := (mem_Dset.1 hv).1
    have hvr : v ≠ r := by
      rintro rfl
      exact (mem_Dset.1 hv).2 (ReachIn.of_mem r_mem_Kbar)
    by_cases hp : A.par v ∈ Kbar r K X
    · have hadj := A.par_adj v (hKS hvK) hvr
      have hpD : A.par v ∈ Dset G r K X := by
        rw [mem_Dset]
        exact ⟨hp, fun h => (mem_Dset.1 hv).2 (h.tail_adj hvK hadj)⟩
      have h1 := A.height_lt v (hKS hvK) hvr
      obtain ⟨u, hu, hreach, hpar⟩ := ih (A.par v) hpD (by omega)
      exact ⟨u, hu, hreach.tail_adj hv hadj, hpar⟩
    · exact ⟨v, hv, ReachIn.of_mem hv, hp⟩

/-! ### Helper lemmas for the examples -/

theorem gDST_eq_zero_of {X : Finset V} (h : ∀ v ∈ Kbar r K X, ReachIn G (Kbar r K X) r v) :
    gDST G r K X = 0 := by
  have hD : Dset G r K X = ∅ :=
    Finset.eq_empty_iff_forall_notMem.2
      (fun v hv => (mem_Dset.1 hv).2 (h v (mem_Dset.1 hv).1))
  rw [gDST, hD]
  simp [sourceComps]

theorem Dset_eq_of {X R : Finset V} (hr : r ∈ R) (hR : ∀ v ∈ R, ReachIn G (Kbar r K X) r v)
    (hcl : ∀ a ∈ R, ∀ b ∈ Kbar r K X, G.Adj a b → b ∈ R) :
    Dset G r K X = Kbar r K X \ R := by
  ext v
  rw [mem_Dset, Finset.mem_sdiff]
  constructor
  · rintro ⟨hv, hn⟩
    exact ⟨hv, fun h => hn (hR v h)⟩
  · rintro ⟨hv, hn⟩
    exact ⟨hv, fun h => hn (h.mem_of_closed hr hcl)⟩

theorem sourceComps_eq_single {D : Finset V} (hne : D.Nonempty)
    (h : ∀ v ∈ D, ∀ w ∈ D, ReachIn G D v w) : sourceComps G D = {D} := by
  have hscc : ∀ v ∈ D, scc G D v = D := by
    intro v hv
    ext w
    rw [mem_scc]
    exact ⟨fun hw => hw.1, fun hw => ⟨hw, h v hv w hw, h w hw v hv⟩⟩
  ext C
  rw [mem_sourceComps, Finset.mem_singleton]
  constructor
  · rintro ⟨⟨v, hv, rfl⟩, -⟩
    exact hscc v hv
  · rintro rfl
    obtain ⟨v, hv⟩ := hne
    exact ⟨⟨v, hv, hscc v hv⟩, fun u hu _ _ _ => hu⟩

theorem strong_of_adj {D : Finset V} (h : ∀ v ∈ D, ∀ w ∈ D, v = w ∨ G.Adj v w) :
    ∀ v ∈ D, ∀ w ∈ D, ReachIn G D v w := by
  intro v hv w hw
  rcases h v hv w hw with rfl | hadj
  · exact ReachIn.of_mem hv
  · exact (ReachIn.of_mem hv).tail_adj hw hadj

/-! ### Helpers for `exists_outArb` and `exists_rtree` -/

namespace Aux

/-- `v` is reached from `r` by a walk of exactly `d` arcs inside `N`. -/
def RW (G : Digraph V) (N : Finset V) (r : V) : ℕ → V → Prop
  | 0, v => v = r
  | d + 1, v => ∃ a, RW G N r d a ∧ a ∈ N ∧ v ∈ N ∧ G.Adj a v

theorem exists_RW {N : Finset V} {v : V} (h : ReachIn G N r v) : ∃ d, RW G N r d v := by
  obtain ⟨-, h⟩ := h
  induction h with
  | refl => exact ⟨0, by simp only [RW]⟩
  | tail _ hbc ih =>
    obtain ⟨d, hd⟩ := ih
    exact ⟨d + 1, by simp only [RW]; exact ⟨_, hd, hbc.1, hbc.2.1, hbc.2.2⟩⟩

/-- The children of `v`: the vertices `u ∈ N \ {r}` with `par u = v`, in some order. -/
noncomputable def kids (par : V → V) (N : Finset V) (r v : V) : List V :=
  (N.filter (fun u => u ≠ r ∧ par u = v)).toList

/-- Follow a list of child indices from `v`. -/
noncomputable def walk (par : V → V) (N : Finset V) (r : V) : V → List ℕ → Option V
  | v, [] => some v
  | v, i :: p => ((kids par N r v)[i]?).bind (fun c => walk par N r c p)

/-- The label of a vertex: `steiner` on `S`, `term` elsewhere. -/
def lab (S : Finset V) (v : V) : DSTCert.Kind := if v ∈ S then .steiner else .term

/-- The tree below `v`, cut at depth `n`. -/
noncomputable def tree (par : V → V) (N S : Finset V) (r : V) : ℕ → V → RTree DSTCert.Kind
  | 0, v => .node (lab S v) []
  | n + 1, v => .node (lab S v) ((kids par N r v).map (tree par N S r n))

/-- The vertex at a position (`r` off the tree). -/
noncomputable def phi (par : V → V) (N : Finset V) (r : V) (p : List ℕ) : V :=
  (walk par N r r p).getD r

/-- The positions in `P` whose vertex lies in `X`. -/
noncomputable def pre (par : V → V) (N : Finset V) (r : V) (P : Finset (List ℕ))
    (X : Finset V) : Finset (List ℕ) :=
  P.filter (fun p => phi par N r p ∈ X)

theorem mem_of_getElem {l : List V} {i : ℕ} {a : V} (h : l[i]? = some a) : a ∈ l :=
  List.mem_iff_getElem?.2 ⟨i, h⟩

theorem getElem_inj_of_nodup {l : List V} (hl : l.Nodup) {i j : ℕ} {a : V}
    (hi : l[i]? = some a) (hj : l[j]? = some a) : i = j := by
  rw [List.getElem?_eq_some_iff] at hi hj
  obtain ⟨hi', rfl⟩ := hi
  obtain ⟨hj', hj⟩ := hj
  exact (List.Nodup.getElem_inj_iff hl).1 hj.symm

theorem mem_kids {par : V → V} {N : Finset V} {v c : V} :
    c ∈ kids par N r v ↔ c ∈ N ∧ c ≠ r ∧ par c = v := by
  simp only [kids, Finset.mem_toList, Finset.mem_filter]

theorem walk_nil (par : V → V) (N : Finset V) (v : V) : walk par N r v [] = some v := by
  simp only [walk]

theorem walk_cons (par : V → V) (N : Finset V) (v : V) (i : ℕ) (p : List ℕ) :
    walk par N r v (i :: p) = ((kids par N r v)[i]?).bind (fun c => walk par N r c p) := by
  simp only [walk]

theorem walk_append (par : V → V) (N : Finset V) (p : List ℕ) :
    ∀ (v : V) (i : ℕ),
      walk par N r v (p ++ [i]) = (walk par N r v p).bind (fun u => (kids par N r u)[i]?) := by
  induction p with
  | nil => intro v i; simp [walk]
  | cons j p ih =>
    intro v i
    rw [List.cons_append, walk_cons, walk_cons, Option.bind_assoc]
    congr 1
    funext c
    exact ih c i

theorem walk_spec {N : Finset V} (A : OutArb G r N) :
    ∀ (p : List ℕ) (v u : V), v ∈ N → walk A.par N r v p = some u →
      u ∈ N ∧ A.height v + p.length ≤ A.height u := by
  intro p
  induction p with
  | nil =>
    intro v u hv h
    rw [walk_nil] at h
    cases h
    exact ⟨hv, by simp⟩
  | cons i q ih =>
    intro v u hv h
    rw [walk_cons] at h
    cases hc : (kids A.par N r v)[i]? with
    | none => rw [hc] at h; simp at h
    | some c =>
      rw [hc] at h
      obtain ⟨hcN, hcr, hcp⟩ := mem_kids.1 (mem_of_getElem hc)
      have h1 := A.height_lt c hcN hcr
      rw [hcp] at h1
      obtain ⟨huN, hu⟩ := ih c u hcN h
      refine ⟨huN, ?_⟩
      simp only [List.length_cons]
      omega

theorem walk_last (par : V → V) (N : Finset V) {v u : V} {p : List ℕ} (hp : p ≠ [])
    (h : walk par N r v p = some u) :
    ∃ w, walk par N r v p.dropLast = some w ∧ (kids par N r w)[p.getLast hp]? = some u := by
  rw [← List.dropLast_append_getLast hp, walk_append] at h
  cases hw : walk par N r v p.dropLast with
  | none => rw [hw] at h; simp at h
  | some w => rw [hw] at h; exact ⟨w, rfl, h⟩

theorem walk_inj {N : Finset V} (A : OutArb G r N) {v : V} (hv : v ∈ N) :
    ∀ (n : ℕ) (p q : List ℕ) (u : V), p.length < n → walk A.par N r v p = some u →
      walk A.par N r v q = some u → p = q := by
  -- a nonempty walk from `v` does not return to `v`
  have hne : ∀ (s : List ℕ), s ≠ [] → walk A.par N r v s = some v → False := by
    intro s hs h
    obtain ⟨w, hw, hwv⟩ := walk_last A.par N hs h
    obtain ⟨hvN, hvr, hvp⟩ := mem_kids.1 (mem_of_getElem hwv)
    have h1 := A.height_lt v hvN hvr
    rw [hvp] at h1
    have h2 := (walk_spec A _ v w hv hw).2
    omega
  intro n
  induction n with
  | zero => intro p q u h; exact absurd h (Nat.not_lt_zero _)
  | succ n ih =>
    intro p q u hlen hp hq
    by_cases hp0 : p = []
    · subst hp0
      rw [walk_nil] at hp
      cases hp
      by_cases hq0 : q = []
      · exact hq0.symm
      · exact (hne q hq0 hq).elim
    · by_cases hq0 : q = []
      · subst hq0
        rw [walk_nil] at hq
        cases hq
        exact (hne p hp0 hp).elim
      · obtain ⟨w, hw, hwu⟩ := walk_last A.par N hp0 hp
        obtain ⟨w', hw', hwu'⟩ := walk_last A.par N hq0 hq
        have e1 := (mem_kids.1 (mem_of_getElem hwu)).2.2
        have e2 := (mem_kids.1 (mem_of_getElem hwu')).2.2
        rw [e1] at e2
        subst e2
        have hpos : 0 < p.length := by
          cases p with
          | nil => exact absurd rfl hp0
          | cons a l => simp
        have hlt : p.dropLast.length < n := by
          rw [List.length_dropLast]
          omega
        have hd := ih p.dropLast q.dropLast w hlt hw hw'
        have hi := getElem_inj_of_nodup (Finset.nodup_toList _) hwu hwu'
        rw [← List.dropLast_append_getLast hp0, ← List.dropLast_append_getLast hq0, hd, hi]

theorem walk_surj {N : Finset V} (A : OutArb G r N) :
    ∀ (n : ℕ) (u : V), u ∈ N → A.height u < n → ∃ p, walk A.par N r r p = some u := by
  intro n
  induction n with
  | zero => intro u _ h; exact absurd h (Nat.not_lt_zero _)
  | succ n ih =>
    intro u hu hlt
    by_cases hur : u = r
    · exact ⟨[], by rw [walk_nil, hur]⟩
    · have h1 := A.height_lt u hu hur
      obtain ⟨p, hp⟩ := ih (A.par u) (A.par_mem u hu hur) (by omega)
      have hmem : u ∈ kids A.par N r (A.par u) := mem_kids.2 ⟨hu, hur, rfl⟩
      obtain ⟨i, hi⟩ := List.mem_iff_getElem?.1 hmem
      exact ⟨p ++ [i], by rw [walk_append, hp]; exact hi⟩

theorem lab_eq_steiner {S : Finset V} {u : V} : lab S u = .steiner ↔ u ∈ S := by
  unfold lab
  split_ifs with h <;> simp [h]

theorem lab_eq_term {S : Finset V} {u : V} : lab S u = .term ↔ u ∉ S := by
  unfold lab
  split_ifs with h <;> simp [h]

theorem rootKind_tree (par : V → V) (N S : Finset V) (n : ℕ) (v : V) :
    DSTCert.rootKind (tree par N S r n v) = lab S v := by
  cases n <;> rfl

theorem labelAt_tree {N : Finset V} (A : OutArb G r N) (S : Finset V) :
    ∀ (n : ℕ) (v : V) (p : List ℕ), v ∈ N → N.sup A.height ≤ A.height v + n →
      DSTCert.labelAt (tree A.par N S r n v) p = (walk A.par N r v p).map (lab S) := by
  intro n
  induction n with
  | zero =>
    intro v p hv hM
    cases p with
    | nil => simp [tree, walk_nil, DSTCert.labelAt_nil]
    | cons i q =>
      have hk : kids A.par N r v = [] := by
        cases hk : kids A.par N r v with
        | nil => rfl
        | cons c l =>
          exfalso
          have hc : c ∈ kids A.par N r v := by rw [hk]; simp
          obtain ⟨hcN, hcr, hcp⟩ := mem_kids.1 hc
          have h1 := A.height_lt c hcN hcr
          have h2 : A.height c ≤ N.sup A.height := Finset.le_sup hcN
          rw [hcp] at h1
          omega
      simp [tree, walk_cons, DSTCert.labelAt_cons, hk]
  | succ n ih =>
    intro v p hv hM
    cases p with
    | nil => simp [tree, walk_nil, DSTCert.labelAt_nil]
    | cons i q =>
      simp only [tree]
      rw [walk_cons, DSTCert.labelAt_cons, List.getElem?_map]
      cases hc : (kids A.par N r v)[i]? with
      | none => simp
      | some c =>
        obtain ⟨hcN, hcr, hcp⟩ := mem_kids.1 (mem_of_getElem hc)
        have h1 := A.height_lt c hcN hcr
        rw [hcp] at h1
        have := ih c q hcN (by omega)
        simpa using this

theorem noLeaf_tree (A : OutArb G r (Kbar r K S)) (hrK : r ∉ K) (hrS : r ∉ S)
    (hNL : NoSteinerLeafG A) : ∀ (n : ℕ) (v : V), v ∈ Kbar r K S →
      (Kbar r K S).sup A.height ≤ A.height v + n →
      DSTCert.NoSteinerLeaf (tree A.par (Kbar r K S) S r n v) := by
  have hchild : ∀ v ∈ S, ∃ c, c ∈ kids A.par (Kbar r K S) r v := by
    intro v hv
    obtain ⟨u, hu, hpu⟩ := hNL v hv
    rw [Finset.mem_union] at hu
    refine ⟨u, mem_kids.2 ⟨?_, ?_, hpu⟩⟩
    · rw [mem_Kbar]
      tauto
    · rintro rfl
      tauto
  intro n
  induction n with
  | zero =>
    intro v hv hM
    simp only [tree]
    rw [DSTCert.NoSteinerLeaf]
    refine ⟨fun hs => ?_, by simp [DSTCert.NoSteinerLeafAll]⟩
    exfalso
    obtain ⟨c, hc⟩ := hchild v (lab_eq_steiner.1 hs)
    obtain ⟨hcN, hcr, hcp⟩ := mem_kids.1 hc
    have h1 := A.height_lt c hcN hcr
    have h2 : A.height c ≤ (Kbar r K S).sup A.height := Finset.le_sup hcN
    rw [hcp] at h1
    omega
  | succ n ih =>
    intro v hv hM
    simp only [tree]
    rw [DSTCert.NoSteinerLeaf, DSTCert.rec_noLeafAll_iff]
    refine ⟨fun hs => ?_, fun c hc => ?_⟩
    · obtain ⟨c, hc⟩ := hchild v (lab_eq_steiner.1 hs)
      cases hk : kids A.par (Kbar r K S) r v with
      | nil => rw [hk] at hc; simp at hc
      | cons a l => simp
    · rw [List.mem_map] at hc
      obtain ⟨c', hc', rfl⟩ := hc
      obtain ⟨hcN, hcr, hcp⟩ := mem_kids.1 hc'
      have h1 := A.height_lt c' hcN hcr
      rw [hcp] at h1
      exact ih c' hcN (by omega)

/-- `count k t` is the number of positions labelled `k` (any tree). -/
theorem count_eq_card (k : DSTCert.Kind) : ∀ t : RTree DSTCert.Kind,
    DSTCert.count k t =
      ((DSTCert.positions t).filter (fun p => DSTCert.labelAt t p = some k)).card := by
  refine Antinorm8.RTree.ind _ ?_
  intro k' cs ih
  have hall : ∀ (cs' pre : List (RTree DSTCert.Kind)),
      (∀ c ∈ cs', DSTCert.count k c =
        ((DSTCert.positions c).filter (fun p => DSTCert.labelAt c p = some k)).card) →
      ((DSTCert.positionsAll pre.length cs').filter
        (fun p => DSTCert.labelAt (.node k' (pre ++ cs')) p = some k)).card =
        DSTCert.countAll k cs' := by
    intro cs'
    induction cs' with
    | nil => intro pre _; simp [DSTCert.positionsAll_nil, DSTCert.countAll]
    | cons c cs' ihc =>
      intro pre h
      have hdisj : Disjoint ((DSTCert.positions c).map (DSTCert.consEmb pre.length))
          (DSTCert.positionsAll (pre.length + 1) cs') := by
        rw [Finset.disjoint_left]
        intro p hp1 hp2
        obtain ⟨q, _, rfl⟩ := Finset.mem_map.1 hp1
        obtain ⟨a, q', he, ha, -⟩ :=
          (DSTCert.mem_positionsAll_aux cs' (fun c _ p => DSTCert.mem_positions_iff) _ _).1 hp2
        rw [DSTCert.consEmb_apply] at he
        have := (List.cons.inj he).1
        omega
      have hlc : ∀ q, DSTCert.labelAt (.node k' (pre ++ c :: cs')) (pre.length :: q) =
          DSTCert.labelAt c q := by
        intro q
        rw [DSTCert.labelAt_cons, List.getElem?_append_right (le_refl _), Nat.sub_self]
        rfl
      have ih2 := ihc (pre ++ [c]) (fun c' hc' => h c' (List.mem_cons_of_mem _ hc'))
      rw [List.length_append, List.length_singleton, List.append_assoc,
        List.singleton_append] at ih2
      rw [DSTCert.positionsAll_cons, Finset.filter_union,
        Finset.card_union_of_disjoint (Finset.disjoint_filter_filter hdisj), Finset.filter_map,
        Finset.card_map, ih2, DSTCert.countAll, h c (List.mem_cons_self ..)]
      congr 2
      ext q
      simp only [Finset.mem_filter, Function.comp_apply, DSTCert.consEmb_apply, hlc]
  have hnot : ([] : List ℕ) ∉ DSTCert.positionsAll 0 cs := by
    intro hm
    obtain ⟨a, q, he, -⟩ :=
      (DSTCert.mem_positionsAll_aux cs (fun c _ p => DSTCert.mem_positions_iff) _ _).1 hm
    simp at he
  have h0 := hall cs [] ih
  simp only [List.length_nil, List.nil_append] at h0
  rw [Finset.card_filter, DSTCert.positions_node, Finset.sum_insert hnot, ← Finset.card_filter,
    h0, DSTCert.labelAt_nil, DSTCert.count]
  simp

theorem phi_of {par : V → V} {N : Finset V} {p : List ℕ} {u : V}
    (h : walk par N r r p = some u) : phi par N r p = u := by
  rw [phi, h]
  rfl

theorem mem_pre {par : V → V} {N : Finset V} {P : Finset (List ℕ)} {X : Finset V}
    {p : List ℕ} : p ∈ pre par N r P X ↔ p ∈ P ∧ phi par N r p ∈ X := by
  simp only [pre, Finset.mem_filter]

theorem labelAt_T {N : Finset V} (A : OutArb G r N) (hrN : r ∈ N) (S : Finset V)
    (p : List ℕ) :
    DSTCert.labelAt (tree A.par N S r (N.sup A.height) r) p =
      (walk A.par N r r p).map (lab S) :=
  labelAt_tree A S _ r p hrN (Nat.le_add_left _ _)

theorem mem_positions_T {N : Finset V} (A : OutArb G r N) (hrN : r ∈ N) (S : Finset V)
    (p : List ℕ) :
    p ∈ DSTCert.positions (tree A.par N S r (N.sup A.height) r) ↔
      ∃ u, walk A.par N r r p = some u := by
  rw [DSTCert.mem_positions_iff, labelAt_T A hrN S p]
  cases walk A.par N r r p <;> simp

theorem mem_steinerPos_T {N : Finset V} (A : OutArb G r N) (hrN : r ∈ N) (S : Finset V)
    (p : List ℕ) :
    p ∈ DSTCert.steinerPos (tree A.par N S r (N.sup A.height) r) ↔
      ∃ u, walk A.par N r r p = some u ∧ u ∈ S := by
  rw [DSTCert.steinerPos, Finset.mem_filter, mem_positions_T A hrN S p, labelAt_T A hrN S p]
  cases walk A.par N r r p with
  | none => simp
  | some u => simp [lab_eq_steiner]

theorem card_transfer {N : Finset V} (A : OutArb G r N) (hrN : r ∈ N) (S : Finset V)
    (P : V → Prop) [DecidablePred P] :
    ((DSTCert.positions (tree A.par N S r (N.sup A.height) r)).filter
      (fun p => P (phi A.par N r p))).card = (N.filter P).card := by
  refine Finset.card_nbij (phi A.par N r) ?_ ?_ ?_
  · intro p hp
    rw [Finset.mem_coe, Finset.mem_filter] at hp
    rw [Finset.mem_coe, Finset.mem_filter]
    obtain ⟨u, hu⟩ := (mem_positions_T A hrN S p).1 hp.1
    have h2 := hp.2
    rw [phi_of hu] at h2 ⊢
    exact ⟨(walk_spec A p r u hrN hu).1, h2⟩
  · intro p₁ h₁ p₂ h₂ he
    have h₁' := (Finset.mem_filter.1 (Finset.mem_coe.1 h₁)).1
    have h₂' := (Finset.mem_filter.1 (Finset.mem_coe.1 h₂)).1
    obtain ⟨u₁, hu₁⟩ := (mem_positions_T A hrN S p₁).1 h₁'
    obtain ⟨u₂, hu₂⟩ := (mem_positions_T A hrN S p₂).1 h₂'
    rw [phi_of hu₁, phi_of hu₂] at he
    subst he
    exact walk_inj A hrN _ p₁ p₂ u₁ (Nat.lt_succ_self _) hu₁ hu₂
  · intro u hu
    obtain ⟨huN, hPu⟩ := Finset.mem_filter.1 (Finset.mem_coe.1 hu)
    obtain ⟨p, hp⟩ := walk_surj A _ u huN (Nat.lt_succ_self _)
    refine ⟨p, ?_, phi_of hp⟩
    rw [Finset.mem_coe, Finset.mem_filter, mem_positions_T A hrN S p, phi_of hp]
    exact ⟨⟨u, hp⟩, hPu⟩

theorem count_T {N : Finset V} (A : OutArb G r N) (hrN : r ∈ N) (S : Finset V)
    (k : DSTCert.Kind) :
    DSTCert.count k (tree A.par N S r (N.sup A.height) r) =
      (N.filter (fun u => lab S u = k)).card := by
  rw [count_eq_card, ← card_transfer A hrN S (fun u => lab S u = k)]
  congr 1
  refine Finset.filter_congr (fun p hp => ?_)
  obtain ⟨u, hu⟩ := (mem_positions_T A hrN S p).1 hp
  rw [labelAt_T A hrN S p, hu, phi_of hu]
  simp

theorem phi_injOn {N : Finset V} (A : OutArb G r N) (hrN : r ∈ N) (S : Finset V)
    {p q : List ℕ} (hp : p ∈ DSTCert.positions (tree A.par N S r (N.sup A.height) r))
    (hq : q ∈ DSTCert.positions (tree A.par N S r (N.sup A.height) r))
    (h : phi A.par N r p = phi A.par N r q) : p = q := by
  obtain ⟨u, hu⟩ := (mem_positions_T A hrN S p).1 hp
  obtain ⟨u', hu'⟩ := (mem_positions_T A hrN S q).1 hq
  rw [phi_of hu, phi_of hu'] at h
  subst h
  exact walk_inj A hrN _ p q u (Nat.lt_succ_self _) hu hu'

theorem inKbar_T (A : OutArb G r (Kbar r K S)) (hrK : r ∉ K) (hSU : S ⊆ nonterm r K)
    {X' : Finset (List ℕ)}
    (hX' : X' ⊆ DSTCert.steinerPos
      (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r))
    {p : List ℕ} {u : V} (hp : walk A.par (Kbar r K S) r r p = some u) :
    DSTCert.inKbar (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r) X' p ↔
      u ∈ Kbar r K (X'.image (phi A.par (Kbar r K S) r)) := by
  have hrS : r ∉ S := fun h => (mem_nonterm.1 (hSU h)).1 rfl
  have hSK : ∀ w ∈ S, w ∉ K := fun w hw => (mem_nonterm.1 (hSU hw)).2
  have huN := (walk_spec A p r u r_mem_Kbar hp).1
  have hmem : p ∈ X' ↔ u ∈ X'.image (phi A.par (Kbar r K S) r) := by
    rw [Finset.mem_image]
    constructor
    · intro h
      exact ⟨p, h, phi_of hp⟩
    · rintro ⟨q, hq, hqu⟩
      obtain ⟨u', hu', -⟩ := (mem_steinerPos_T A r_mem_Kbar S q).1 (hX' hq)
      rw [phi_of hu'] at hqu
      subst hqu
      rw [walk_inj A r_mem_Kbar _ p q u' (Nat.lt_succ_self _) hp hu']
      exact hq
  have hX'S : p ∈ X' → u ∈ S := by
    intro h
    obtain ⟨u', hu', hS⟩ := (mem_steinerPos_T A r_mem_Kbar S p).1 (hX' h)
    rw [hp] at hu'
    cases hu'
    exact hS
  rw [DSTCert.inKbar, labelAt_T A r_mem_Kbar S p, hp, mem_Kbar, ← hmem]
  have hlab : Option.map (lab S) (some u) = some DSTCert.Kind.term ↔ u ∉ S := by
    simp [lab_eq_term]
  rw [hlab]
  rw [mem_Kbar] at huN
  constructor
  · rintro (h | h)
    · rcases huN with h' | h' | h'
      · exact Or.inl h'
      · exact Or.inr (Or.inl h')
      · exact absurd h' h
    · exact Or.inr (Or.inr h)
  · rintro (h | h | h)
    · left
      rw [h]
      exact hrS
    · left
      exact fun hs => hSK u hs h
    · exact Or.inr h

theorem PsiA_T (A : OutArb G r (Kbar r K S)) (hrK : r ∉ K) (hSU : S ⊆ nonterm r K)
    {X' : Finset (List ℕ)}
    (hX' : X' ⊆ DSTCert.steinerPos
      (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r)) :
    DSTCert.PsiA (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r) X' =
      PsiG A (X'.image (phi A.par (Kbar r K S) r)) := by
  have hrS : r ∉ S := fun h => (mem_nonterm.1 (hSU h)).1 rfl
  have hXS : X'.image (phi A.par (Kbar r K S) r) ⊆ S := by
    intro u hu
    obtain ⟨q, hq, rfl⟩ := Finset.mem_image.1 hu
    obtain ⟨u', hu', hS⟩ := (mem_steinerPos_T A r_mem_Kbar S q).1 (hX' hq)
    rw [phi_of hu']
    exact hS
  have e1 : PsiG A (X'.image (phi A.par (Kbar r K S) r)) =
      ((Kbar r K S).filter (fun u => u ∈ K ∪ X'.image (phi A.par (Kbar r K S) r) ∧
        A.par u ∉ Kbar r K (X'.image (phi A.par (Kbar r K S) r)))).card := by
    rw [PsiG]
    congr 1
    ext u
    simp only [Finset.mem_filter]
    constructor
    · rintro ⟨h1, h2⟩
      refine ⟨?_, h1, h2⟩
      rw [mem_Kbar]
      rw [Finset.mem_union] at h1
      rcases h1 with h | h
      · exact Or.inr (Or.inl h)
      · exact Or.inr (Or.inr (hXS h))
    · rintro ⟨-, h1, h2⟩
      exact ⟨h1, h2⟩
  rw [e1, ← card_transfer A r_mem_Kbar S (fun u => u ∈ K ∪ X'.image (phi A.par (Kbar r K S) r) ∧
        A.par u ∉ Kbar r K (X'.image (phi A.par (Kbar r K S) r))), DSTCert.PsiA]
  congr 1
  refine Finset.filter_congr (fun p hp => ?_)
  obtain ⟨u, hu⟩ := (mem_positions_T A r_mem_Kbar S p).1 hp
  rw [phi_of hu, inKbar_T A hrK hSU hX' hu]
  show _ ↔ (u ∈ K ∪ X'.image (phi A.par (Kbar r K S) r) ∧
    A.par u ∉ Kbar r K (X'.image (phi A.par (Kbar r K S) r)))
  constructor
  · rintro ⟨hne, hin, hnot⟩
    obtain ⟨w, hw, hwu⟩ := walk_last A.par _ hne hu
    obtain ⟨-, hur, hpw⟩ := mem_kids.1 (mem_of_getElem hwu)
    rw [inKbar_T A hrK hSU hX' hw, ← hpw] at hnot
    refine ⟨?_, hnot⟩
    rw [mem_Kbar] at hin
    rw [Finset.mem_union]
    rcases hin with h | h | h
    · exact absurd h hur
    · exact Or.inl h
    · exact Or.inr h
  · rintro ⟨hin, hnot⟩
    have hur : u ≠ r := by
      rintro rfl
      rw [Finset.mem_union] at hin
      rcases hin with h | h
      · exact hrK h
      · exact hrS (hXS h)
    have hne : p ≠ [] := by
      rintro rfl
      rw [walk_nil] at hu
      cases hu
      exact hur rfl
    obtain ⟨w, hw, hwu⟩ := walk_last A.par _ hne hu
    obtain ⟨-, -, hpw⟩ := mem_kids.1 (mem_of_getElem hwu)
    refine ⟨hne, ?_, ?_⟩
    · rw [mem_Kbar]
      rw [Finset.mem_union] at hin
      tauto
    · rw [inKbar_T A hrK hSU hX' hw, ← hpw]
      exact hnot

theorem WA_T (A : OutArb G r (Kbar r K S)) (hrK : r ∉ K) (hSU : S ⊆ nonterm r K) (y : ℝ) :
    DSTCert.WA y (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r) = WAg A y := by
  have hSN : S ⊆ Kbar r K S := fun u hu => by rw [mem_Kbar]; exact Or.inr (Or.inr hu)
  have hsub : DSTCert.steinerPos (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r) ⊆
      DSTCert.positions (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r) :=
    DSTCert.steinerPos_subset _
  rw [DSTCert.WA, WAg]
  refine Finset.sum_nbij' (Finset.image (phi A.par (Kbar r K S) r))
    (pre A.par (Kbar r K S) r
      (DSTCert.steinerPos (tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r)))
    ?_ ?_ ?_ ?_ ?_
  · intro X' hX'
    have hX'' : X' ⊆ _ := Finset.mem_powerset.1 (by simpa using hX')
    simp only [Finset.mem_powerset]
    intro u hu
    obtain ⟨q, hq, rfl⟩ := Finset.mem_image.1 hu
    obtain ⟨u', hu', hS⟩ := (mem_steinerPos_T A r_mem_Kbar S q).1 (hX'' hq)
    rw [phi_of hu']
    exact hS
  · intro X _
    simp only [Finset.mem_powerset]
    intro p hp
    exact (mem_pre.1 hp).1
  · intro X' hX'
    have hX'' : X' ⊆ _ := Finset.mem_powerset.1 (by simpa using hX')
    ext p
    rw [mem_pre, Finset.mem_image]
    constructor
    · rintro ⟨hp, q, hq, hqp⟩
      rw [phi_injOn A r_mem_Kbar S (hsub (hX'' hq)) (hsub hp) hqp] at hq
      exact hq
    · intro hp
      exact ⟨hX'' hp, p, hp, rfl⟩
  · intro X hX
    have hX'' : X ⊆ S := Finset.mem_powerset.1 (by simpa using hX)
    ext u
    rw [Finset.mem_image]
    constructor
    · rintro ⟨p, hp, rfl⟩
      exact (mem_pre.1 hp).2
    · intro hu
      obtain ⟨p, hp⟩ := walk_surj A _ u (hSN (hX'' hu)) (Nat.lt_succ_self _)
      refine ⟨p, ?_, phi_of hp⟩
      rw [mem_pre, phi_of hp, mem_steinerPos_T A r_mem_Kbar S p]
      exact ⟨⟨u, hp, hX'' hu⟩, hu⟩
  · intro X' hX'
    have hX'' : X' ⊆ _ := Finset.mem_powerset.1 (by simpa using hX')
    have hinj : Set.InjOn (phi A.par (Kbar r K S) r) X' := by
      intro p hp q hq h
      exact phi_injOn A r_mem_Kbar S (hsub (hX'' hp)) (hsub (hX'' hq)) h
    rw [Finset.card_image_of_injOn hinj, PsiA_T A hrK hSU hX'']

end Aux

/-! ### Core -/

/-- lem:fa-dst-point, inequality. -/
theorem fa_dst_point (hrK : r ∉ K) (hSU : S ⊆ nonterm r K)
    (A : OutArb G r (Kbar r K S)) {X : Finset V} (hX : X ⊆ S) :
    gDST G r K X ≤ PsiG A X := by
  have key : ∀ C ∈ sourceComps G (Dset G r K X),
      ∃ u, (u ∈ K ∪ X ∧ A.par u ∉ Kbar r K X) ∧ u ∈ C := by
    intro C hC
    obtain ⟨⟨v, hvD, hvC⟩, -⟩ := mem_sourceComps.1 hC
    obtain ⟨u, huD, hreach, hpar⟩ := exists_top A hX _ v hvD (Nat.lt_succ_self _)
    have hu := (mem_Dset.1 huD).1
    have hur : u ≠ r := by
      rintro rfl
      exact (mem_Dset.1 huD).2 (ReachIn.of_mem r_mem_Kbar)
    refine ⟨u, ⟨?_, hpar⟩, ?_⟩
    · rw [mem_Kbar] at hu
      rw [Finset.mem_union]
      rcases hu with h | h | h
      · exact absurd h hur
      · exact Or.inl h
      · exact Or.inr h
    · have hvC' : v ∈ C := hvC ▸ scc_self hvD
      exact mem_of_mem_sourceComps hC hvC' hreach
  have : Nonempty V := ⟨r⟩
  choose! f hf using key
  have e : ∀ C ∈ sourceComps G (Dset G r K X), C = scc G (Dset G r K X) (f C) := by
    intro C hC
    obtain ⟨⟨v, _, rfl⟩, -⟩ := mem_sourceComps.1 hC
    exact (scc_eq_of_mem (hf _ hC).2).symm
  unfold gDST PsiG
  refine Finset.card_le_card_of_injOn f ?_ ?_
  · intro C hC
    have hC' : C ∈ sourceComps G (Dset G r K X) := by simpa using hC
    simp only [Finset.mem_coe, Finset.mem_filter]
    exact (hf C hC').1
  · intro C₁ h₁ C₂ h₂ he
    rw [e C₁ (Finset.mem_coe.1 h₁), e C₂ (Finset.mem_coe.1 h₂), he]

/-- eq:fa-dst-W. -/
theorem fa_dst_W (hrK : r ∉ K) (hSU : S ⊆ nonterm r K)
    (A : OutArb G r (Kbar r K S)) {y : ℝ} (hy : 0 ≤ y) :
    WAg A y ≤ WS G r K S y := by
  unfold WAg WS
  refine Finset.sum_le_sum (fun X hX => ?_)
  have hXS : X ⊆ S := Finset.mem_powerset.1 hX
  exact mul_le_mul_of_nonneg_left
    (pow_le_pow_of_le_one (by norm_num) (by norm_num) (fa_dst_point hrK hSU A hXS))
    (pow_nonneg hy _)

/-! ### Optional -/

/-- lem:fa-dst-point, equality clause: if `G[\bar K_X] = A[\bar K_X]`, then `g(X) = Ψ_A(X)`. -/
theorem fa_dst_point_eq (hrK : r ∉ K) (hSU : S ⊆ nonterm r K)
    (A : OutArb G r (Kbar r K S)) {X : Finset V} (hX : X ⊆ S)
    (hGA : ∀ a ∈ Kbar r K X, ∀ b ∈ Kbar r K X, G.Adj a b ↔ (b ≠ r ∧ A.par b = a)) :
    gDST G r K X = PsiG A X := by
  refine le_antisymm (fa_dst_point hrK hSU A hX) ?_
  -- under `hGA`, a vertex whose parent is outside `\bar K_X` is reached by nothing else
  have only : ∀ (T : Finset V), T ⊆ Kbar r K X → ∀ u ∈ Kbar r K X, A.par u ∉ Kbar r K X →
      ∀ b, ReachIn G T b u → b = u := by
    intro T hT u hu hpar b hb
    obtain ⟨-, hb⟩ := hb
    cases hb with
    | refl => rfl
    | tail _ hcu =>
      have h1 := ((hGA _ (hT hcu.1) _ hu).1 hcu.2.2).2
      exact absurd (h1 ▸ hT hcu.1) hpar
  have hDK : Dset G r K X ⊆ Kbar r K X := fun w hw => (mem_Dset.1 hw).1
  have props : ∀ u ∈ (K ∪ X).filter (fun u => A.par u ∉ Kbar r K X),
      u ∈ Kbar r K X ∧ A.par u ∉ Kbar r K X ∧ u ∈ Dset G r K X := by
    intro u hu
    rw [Finset.mem_filter, Finset.mem_union] at hu
    have hur : u ≠ r := by
      rintro rfl
      rcases hu.1 with h | h
      · exact hrK h
      · exact (mem_nonterm.1 (hSU (hX h))).1 rfl
    have huK : u ∈ Kbar r K X := by
      rw [mem_Kbar]
      tauto
    exact ⟨huK, hu.2, mem_Dset.2 ⟨huK, fun h =>
      hur (only _ (Finset.Subset.refl _) u huK hu.2 r h).symm⟩⟩
  unfold gDST PsiG
  refine Finset.card_le_card_of_injOn (scc G (Dset G r K X)) ?_ ?_
  · intro u hu
    have hu' : u ∈ (K ∪ X).filter (fun u => A.par u ∉ Kbar r K X) := by simpa using hu
    obtain ⟨huK, hpar, huD⟩ := props u hu'
    simp only [Finset.mem_coe]
    rw [mem_sourceComps]
    refine ⟨⟨u, huD, rfl⟩, fun a ha b hb hab => ?_⟩
    have hbu : b = u := only _ hDK u huK hpar b (mem_scc.1 hb).2.2
    subst hbu
    have h1 := ((hGA a (hDK ha) b huK).1 hab).2
    exact (hpar (h1 ▸ hDK ha)).elim
  · intro u₁ h₁ u₂ h₂ he
    have h₁' : u₁ ∈ (K ∪ X).filter (fun u => A.par u ∉ Kbar r K X) := by simpa using h₁
    have h₂' : u₂ ∈ (K ∪ X).filter (fun u => A.par u ∉ Kbar r K X) := by simpa using h₂
    obtain ⟨-, -, hu₁D⟩ := props u₁ h₁'
    obtain ⟨hu₂K, hpar₂, -⟩ := props u₂ h₂'
    have hmem : u₁ ∈ scc G (Dset G r K X) u₂ := he ▸ scc_self hu₁D
    exact only _ hDK u₂ hu₂K hpar₂ u₁ (mem_scc.1 hmem).2.2

/-- `WS` is `MLS.W` for the running-time exponent `g` (which ignores `k`). -/
theorem WS_eq_MLS_W (k : ℕ) (y : ℝ) :
    WS G r K S y = MLS.W (fun X _ => (gDST G r K X : ℝ)) S k y := by
  unfold WS MLS.W
  refine Finset.sum_congr rfl (fun X _ => ?_)
  rw [Real.rpow_neg (by norm_num : (0 : ℝ) ≤ 2), Real.rpow_natCast, one_div, inv_pow]

/-- An out-arborescence exists when `S` is rooted. -/
theorem exists_outArb (hroot : Rooted G r K S) : Nonempty (OutArb G r (Kbar r K S)) := by
  classical
  have hreach : ∀ v ∈ Kbar r K S, ∃ d, Aux.RW G (Kbar r K S) r d v := by
    intro v hv
    by_cases hvr : v = r
    · exact ⟨0, by simp only [Aux.RW]; exact hvr⟩
    · have hv' : v ∈ K ∪ S := by
        rw [mem_Kbar] at hv
        rw [Finset.mem_union]
        tauto
      exact Aux.exists_RW (hroot v hv')
  let dist : V → ℕ := fun v =>
    if h : ∃ d, Aux.RW G (Kbar r K S) r d v then Nat.find h else 0
  have key : ∀ v ∈ Kbar r K S, v ≠ r →
      ∃ a, a ∈ Kbar r K S ∧ G.Adj a v ∧ dist a < dist v := by
    intro v hv hvr
    have h := hreach v hv
    have hspec := Nat.find_spec h
    have hdv : dist v = Nat.find h := dite_eq_left h
    obtain ⟨d, hd⟩ : ∃ d, Nat.find h = d + 1 := by
      rcases hk : Nat.find h with _ | d
      · rw [hk] at hspec
        simp only [Aux.RW] at hspec
        exact absurd hspec hvr
      · exact ⟨d, rfl⟩
    rw [hd] at hspec
    simp only [Aux.RW] at hspec
    obtain ⟨a, ha, haN, -, hadj⟩ := hspec
    refine ⟨a, haN, hadj, ?_⟩
    have ha' : ∃ d, Aux.RW G (Kbar r K S) r d a := ⟨d, ha⟩
    have hda : dist a = Nat.find ha' := dite_eq_left ha'
    rw [hda, hdv, hd]
    exact Nat.lt_succ_of_le (Nat.find_min' ha' ha)
  have : Nonempty V := ⟨r⟩
  choose! p hp using key
  exact ⟨⟨p, dist, fun u hu hur => (hp u hu hur).1, fun u hu hur => (hp u hu hur).2.1,
    fun u hu hur => (hp u hu hur).2.2⟩⟩

/-- Minimality: no vertex of `S` is a leaf. -/
theorem noSteinerLeaf_of_minimal (hrK : r ∉ K) (hSU : S ⊆ nonterm r K)
    (hmin : ∀ T ⊆ S, Rooted G r K T → T = S) (A : OutArb G r (Kbar r K S)) :
    NoSteinerLeafG A := by
  intro v hv
  by_contra hno
  have hno' : ∀ u ∈ K ∪ S, A.par u ≠ v := fun u hu h => hno ⟨u, hu, h⟩
  have key : ∀ (n : ℕ) (w : V), w ∈ Kbar r K (S.erase v) → A.height w < n →
      ReachIn G (Kbar r K (S.erase v)) r w := by
    intro n
    induction n with
    | zero => intro w _ h; exact absurd h (Nat.not_lt_zero _)
    | succ n ih =>
      intro w hw hlt
      by_cases hwr : w = r
      · rw [hwr]
        exact ReachIn.of_mem r_mem_Kbar
      · have hwKS : w ∈ K ∪ S := by
          rw [mem_Kbar, Finset.mem_erase] at hw
          rw [Finset.mem_union]
          tauto
        have hwN : w ∈ Kbar r K S := by
          rw [mem_Kbar]
          rw [Finset.mem_union] at hwKS
          tauto
        have hpN := A.par_mem w hwN hwr
        have hpv : A.par w ≠ v := hno' w hwKS
        have hp' : A.par w ∈ Kbar r K (S.erase v) := by
          rw [mem_Kbar] at hpN ⊢
          rw [Finset.mem_erase]
          tauto
        have h1 := A.height_lt w hwN hwr
        exact (ih (A.par w) hp' (by omega)).tail_adj hw (A.par_adj w hwN hwr)
  have hroot : Rooted G r K (S.erase v) := by
    intro w hw
    refine key _ w ?_ (Nat.lt_succ_self _)
    rw [mem_Kbar]
    rw [Finset.mem_union] at hw
    tauto
  have he := hmin (S.erase v) (Finset.erase_subset _ _) hroot
  have h2 : v ∈ S.erase v := by
    rw [he]
    exact hv
  exact (Finset.mem_erase.1 h2).1 rfl

/-- The bridge to `lem:fa-dst-rec` and `lem:fa-dst-cert`: a tree with the properties that `dst_tree_bound_WA` uses. -/
theorem exists_rtree (hrK : r ∉ K) (hSU : S ⊆ nonterm r K) (A : OutArb G r (Kbar r K S)) :
    ∃ t : RTree DSTCert.Kind, DSTCert.rootKind t = .term ∧
      DSTCert.count .steiner t = S.card ∧ DSTCert.count .term t = K.card + 1 ∧
      (NoSteinerLeafG A → DSTCert.NoSteinerLeaf t) ∧
      ∀ y : ℝ, DSTCert.WA y t = WAg A y := by
  have hrS : r ∉ S := fun h => (mem_nonterm.1 (hSU h)).1 rfl
  have hSK : ∀ w ∈ S, w ∉ K := fun w hw => (mem_nonterm.1 (hSU hw)).2
  have hSN : S ⊆ Kbar r K S := fun u hu => by rw [mem_Kbar]; exact Or.inr (Or.inr hu)
  refine ⟨Aux.tree A.par (Kbar r K S) S r ((Kbar r K S).sup A.height) r, ?_, ?_, ?_, ?_, ?_⟩
  · rw [Aux.rootKind_tree]
    exact Aux.lab_eq_term.2 hrS
  · rw [Aux.count_T A r_mem_Kbar S]
    congr 1
    ext u
    rw [Finset.mem_filter, Aux.lab_eq_steiner]
    exact ⟨fun h => h.2, fun h => ⟨hSN h, h⟩⟩
  · rw [Aux.count_T A r_mem_Kbar S]
    have he : (Kbar r K S).filter (fun u => Aux.lab S u = .term) = insert r K := by
      ext u
      rw [Finset.mem_filter, Aux.lab_eq_term, Finset.mem_insert, mem_Kbar]
      constructor
      · rintro ⟨h | h | h, h'⟩
        · exact Or.inl h
        · exact Or.inr h
        · exact absurd h h'
      · rintro (h | h)
        · exact ⟨Or.inl h, h ▸ hrS⟩
        · exact ⟨Or.inr (Or.inl h), fun hs => hSK u hs h⟩
    rw [he, Finset.card_insert_of_notMem hrK]
  · intro hNL
    exact Aux.noLeaf_tree A hrK hrS hNL _ r r_mem_Kbar (Nat.le_add_left _ _)
  · intro y
    exact Aux.WA_T A hrK hSU y

/-! ### Rooted and minimal sets -/

/-- Every rooted set is a Steiner set. -/
theorem steiner_of_rooted (h : Rooted G r K S) : Steiner G r K S :=
  fun v hv => h v (Finset.mem_union_left _ hv)

/-- The reachable part of a Steiner set is a rooted subset of it. -/
theorem reachPart_rooted (hS : Steiner G r K S) :
    reachPart G r K S ⊆ S ∧ Rooted G r K (reachPart G r K S) := by
  classical
  have key : ∀ v, ReachIn G (Kbar r K S) r v →
      ReachIn G (Kbar r K (reachPart G r K S)) r v := by
    intro v h
    obtain ⟨-, h⟩ := h
    induction h with
    | refl => exact ReachIn.of_mem r_mem_Kbar
    | tail hab hbc ih =>
      refine ih.tail_adj ?_ hbc.2.2
      have hc := hbc.2.1
      rw [mem_Kbar] at hc ⊢
      rcases hc with hc | hc | hc
      · exact Or.inl hc
      · exact Or.inr (Or.inl hc)
      · refine Or.inr (Or.inr ?_)
        simp only [reachPart, Finset.mem_filter]
        exact ⟨hc, r_mem_Kbar, hab.tail hbc⟩
  refine ⟨fun v hv => (Finset.mem_filter.1 hv).1, fun v hv => ?_⟩
  rw [Finset.mem_union] at hv
  rcases hv with hv | hv
  · exact key v (hS v hv)
  · simp only [reachPart, Finset.mem_filter] at hv
    exact key v hv.2

/-- An inclusion-minimal Steiner set is rooted, and minimal among rooted sets. -/
theorem rooted_minimal_of_minimal_steiner (hS : Steiner G r K S)
    (hmin : ∀ T ⊆ S, Steiner G r K T → T = S) :
    Rooted G r K S ∧ ∀ T ⊆ S, Rooted G r K T → T = S := by
  have hR := reachPart_rooted hS
  have hRS : reachPart G r K S = S := hmin _ hR.1 (steiner_of_rooted hR.2)
  exact ⟨hRS ▸ hR.2, fun T hT hTr => hmin T hT (steiner_of_rooted hTr)⟩

/-- A minimum Steiner set is rooted and inclusion-minimal among rooted sets. -/
theorem minimum_steiner_rooted_minimal (hSU : S ⊆ nonterm r K) (hS : Steiner G r K S)
    (hleast : ∀ T ⊆ nonterm r K, Steiner G r K T → S.card ≤ T.card) :
    Rooted G r K S ∧ ∀ T ⊆ S, Rooted G r K T → T = S := by
  have hR := reachPart_rooted hS
  have hRS : reachPart G r K S = S :=
    Finset.eq_of_subset_of_card_le hR.1 (hleast _ (hR.1.trans hSU) (steiner_of_rooted hR.2))
  exact ⟨hRS ▸ hR.2, fun T hT hTr =>
    Finset.eq_of_subset_of_card_le hT (hleast T (hT.trans hSU) (steiner_of_rooted hTr))⟩

/-! ### Composites -/

/-- eq:fa-dst-W with lem:fa-dst-cert, for an inclusion-minimal rooted Steiner set. -/
theorem fa_dst_WS_cert (hrK : r ∉ K) (hSU : S ⊆ nonterm r K) (hroot : Rooted G r K S)
    (hmin : ∀ T ⊆ S, Rooted G r K T → T = S)
    {y e₁ e₂ : ℝ} {Z : Finset (ℝ × ℝ)} (hZ : Z.Nonempty) (h : DSTCert.CertHyp y e₁ e₂ Z) :
    DSTCert.cZ Z hZ * e₁ ^ S.card * e₂ ^ (K.card + 1) ≤ WS G r K S y := by
  obtain ⟨A⟩ := exists_outArb hroot
  obtain ⟨t, ht1, ht2, ht3, ht4, ht5⟩ := exists_rtree hrK hSU A
  have hl := ht4 (noSteinerLeaf_of_minimal hrK hSU hmin A)
  have hb := DSTCert.dst_tree_bound_WA y e₁ e₂ Z hZ h t ht1 hl
  rw [ht2, ht3, ht5 y] at hb
  exact hb.trans (fa_dst_W hrK hSU A h.1)

/-- The middle inequality of the proof of `thm:fa-dst`, times `(1 + y_j)^{n_U}`:
for a minimum Steiner set and each certificate `j` of prop:fa-dst-certs. The factor cancels:
the paper's denominator is `(1 + y_j)^{s + r_0}` and `n_U = s + r_0`, so the statement is
`c_{Z_j} e_{2,j} e_{1,j}^s e_{2,j}^p ≤ W_S(y_j)` with `s = |S|` and `p = |K|`. -/
theorem fa_dst_WS_minimum (hrK : r ∉ K) (hSU : S ⊆ nonterm r K) (hS : Steiner G r K S)
    (hleast : ∀ T ⊆ nonterm r K, Steiner G r K T → S.card ≤ T.card) (j : Fin 3) :
    DSTCert.cZ (DSTCert.ZR j) (DSTCert.ZR_nonempty j) * (DSTCert.e₂ j : ℝ) *
        (DSTCert.e₁ j : ℝ) ^ S.card * (DSTCert.e₂ j : ℝ) ^ K.card ≤
      WS G r K S (DSTCert.y j : ℝ) := by
  obtain ⟨hroot, hmin⟩ := minimum_steiner_rooted_minimal hSU hS hleast
  have h := fa_dst_WS_cert hrK hSU hroot hmin (DSTCert.ZR_nonempty j)
    ((DSTCert.dst_certs_exact).1 j)
  calc DSTCert.cZ (DSTCert.ZR j) (DSTCert.ZR_nonempty j) * (DSTCert.e₂ j : ℝ) *
        (DSTCert.e₁ j : ℝ) ^ S.card * (DSTCert.e₂ j : ℝ) ^ K.card
      = DSTCert.cZ (DSTCert.ZR j) (DSTCert.ZR_nonempty j) * (DSTCert.e₁ j : ℝ) ^ S.card *
          (DSTCert.e₂ j : ℝ) ^ (K.card + 1) := by ring
    _ ≤ _ := h

/-! ### Examples: seven small instances E1–E7, root `0` -/

namespace Examples

/-- The digraph on `Fin n` whose arcs are exactly the listed pairs `(a, b)`, read as `a → b`. -/
abbrev ofArcs {n : ℕ} (L : List (Fin n × Fin n)) : Digraph (Fin n) := ⟨fun a b => (a, b) ∈ L⟩

/-- E1: `r, v, k = 0, 1, 2`; arcs `r → v`, `v → k`. -/
abbrev G1 : Digraph (Fin 3) := ofArcs [(0, 1), (1, 2)]

/-- E2: E1 plus the arc `r → k`. -/
abbrev G2 : Digraph (Fin 3) := ofArcs [(0, 1), (1, 2), (0, 2)]

/-- E3: `r, v, k₁, k₂ = 0, 1, 2, 3`; arcs `r → v`, `v → k₁`, `v → k₂`, `k₁ → k₂`, `k₂ → k₁`. -/
abbrev G3 : Digraph (Fin 4) := ofArcs [(0, 1), (1, 2), (1, 3), (2, 3), (3, 2)]

/-- E4: `r, v, a, k₁, k₂ = 0, 1, 2, 3, 4`; arcs `r → v`, `v → a`, `a → k₁`, `a → k₂`, `k₁ → k₂`,
`k₂ → k₁`. -/
abbrev G4 : Digraph (Fin 5) := ofArcs [(0, 1), (1, 2), (2, 3), (2, 4), (3, 4), (4, 3)]

/-- E5: `r, v, k₁, k₂ = 0, 1, 2, 3`; arcs `r → v`, `v → k₁`, `k₁ → k₂`. -/
abbrev G5 : Digraph (Fin 4) := ofArcs [(0, 1), (1, 2), (2, 3)]

/-- E6: `r, v, k₁, k₂, k₃ = 0, 1, 2, 3, 4`; arcs `r → v`, `v → k₁`, `k₁ → k₂`, `k₁ → k₃`. -/
abbrev G6 : Digraph (Fin 5) := ofArcs [(0, 1), (1, 2), (2, 3), (2, 4)]

/-- E7: `r, v, k, u = 0, 1, 2, 3`; arcs `r → v`, `v → k`; `u` has no arcs. -/
abbrev G7 : Digraph (Fin 4) := ofArcs [(0, 1), (1, 2)]

/-- E1's arborescence: `par v = r`, `par k = v` (`par r = r` is unused). -/
def A1 : OutArb G1 0 (Kbar 0 {2} {1}) where
  par := ![0, 0, 1]
  height := ![0, 1, 2]
  par_mem := by decide
  par_adj := by decide
  height_lt := by decide

/-- An arborescence of E2 with a Steiner leaf: `par v = par k = r` (it uses the arc `r → k`). -/
def A2 : OutArb G2 0 (Kbar 0 {2} {1}) where
  par := ![0, 0, 0]
  height := ![0, 1, 1]
  par_mem := by decide
  par_adj := by decide
  height_lt := by decide

/-- E3's arborescence: `par v = r`, `par k₁ = par k₂ = v`. -/
def A3 : OutArb G3 0 (Kbar 0 {2, 3} {1}) where
  par := ![0, 0, 1, 1]
  height := ![0, 1, 2, 2]
  par_mem := by decide
  par_adj := by decide
  height_lt := by decide

/-- E4's arborescence: `par v = r`, `par a = v`, `par k₁ = par k₂ = a`. -/
def A4 : OutArb G4 0 (Kbar 0 {3, 4} {1, 2}) where
  par := ![0, 0, 1, 2, 2]
  height := ![0, 1, 2, 3, 3]
  par_mem := by decide
  par_adj := by decide
  height_lt := by decide

theorem ex1_psi : PsiG A1 ∅ = 1 ∧ PsiG A1 {1} = 0 := ⟨by decide, by decide⟩

/-- The hypothesis `hGA` of `fa_dst_point_eq` for E1, at `X = ∅` and at `X = {1}`. -/
theorem ex1_hGA :
    (∀ a ∈ Kbar (0 : Fin 3) {2} ∅, ∀ b ∈ Kbar (0 : Fin 3) {2} ∅,
      G1.Adj a b ↔ (b ≠ 0 ∧ A1.par b = a)) ∧
    (∀ a ∈ Kbar (0 : Fin 3) {2} {1}, ∀ b ∈ Kbar (0 : Fin 3) {2} {1},
      G1.Adj a b ↔ (b ≠ 0 ∧ A1.par b = a)) := by
  exact ⟨by simp only [G1, ofArcs]; decide, by simp only [G1, ofArcs]; decide⟩

theorem ex1_g : gDST G1 0 {2} ∅ = 1 ∧ gDST G1 0 {2} {1} = 0 := by
  have h0 : (0 : Fin 3) ∉ ({2} : Finset (Fin 3)) := by decide
  have hS : ({1} : Finset (Fin 3)) ⊆ nonterm (0 : Fin 3) {2} := by decide
  refine ⟨?_, ?_⟩
  · rw [fa_dst_point_eq h0 hS A1 (Finset.empty_subset _) ex1_hGA.1]
    exact ex1_psi.1
  · rw [fa_dst_point_eq h0 hS A1 (Finset.Subset.refl _) ex1_hGA.2]
    exact ex1_psi.2

/-- In E1, `k` is not reachable from `r` inside `{r, k}`. -/
theorem ex1_not_steiner_empty : ¬ Steiner G1 0 {2} ∅ := by
  intro h
  have h2 := (h 2 (by decide)).mem_of_closed (Z := {0}) (by decide) (by decide)
  exact absurd h2 (by decide)

theorem ex1_minimum : Steiner G1 0 {2} {1} ∧
    ∀ T ⊆ nonterm (0 : Fin 3) {2}, Steiner G1 0 {2} T → ({1} : Finset (Fin 3)).card ≤ T.card := by
  refine ⟨?_, ?_⟩
  · intro v hv
    rw [Finset.mem_singleton] at hv
    subst hv
    have h1 : ReachIn G1 (Kbar 0 {2} {1}) 0 1 :=
      (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)
    exact h1.tail_adj (by decide) (by decide)
  · intro T _ hT
    rw [Finset.card_singleton]
    rcases Nat.eq_zero_or_pos T.card with h | h
    · rw [Finset.card_eq_zero] at h
      subst h
      exact absurd hT ex1_not_steiner_empty
    · exact h

/-- For E1: `hrK`, `hSU`, `hroot` and `hmin`, the hypotheses of `fa_dst_WS_cert` other than the
certificate (which `DSTCert.ZR_nonempty 0` and `(DSTCert.dst_certs_exact).1 0` supply). -/
theorem ex1_hyps : (0 : Fin 3) ∉ ({2} : Finset (Fin 3)) ∧
    ({1} : Finset (Fin 3)) ⊆ nonterm (0 : Fin 3) {2} ∧ Rooted G1 0 {2} {1} ∧
    ∀ T ⊆ ({1} : Finset (Fin 3)), Rooted G1 0 {2} T → T = {1} := by
  refine ⟨by decide, by decide, ?_, ?_⟩
  · intro v hv
    have h1 : ReachIn G1 (Kbar 0 {2} {1}) 0 1 :=
      (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)
    have hv' : v = 2 ∨ v = 1 := by simpa using hv
    rcases hv' with rfl | rfl
    · exact h1.tail_adj (by decide) (by decide)
    · exact h1
  · intro T hT hroot
    rcases Finset.subset_singleton_iff.1 hT with rfl | rfl
    · exact absurd (steiner_of_rooted hroot) ex1_not_steiner_empty
    · rfl

theorem ex1_WS : ∀ y : ℝ, WS G1 0 {2} {1} y = y + 1 / 2 ∧ WAg A1 y = y + 1 / 2 := by
  intro y
  have hP : ({1} : Finset (Fin 3)).powerset = {∅, {1}} := by decide
  have hne : (∅ : Finset (Fin 3)) ≠ {1} := by decide
  constructor
  · rw [WS, hP, Finset.sum_pair hne, ex1_g.1, ex1_g.2]
    simp only [Finset.card_empty, Finset.card_singleton, pow_zero, pow_one, one_mul, mul_one]
    ring
  · rw [WAg, hP, Finset.sum_pair hne, ex1_psi.1, ex1_psi.2]
    simp only [Finset.card_empty, Finset.card_singleton, pow_zero, pow_one, one_mul, mul_one]
    ring

/-- The conclusion of `fa_dst_WS_cert` for E1 and certificate `0`. -/
theorem ex1_WS_cert :
    DSTCert.cZ (DSTCert.ZR 0) (DSTCert.ZR_nonempty 0) *
        (DSTCert.e₁ 0 : ℝ) ^ ({1} : Finset (Fin 3)).card *
        (DSTCert.e₂ 0 : ℝ) ^ (({2} : Finset (Fin 3)).card + 1) ≤
      WS G1 0 {2} {1} (DSTCert.y 0 : ℝ) :=
  fa_dst_WS_cert ex1_hyps.1 ex1_hyps.2.1 ex1_hyps.2.2.1 ex1_hyps.2.2.2
    (DSTCert.ZR_nonempty 0) ((DSTCert.dst_certs_exact).1 0)

/-- The conclusion of `fa_dst_WS_minimum` for E1 and `j = 0`. -/
theorem ex1_WS_minimum :
    DSTCert.cZ (DSTCert.ZR 0) (DSTCert.ZR_nonempty 0) * (DSTCert.e₂ 0 : ℝ) *
        (DSTCert.e₁ 0 : ℝ) ^ ({1} : Finset (Fin 3)).card *
        (DSTCert.e₂ 0 : ℝ) ^ ({2} : Finset (Fin 3)).card ≤
      WS G1 0 {2} {1} (DSTCert.y 0 : ℝ) :=
  fa_dst_WS_minimum ex1_hyps.1 ex1_hyps.2.1 ex1_minimum.1 ex1_minimum.2 0

theorem ex2_g : gDST G2 0 {2} ∅ = 0 := by
  apply gDST_eq_zero_of
  intro v hv
  have hv' : v = 0 ∨ v = 2 := by revert v; decide
  rcases hv' with rfl | rfl
  · exact ReachIn.of_mem (by decide)
  · exact (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)

/-- E2: `∅` is rooted, so `{1}` is not minimal among rooted sets, and `A2` has a Steiner leaf. -/
theorem ex2_leaf : Rooted G2 0 {2} ∅ ∧ ¬ NoSteinerLeafG A2 := by
  refine ⟨?_, ?_⟩
  · intro v hv
    have hv' : v = 2 := by simpa using hv
    subst hv'
    exact (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)
  · unfold NoSteinerLeafG
    decide

theorem ex3_g : gDST G3 0 {2, 3} ∅ = 1 := by
  have hD : Dset G3 0 {2, 3} ∅ = {2, 3} := by
    refine (Dset_eq_of (R := {0}) (by decide) ?_ (by decide)).trans (by decide)
    intro v hv
    rw [Finset.mem_singleton.1 hv]
    exact ReachIn.of_mem (by decide)
  rw [gDST, hD, sourceComps_eq_single (G := G3) (D := {2, 3}) ⟨2, by decide⟩
    (strong_of_adj (by decide)), Finset.card_singleton]

theorem ex3_psi : PsiG A3 ∅ = 2 := by decide

/-- E4 meets `hrK` and `hSU` (and `A4` is an arborescence), but `W_S(-2) < W_A(-2)`. -/
theorem ex4_strict : (0 : Fin 5) ∉ ({3, 4} : Finset (Fin 5)) ∧
    ({1, 2} : Finset (Fin 5)) ⊆ nonterm (0 : Fin 5) {3, 4} ∧
    WS G4 0 {3, 4} {1, 2} (-2) < WAg A4 (-2) := by
  refine ⟨by decide, by decide, ?_⟩
  have g0 : gDST G4 0 {3, 4} ∅ = 1 := by
    have hD : Dset G4 0 {3, 4} ∅ = {3, 4} := by
      refine (Dset_eq_of (R := {0}) (by decide) ?_ (by decide)).trans (by decide)
      intro v hv
      rw [Finset.mem_singleton.1 hv]
      exact ReachIn.of_mem (by decide)
    rw [gDST, hD, sourceComps_eq_single (G := G4) (D := {3, 4}) ⟨3, by decide⟩
      (strong_of_adj (by decide)), Finset.card_singleton]
  have g1 : gDST G4 0 {3, 4} {1} = 1 := by
    have hD : Dset G4 0 {3, 4} {1} = {3, 4} := by
      refine (Dset_eq_of (R := {0, 1}) (by decide) ?_ (by decide)).trans (by decide)
      intro v hv
      have hv' : v = 0 ∨ v = 1 := by simpa using hv
      rcases hv' with rfl | rfl
      · exact ReachIn.of_mem (by decide)
      · exact (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)
    rw [gDST, hD, sourceComps_eq_single (G := G4) (D := {3, 4}) ⟨3, by decide⟩
      (strong_of_adj (by decide)), Finset.card_singleton]
  have g2 : gDST G4 0 {3, 4} {2} ≤ 1 := by
    have h := fa_dst_point (X := {2}) (by decide) (by decide) A4 (by decide)
    have hp : PsiG A4 {2} = 1 := by decide
    omega
  have g3 : gDST G4 0 {3, 4} {1, 2} = 0 := by
    apply gDST_eq_zero_of
    intro v hv
    have h1 : ReachIn G4 (Kbar 0 {3, 4} {1, 2}) 0 1 :=
      (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)
    have h2 : ReachIn G4 (Kbar 0 {3, 4} {1, 2}) 0 2 := h1.tail_adj (by decide) (by decide)
    have hv' : v = 0 ∨ v = 1 ∨ v = 2 ∨ v = 3 ∨ v = 4 := by revert v; decide
    rcases hv' with rfl | rfl | rfl | rfl | rfl
    · exact ReachIn.of_mem (by decide)
    · exact h1
    · exact h2
    · exact h2.tail_adj (by decide) (by decide)
    · exact h2.tail_adj (by decide) (by decide)
  have p0 : PsiG A4 ∅ = 2 := by decide
  have p1 : PsiG A4 {1} = 2 := by decide
  have p2 : PsiG A4 {2} = 1 := by decide
  have p3 : PsiG A4 {1, 2} = 0 := by decide
  have c12 : ({1, 2} : Finset (Fin 5)).card = 2 := by decide
  have hP : ({1, 2} : Finset (Fin 5)).powerset = {∅, {1}, {2}, {1, 2}} := by decide
  have s1 : ∀ f : Finset (Fin 5) → ℝ,
      ∑ X ∈ ({1, 2} : Finset (Fin 5)).powerset, f X = f ∅ + f {1} + f {2} + f {1, 2} := by
    intro f
    rw [hP, Finset.sum_insert, Finset.sum_insert, Finset.sum_insert, Finset.sum_singleton]
    · ring
    all_goals decide
  have hg2 : (1 / 2 : ℝ) ^ 1 ≤ (1 / 2 : ℝ) ^ gDST G4 0 {3, 4} {2} :=
    pow_le_pow_of_le_one (by norm_num) (by norm_num) g2
  rw [WS, WAg, s1, s1]
  simp only [Finset.card_empty, Finset.card_singleton, c12, g0, g1, g3, p0, p1, p2, p3]
  generalize (1 / 2 : ℝ) ^ gDST G4 0 {3, 4} {2} = a at hg2 ⊢
  norm_num at hg2 ⊢
  linarith

theorem ex5_g : gDST G5 0 {2, 3} ∅ = 1 := by
  rw [fa_dst_point_eq (G := G5) (r := 0) (K := {2, 3}) (S := {1}) (X := ∅) (by decide)
    (by decide) ⟨![0, 0, 1, 2], ![0, 1, 2, 3], by decide, by decide, by decide⟩
    (Finset.empty_subset _) (by decide)]
  decide

theorem ex6_g : gDST G6 0 {2, 3, 4} ∅ = 1 := by
  rw [fa_dst_point_eq (G := G6) (r := 0) (K := {2, 3, 4}) (S := {1}) (X := ∅) (by decide)
    (by decide) ⟨![0, 0, 1, 2, 2], ![0, 1, 2, 3, 3], by decide, by decide, by decide⟩
    (Finset.empty_subset _) (by decide)]
  decide

theorem ex7_reachPart :
    reachPart G7 0 {2} {1, 3} = {1} ∧ Steiner G7 0 {2} {1, 3} ∧ ¬ Rooted G7 0 {2} {1, 3} ∧
      Rooted G7 0 {2} {1} := by
  have h1 : ReachIn G7 (Kbar 0 {2} {1, 3}) 0 1 :=
    (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)
  have h3 : ¬ ReachIn G7 (Kbar 0 {2} {1, 3}) 0 3 := fun h =>
    absurd (h.mem_of_closed (Z := {0, 1, 2}) (by decide) (by decide)) (by decide)
  refine ⟨?_, ?_, ?_, ?_⟩
  · ext v
    simp only [reachPart, Finset.mem_filter]
    constructor
    · rintro ⟨hv, hr⟩
      have hv' : v = 1 ∨ v = 3 := by simpa using hv
      rcases hv' with rfl | rfl
      · decide
      · exact absurd hr h3
    · intro hv
      rw [Finset.mem_singleton.1 hv]
      exact ⟨by decide, h1⟩
  · intro v hv
    rw [Finset.mem_singleton.1 hv]
    exact h1.tail_adj (by decide) (by decide)
  · intro h
    exact h3 (h 3 (by decide))
  · intro v hv
    have k1 : ReachIn G7 (Kbar 0 {2} {1}) 0 1 :=
      (ReachIn.of_mem (by decide)).tail_adj (by decide) (by decide)
    have hv' : v = 2 ∨ v = 1 := by simpa using hv
    rcases hv' with rfl | rfl
    · exact k1.tail_adj (by decide) (by decide)
    · exact k1

/-- `NoSteinerLeafG` on data: it holds for `A1` and `A4` (and fails for `A2`, `ex2_leaf`). -/
theorem ex_noLeaf : NoSteinerLeafG A1 ∧ NoSteinerLeafG A4 := by
  unfold NoSteinerLeafG
  decide

end Examples

end MaxLeafFormal.DSTGraph