MaxLeafFormal.SteinerDir

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

Statements of the paper formalised here: Lemma 5.3.

import Mathlib

/-!
# `lem:cv-W`, correctness

Branching walks use a non-nested binary form: `BTree.leaf v` is the walk
consisting of `v` alone, and `BTree.graft t w` hangs the walk `t` below the root of `w` as an
extra (first) child, through the arc from `w.root` to `t.root`. This is the paper's
sequence-of-pairs form `((u₁,𝒲₁),…,(u_q,𝒲_q))` read one pair at a time
(`graft 𝒲₁ (graft 𝒲₂ (… (leaf v)))`), and it follows the recurrence for `b_Y(v, L)` directly.
-/

namespace MaxLeafFormal.SteinerDir

open Finset

universe u

/-- Rooted ordered trees with vertex labels, in a binary form. -/
inductive BTree (W : Type u) : Type u
  | leaf : W → BTree W
  | graft : BTree W → BTree W → BTree W
  deriving DecidableEq

variable {W : Type u}

/-- The label of the root. -/
def BTree.root : BTree W → W
  | .leaf v => v
  | .graft _ w => w.root

/-- Every child's label is an out-neighbour of its parent's label. -/
def IsBW (A : W → W → Prop) : BTree W → Prop
  | .leaf _ => True
  | .graft t w => A w.root t.root ∧ IsBW A t ∧ IsBW A w

/-- All labels of a tree: the image of the walk. -/
def BTree.labels [DecidableEq W] : BTree W → Finset W
  | .leaf v => {v}
  | .graft t w => t.labels ∪ w.labels

/-- The length, when an arc with head `u` has length `ℓ u`. -/
def blen (ℓ : W → ℕ) : BTree W → ℕ
  | .leaf _ => 0
  | .graft t w => ℓ t.root + blen ℓ t + blen ℓ w

variable [DecidableEq W] (A : W → W → Prop)

/-- Feasible sets (sec:cv-steiner). Stated before `[Fintype W]` and `[DecidableRel A]`
enter. -/
def Feasible (r : W) (K D : Finset W) : Prop :=
  r ∉ D ∧ Disjoint K D ∧
    ∀ k ∈ K, Relation.ReflTransGen (fun u v => A u v ∧ v ∈ insert r (K ∪ D)) r k

/-- `OPT_φ(G, r, K)`, `⊤` if nothing is feasible. -/
noncomputable def optDir (φ : W → ℕ) (r : W) (K : Finset W) : ℕ∞ :=
  sInf ((fun D : Finset W => ((∑ v ∈ D, φ v : ℕ) : ℕ∞)) '' {D | Feasible A r K D})

/-- `φ'` (proof of lem:cv-W). -/
def phi' (φ : W → ℕ) (r : W) (K : Finset W) (v : W) : ℕ := if v = r ∨ v ∈ K then 0 else φ v

/-! ### Auxiliary facts about walks (not part of the fixed interface) -/

section Aux

variable {A}

theorem BTree.root_mem_labels : ∀ w : BTree W, w.root ∈ w.labels
  | .leaf v => by simp [BTree.root, BTree.labels]
  | .graft t w => by
    simp only [BTree.root, BTree.labels, mem_union]
    exact Or.inr (BTree.root_mem_labels w)

/-- Number of nodes labelled `x`. -/
def occ (x : W) : BTree W → ℕ
  | .leaf v => if v = x then 1 else 0
  | .graft t w => occ x t + occ x w

theorem mem_labels_iff (x : W) : ∀ w : BTree W, x ∈ w.labels ↔ 0 < occ x w
  | .leaf v => by
    by_cases h : v = x
    · subst h; simp [BTree.labels, occ]
    · have h' : x ≠ v := fun e => h e.symm
      simp [BTree.labels, occ, h, h']
  | .graft t w => by
    simp only [BTree.labels, occ, mem_union, mem_labels_iff x t, mem_labels_iff x w]
    omega

theorem blen_add_root [Fintype W] (ℓ : W → ℕ) : ∀ w : BTree W,
    blen ℓ w + ℓ w.root = ∑ x, occ x w * ℓ x
  | .leaf v => by simp [blen, occ, BTree.root]
  | .graft t w => by
    have h1 := blen_add_root ℓ t
    have h2 := blen_add_root ℓ w
    simp only [blen, occ, BTree.root, add_mul, sum_add_distrib]
    omega

theorem sum_labels_le_occ [Fintype W] (f : W → ℕ) (w : BTree W) :
    ∑ x ∈ w.labels, f x ≤ ∑ x, occ x w * f x :=
  calc ∑ x ∈ w.labels, f x ≤ ∑ x ∈ w.labels, occ x w * f x :=
        sum_le_sum fun x hx => Nat.le_mul_of_pos_left _ ((mem_labels_iff x w).mp hx)
    _ ≤ ∑ x, occ x w * f x :=
        sum_le_sum_of_subset_of_nonneg (subset_univ _) (fun _ _ _ => Nat.zero_le _)

theorem sum_occ_eq [Fintype W] (f : W → ℕ) (w : BTree W) (h : ∀ x, occ x w ≤ 1) :
    ∑ x, occ x w * f x = ∑ x ∈ w.labels, f x := by
  rw [← Finset.sum_subset (subset_univ w.labels) (fun x _ hx => by
      have : occ x w = 0 := by have := (mem_labels_iff x w).not.mp hx; omega
      simp [this])]
  refine sum_congr rfl fun x hx => ?_
  have h1 := (mem_labels_iff x w).mp hx
  have h2 := h x
  have : occ x w = 1 := by omega
  simp [this]

theorem rtg_mono {α : Type*} {r p : α → α → Prop} (h : ∀ a b, r a b → p a b) {a b : α}
    (hab : Relation.ReflTransGen r a b) : Relation.ReflTransGen p a b := by
  induction hab with
  | refl => exact .refl
  | tail _ hbc ih => exact ih.tail (h _ _ hbc)

theorem reach_labels : ∀ w : BTree W, IsBW A w → ∀ x ∈ w.labels,
    Relation.ReflTransGen (fun a b => A a b ∧ b ∈ w.labels) w.root x
  | .leaf v, _, x, hx => by
    simp only [BTree.labels, mem_singleton] at hx
    subst hx
    exact Relation.ReflTransGen.refl
  | .graft t w, hw, x, hx => by
    simp only [IsBW] at hw
    obtain ⟨ha, ht, hw'⟩ := hw
    simp only [BTree.labels, mem_union] at hx
    have mono : ∀ (s : BTree W) (a b : W),
        Relation.ReflTransGen (fun a b => A a b ∧ b ∈ s.labels) a b →
        s.labels ⊆ t.labels ∪ w.labels →
        Relation.ReflTransGen (fun a b => A a b ∧ b ∈ t.labels ∪ w.labels) a b :=
      fun s a b h hs => rtg_mono (fun a b hab => ⟨hab.1, hs hab.2⟩) h
    simp only [BTree.root, BTree.labels]
    rcases hx with hx | hx
    · refine Relation.ReflTransGen.head ⟨ha, ?_⟩
        (mono t _ _ (reach_labels t ht x hx) subset_union_left)
      exact mem_union_left _ (BTree.root_mem_labels t)
    · exact mono w _ _ (reach_labels w hw' x hx) subset_union_right

/-- Hang `s` below every node labelled `x`. -/
def graftAt (x : W) (s : BTree W) : BTree W → BTree W
  | .leaf v => if v = x then .graft s (.leaf v) else .leaf v
  | .graft t w => .graft (graftAt x s t) (graftAt x s w)

theorem root_graftAt (x : W) (s : BTree W) : ∀ w : BTree W, (graftAt x s w).root = w.root
  | .leaf v => by
    unfold graftAt
    split_ifs <;> rfl
  | .graft t w => by
    simp only [graftAt, BTree.root]
    exact root_graftAt x s w

theorem isBW_graftAt (x : W) (s : BTree W) (hs : IsBW A s) (hx : A x s.root) :
    ∀ w : BTree W, IsBW A w → IsBW A (graftAt x s w)
  | .leaf v, _ => by
    unfold graftAt
    split_ifs with h
    · subst h
      simp only [IsBW, BTree.root]
      exact ⟨hx, hs, trivial⟩
    · trivial
  | .graft t w, hw => by
    simp only [IsBW] at hw
    obtain ⟨ha, ht, hw'⟩ := hw
    simp only [graftAt, IsBW]
    refine ⟨?_, isBW_graftAt x s hs hx t ht, isBW_graftAt x s hs hx w hw'⟩
    rw [root_graftAt, root_graftAt]
    exact ha

theorem occ_graftAt (x : W) (s : BTree W) (y : W) : ∀ w : BTree W,
    occ y (graftAt x s w) = occ y w + occ x w * occ y s
  | .leaf v => by
    unfold graftAt
    split_ifs with h
    · subst h; simp [occ]; ring
    · simp [occ, h]
  | .graft t w => by
    simp only [graftAt, occ, occ_graftAt x s y t, occ_graftAt x s y w]
    ring

theorem extend_walk (H : Finset W) (w : BTree W) (hw : IsBW A w) (hocc : ∀ x, occ x w ≤ 1)
    (hH : w.labels ⊆ H) (k : W)
    (hk : Relation.ReflTransGen (fun u v => A u v ∧ v ∈ H) w.root k) :
    ∃ w' : BTree W, w'.root = w.root ∧ IsBW A w' ∧ (∀ x, occ x w' ≤ 1) ∧ w'.labels ⊆ H ∧
      w.labels ⊆ w'.labels ∧ k ∈ w'.labels := by
  induction hk with
  | refl => exact ⟨w, rfl, hw, hocc, hH, subset_refl _, BTree.root_mem_labels w⟩
  | @tail b k _ hbk ih =>
    obtain ⟨w1, hr1, hw1, hocc1, hH1, hsub1, hb1⟩ := ih
    by_cases hk1 : k ∈ w1.labels
    · exact ⟨w1, hr1, hw1, hocc1, hH1, hsub1, hk1⟩
    have hb1' := (mem_labels_iff b w1).mp hb1
    have hob : occ b w1 = 1 := by have := hocc1 b; omega
    have hok : occ k w1 = 0 := by have := (mem_labels_iff k w1).not.mp hk1; omega
    refine ⟨graftAt b (.leaf k) w1, ?_, ?_, ?_, ?_, ?_, ?_⟩
    · rw [root_graftAt, hr1]
    · exact isBW_graftAt b (.leaf k) trivial hbk.1 w1 hw1
    · intro y
      rw [occ_graftAt, hob, one_mul]
      by_cases hy : k = y
      · subst hy; simp [occ, hok]
      · have := hocc1 y; simp [occ, hy]; omega
    · intro y hy
      rw [mem_labels_iff, occ_graftAt, hob, one_mul] at hy
      by_cases hky : k = y
      · subst hky; exact hbk.2
      · simp only [occ, hky, if_false, add_zero] at hy
        exact hH1 ((mem_labels_iff y w1).mpr hy)
    · intro y hy
      have h1 := (mem_labels_iff y w1).mp (hsub1 hy)
      rw [mem_labels_iff, occ_graftAt]
      omega
    · rw [mem_labels_iff, occ_graftAt, hob]
      simp [occ]

theorem exists_walk_cover (H : Finset W) (r : W) (hr : r ∈ H) (R : Finset W)
    (hR : ∀ k ∈ R, Relation.ReflTransGen (fun u v => A u v ∧ v ∈ H) r k) :
    ∃ w : BTree W, w.root = r ∧ IsBW A w ∧ (∀ x, occ x w ≤ 1) ∧ w.labels ⊆ H ∧
      R ⊆ w.labels := by
  induction R using Finset.induction_on with
  | empty =>
    refine ⟨.leaf r, rfl, trivial, fun x => ?_, ?_, empty_subset _⟩
    · simp only [occ]; split_ifs <;> omega
    · simpa [BTree.labels] using hr
  | insert k R _ ih =>
    obtain ⟨w, hr', hw, hocc, hH, hRw⟩ := ih (fun k' hk' => hR k' (mem_insert_of_mem hk'))
    obtain ⟨w', hr'', hw', hocc', hH', hsub, hk⟩ :=
      extend_walk H w hw hocc hH k (hr' ▸ hR k (mem_insert_self k R))
    refine ⟨w', hr''.trans hr', hw', hocc', hH', ?_⟩
    rw [insert_subset_iff]
    exact ⟨hk, hRw.trans hsub⟩

end Aux

variable [Fintype W]

/-- `len(uv) = n φ'(v) + 1`; it depends on the head only. -/
def arcLen (φ : W → ℕ) (r : W) (K : Finset W) (v : W) : ℕ :=
  Fintype.card W * phi' φ r K v + 1

-- A walk covering K gives a feasible set, with n φ(D) ≤ length.
-- Stated before `[DecidableRel A]` enters, so it does not take that instance.

theorem feasible_of_walk (φ : W → ℕ) (r : W) (K : Finset W) (w : BTree W)
    (hr : w.root = r) (hw : IsBW A w) (hK : K ⊆ w.labels) :
    Feasible A r K (w.labels \ insert r K) ∧
      Fintype.card W * ∑ v ∈ w.labels \ insert r K, φ v ≤ blen (arcLen φ r K) w := by
  refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
  · simp
  · rw [disjoint_left]
    intro k hk hk'
    simp only [mem_sdiff, mem_insert, not_or] at hk'
    exact hk'.2.2 hk
  · intro k hk
    have h := reach_labels w hw k (hK hk)
    rw [hr] at h
    refine rtg_mono (fun a b hab => ⟨hab.1, ?_⟩) h
    have hb := hab.2
    by_cases h1 : b = r
    · subst h1; exact mem_insert_self _ _
    by_cases h2 : b ∈ K
    · exact mem_insert_of_mem (mem_union_left _ h2)
    · refine mem_insert_of_mem (mem_union_right _ ?_)
      simp [hb, h1, h2]
  · set D := w.labels \ insert r K with hD
    have key := blen_add_root (arcLen φ r K) w
    have h1 := sum_labels_le_occ (arcLen φ r K) w
    have hsub : insert r D ⊆ w.labels := by
      rw [insert_subset_iff]
      exact ⟨hr ▸ BTree.root_mem_labels w, sdiff_subset⟩
    have h2 := sum_le_sum_of_subset_of_nonneg hsub (f := arcLen φ r K)
      (fun _ _ _ => Nat.zero_le _)
    have hrD : r ∉ D := by simp [hD]
    rw [sum_insert hrD] at h2
    have h3 : Fintype.card W * ∑ v ∈ D, φ v ≤ ∑ v ∈ D, arcLen φ r K v := by
      rw [mul_sum]
      refine sum_le_sum fun v hv => ?_
      have hv' : ¬ (v = r ∨ v ∈ K) := by
        simp only [hD, mem_sdiff, mem_insert] at hv
        exact hv.2
      simp [arcLen, phi', hv']
    rw [hr] at key
    omega

-- A feasible set gives a walk covering K of length ≤ n φ(D) + n − 1

theorem walk_of_feasible (φ : W → ℕ) (r : W) (K D : Finset W) (hD : Feasible A r K D) :
    ∃ w : BTree W, w.root = r ∧ IsBW A w ∧ K ⊆ w.labels ∧
      blen (arcLen φ r K) w ≤ Fintype.card W * ∑ v ∈ D, φ v + (Fintype.card W - 1) := by
  obtain ⟨_, _, hreach⟩ := hD
  obtain ⟨w, hr, hw, hocc, hH, hK⟩ :=
    exists_walk_cover (A := A) (insert r (K ∪ D)) r (mem_insert_self _ _) K hreach
  refine ⟨w, hr, hw, hK, ?_⟩
  have key := blen_add_root (arcLen φ r K) w
  rw [sum_occ_eq _ w hocc, hr] at key
  have hr1 : arcLen φ r K r = 1 := by simp [arcLen, phi']
  have hsplit : ∑ x ∈ w.labels, arcLen φ r K x =
      Fintype.card W * ∑ x ∈ w.labels, phi' φ r K x + w.labels.card := by
    simp [arcLen, sum_add_distrib, mul_sum]
  have hphi : ∑ x ∈ w.labels, phi' φ r K x ≤ ∑ v ∈ D, φ v := by
    calc ∑ x ∈ w.labels, phi' φ r K x
        = ∑ x ∈ w.labels.filter (fun x => ¬ (x = r ∨ x ∈ K)), φ x := by
          rw [sum_filter]
          refine sum_congr rfl fun x _ => ?_
          unfold phi'
          split_ifs <;> simp_all
      _ ≤ ∑ v ∈ D, φ v := by
          refine sum_le_sum_of_subset_of_nonneg (fun x hx => ?_) (fun _ _ _ => Nat.zero_le _)
          simp only [mem_filter, not_or] at hx
          have := hH hx.1
          simp only [mem_insert, mem_union] at this
          rcases this with h | h | h
          · exact absurd h hx.2.1
          · exact absurd h hx.2.2
          · exact h
  have hcard : w.labels.card ≤ Fintype.card W := card_le_univ _
  have hpos : 1 ≤ w.labels.card := card_pos.mpr ⟨_, BTree.root_mem_labels w⟩
  have := Nat.mul_le_mul_left (Fintype.card W) hphi
  omega

variable [DecidableRel A]

/-- `b_Y(v, L)` for arc lengths `c u + 1`. Any definition is allowed that satisfies
`bw_mem`, `bw_zero`, `bw_pos`; one possibility: -/
def bw (c : W → ℕ) (Y : Finset W) (L : ℕ) (v : W) : ℕ :=
  if v ∈ Y then 0 else if hL : L = 0 then 1 else
    ∑ u ∈ univ.filter (fun u => A v u ∧ u ∉ Y),
      ∑ L₁ ∈ range (L + 1),
        if h : c u + 1 + L₁ ≤ L then bw c Y L₁ u * bw c Y (L - (c u + 1) - L₁) v else 0
termination_by L
decreasing_by all_goals omega

theorem bw_mem (c : W → ℕ) (Y : Finset W) (L : ℕ) (v : W) (hv : v ∈ Y) :
    bw A c Y L v = 0 := by
  rw [bw, if_pos hv]

theorem bw_zero (c : W → ℕ) (Y : Finset W) (v : W) (hv : v ∉ Y) :
    bw A c Y 0 v = 1 := by
  rw [bw, if_neg hv, dif_pos rfl]

theorem bw_pos (c : W → ℕ) (Y : Finset W) (L : ℕ) (v : W) (hv : v ∉ Y) (hL : 1 ≤ L) :
    bw A c Y L v =
      ∑ u ∈ univ.filter (fun u => A v u ∧ u ∉ Y),
        ∑ L₁ ∈ range (L + 1 - (c u + 1)),
          bw A c Y L₁ u * bw A c Y (L - (c u + 1) - L₁) v := by
  rw [bw, if_neg hv, dif_neg (by omega)]
  refine sum_congr rfl fun u _ => ?_
  simp only [dite_eq_ite]
  rw [← sum_filter]
  congr 1
  ext L₁
  simp only [mem_filter, mem_range]
  omega

/-- `b(L)`. -/
def bIE (c : W → ℕ) (K : Finset W) (r : W) (L : ℕ) : ℤ :=
  ∑ Y ∈ K.powerset, (-1 : ℤ) ^ Y.card * (bw A c Y L r : ℤ)

/-- `L_max = n² φ_max + n − 1`. -/
def Lmax (φ : W → ℕ) : ℕ := Fintype.card W ^ 2 * univ.sup φ + Fintype.card W - 1

/-- The procedure of the proof of lem:cv-W. -/
def steinerAlg (φ : W → ℕ) (r : W) (K : Finset W) : ℕ∞ :=
  if K = ∅ then 0 else
    let c := fun v => Fintype.card W * phi' φ r K v
    let Ls := (range (Lmax φ + 1)).filter (fun L => bIE A c K r L ≠ 0)
    if h : Ls.Nonempty then ((Ls.min' h / Fintype.card W : ℕ) : ℕ∞) else ⊤

/-! ### The finite set of walks counted by `bw` (auxiliary) -/

section Walks

/-- `graft` on pairs. -/
def graftP (p : BTree W × BTree W) : BTree W := .graft p.1 p.2

/-- The walks counted by `bw A c Y L v`, by the same recursion. -/
def walks (c : W → ℕ) (Y : Finset W) (L : ℕ) (v : W) : Finset (BTree W) :=
  if v ∈ Y then ∅ else if hL : L = 0 then {.leaf v} else
    (univ.filter (fun u => A v u ∧ u ∉ Y)).biUnion fun u =>
      (range (L + 1)).biUnion fun L₁ =>
        if h : c u + 1 + L₁ ≤ L then
          (walks c Y L₁ u ×ˢ walks c Y (L - (c u + 1) - L₁) v).image graftP
        else ∅
termination_by L
decreasing_by all_goals omega

theorem mem_walks (c : W → ℕ) (Y : Finset W) : ∀ (w : BTree W) (L : ℕ) (v : W),
    w ∈ walks A c Y L v ↔
      w.root = v ∧ IsBW A w ∧ blen (fun u => c u + 1) w = L ∧ Disjoint w.labels Y
  | .leaf x, L, v => by
    rw [walks]
    simp only [BTree.root, IsBW, blen, BTree.labels, disjoint_singleton_left, true_and]
    by_cases hv : v ∈ Y
    · rw [if_pos hv]
      simp only [notMem_empty, false_iff, not_and]
      rintro rfl _ hx
      exact hx hv
    rw [if_neg hv]
    by_cases hL : L = 0
    · subst hL
      rw [dif_pos rfl]
      simp only [mem_singleton, BTree.leaf.injEq, true_and]
      constructor
      · rintro rfl; exact ⟨rfl, hv⟩
      · exact fun h => h.1
    · rw [dif_neg hL]
      simp only [mem_biUnion, mem_filter, mem_univ, true_and, mem_range]
      constructor
      · rintro ⟨u, _, L₁, _, h⟩
        split_ifs at h
        · simp [graftP] at h
        · simp at h
      · rintro ⟨_, h, _⟩
        exact absurd h.symm hL
  | .graft t w', L, v => by
    have iht := mem_walks c Y t
    have ihw := mem_walks c Y w'
    rw [walks]
    simp only [BTree.root, IsBW, blen, BTree.labels, disjoint_union_left]
    constructor
    · intro h
      split_ifs at h with hv hL
      · simp at h
      · simp at h
      · simp only [mem_biUnion, mem_filter, mem_univ, true_and, mem_range] at h
        obtain ⟨u, ⟨hvu, huY⟩, L₁, hL₁, hmem⟩ := h
        split_ifs at hmem with hle
        · simp only [mem_image, mem_product, graftP, Prod.exists, BTree.graft.injEq] at hmem
          obtain ⟨t₀, w₀, ⟨ht₀, hw₀⟩, rfl, rfl⟩ := hmem
          rw [iht] at ht₀
          rw [ihw] at hw₀
          obtain ⟨htr, htb, htl, htd⟩ := ht₀
          obtain ⟨hwr, hwb, hwl, hwd⟩ := hw₀
          refine ⟨hwr, ⟨?_, htb, hwb⟩, ?_, htd, hwd⟩
          · rw [hwr, htr]; exact hvu
          · rw [htr]; omega
        · simp at hmem
    · rintro ⟨hr, ⟨hA, htb, hwb⟩, hl, htd, hwd⟩
      have hv : v ∉ Y := by
        rw [← hr]
        exact disjoint_left.mp hwd (BTree.root_mem_labels w')
      have htY : t.root ∉ Y := disjoint_left.mp htd (BTree.root_mem_labels t)
      rw [if_neg hv, dif_neg (by omega)]
      simp only [mem_biUnion, mem_filter, mem_univ, true_and, mem_range]
      refine ⟨t.root, ⟨hr ▸ hA, htY⟩, blen (fun u => c u + 1) t, by omega, ?_⟩
      rw [dif_pos (by omega)]
      simp only [mem_image, mem_product, graftP, Prod.exists, BTree.graft.injEq]
      refine ⟨t, w', ⟨?_, ?_⟩, rfl, rfl⟩
      · rw [iht]; exact ⟨rfl, htb, rfl, htd⟩
      · rw [ihw]; exact ⟨hr, hwb, by omega, hwd⟩

theorem card_walks (c : W → ℕ) (Y : Finset W) (L : ℕ) :
    ∀ v, (walks A c Y L v).card = bw A c Y L v := by
  induction L using Nat.strong_induction_on with
  | _ L ih =>
  intro v
  by_cases hv : v ∈ Y
  · rw [walks, bw_mem A c Y L v hv, if_pos hv]; rfl
  by_cases hL : L = 0
  · subst hL
    rw [walks, bw_zero A c Y v hv, if_neg hv, dif_pos rfl]; rfl
  rw [walks, if_neg hv, dif_neg hL, bw_pos A c Y L v hv (by omega)]
  rw [card_biUnion]
  · refine sum_congr rfl fun u _ => ?_
    rw [card_biUnion]
    · refine Eq.trans (sum_congr rfl (g := fun L₁ => if c u + 1 + L₁ ≤ L then
          bw A c Y L₁ u * bw A c Y (L - (c u + 1) - L₁) v else 0) fun L₁ _ => ?_) ?_
      · split_ifs with h
        · rw [card_image_of_injective _ (fun p q hpq => by
              simp only [graftP, BTree.graft.injEq] at hpq
              exact Prod.ext hpq.1 hpq.2), card_product, ih L₁ (by omega), ih _ (by omega)]
        · rfl
      · rw [← sum_filter]
        congr 1
        ext L₁
        simp only [mem_filter, mem_range]
        omega
    · intro L₁ _ L₂ _ hne
      simp only [Function.onFun]
      rw [disjoint_left]
      intro x hx₁ hx₂
      split_ifs at hx₁ hx₂
      · simp only [mem_image, mem_product, graftP, Prod.exists] at hx₁ hx₂
        obtain ⟨t₁, w₁, ⟨ht₁, -⟩, rfl⟩ := hx₁
        obtain ⟨t₂, w₂, ⟨ht₂, -⟩, he⟩ := hx₂
        simp only [BTree.graft.injEq] at he
        obtain ⟨rfl, rfl⟩ := he
        exact hne (((mem_walks A c Y _ _ _).mp ht₁).2.2.1.symm.trans
          ((mem_walks A c Y _ _ _).mp ht₂).2.2.1)
      all_goals simp_all
  · intro u₁ _ u₂ _ hne
    simp only [Function.onFun]
    rw [disjoint_left]
    intro x hx₁ hx₂
    simp only [mem_biUnion, mem_range] at hx₁ hx₂
    obtain ⟨L₁, -, hx₁⟩ := hx₁
    obtain ⟨L₂, -, hx₂⟩ := hx₂
    split_ifs at hx₁ hx₂
    · simp only [mem_image, mem_product, graftP, Prod.exists] at hx₁ hx₂
      obtain ⟨t₁, w₁, ⟨ht₁, -⟩, rfl⟩ := hx₁
      obtain ⟨t₂, w₂, ⟨ht₂, -⟩, he⟩ := hx₂
      simp only [BTree.graft.injEq] at he
      obtain ⟨rfl, rfl⟩ := he
      exact hne (((mem_walks A c Y _ _ _).mp ht₁).1.symm.trans
        ((mem_walks A c Y _ _ _).mp ht₂).1)
    all_goals simp_all

end Walks

-- b_Y(v, L) counts branching walks

theorem bw_count (c : W → ℕ) (Y : Finset W) (L : ℕ) (v : W) :
    {w : BTree W | w.root = v ∧ IsBW A w ∧ blen (fun u => c u + 1) w = L ∧
        Disjoint w.labels Y}.Finite ∧
    {w : BTree W | w.root = v ∧ IsBW A w ∧ blen (fun u => c u + 1) w = L ∧
        Disjoint w.labels Y}.ncard = bw A c Y L v := by
  have hset : {w : BTree W | w.root = v ∧ IsBW A w ∧ blen (fun u => c u + 1) w = L ∧
      Disjoint w.labels Y} = ↑(walks A c Y L v) := by
    ext w
    simp only [Set.mem_ofPred_eq, mem_coe]
    exact (mem_walks A c Y w L v).symm
  rw [hset]
  exact ⟨finite_toSet _, by rw [Set.ncard_coe_finset, card_walks]⟩

-- Inclusion–exclusion

theorem bIE_count (c : W → ℕ) (K : Finset W) (r : W) (L : ℕ) :
    bIE A c K r L =
      ({w : BTree W | w.root = r ∧ IsBW A w ∧ blen (fun u => c u + 1) w = L ∧
          K ⊆ w.labels}.ncard : ℤ) := by
  set W0 := walks A c ∅ L r with hW0
  have hY : ∀ Y : Finset W, walks A c Y L r = W0.filter (fun w => Disjoint w.labels Y) := by
    intro Y
    ext w
    simp only [hW0, mem_filter, mem_walks, disjoint_empty_right, and_true, and_assoc]
  have hset : {w : BTree W | w.root = r ∧ IsBW A w ∧ blen (fun u => c u + 1) w = L ∧
      K ⊆ w.labels} = ↑(W0.filter (fun w => K ⊆ w.labels)) := by
    ext w
    simp only [Set.mem_ofPred_eq, mem_coe, hW0, mem_filter, mem_walks, disjoint_empty_right,
      and_true, and_assoc]
  rw [hset, Set.ncard_coe_finset, bIE]
  simp_rw [← card_walks, hY, card_filter, Nat.cast_sum, mul_sum]
  rw [sum_comm]
  refine sum_congr rfl fun w _ => ?_
  have hfilt : K.powerset.filter (fun Y => Disjoint w.labels Y) = (K \ w.labels).powerset := by
    ext Y
    simp only [mem_filter, mem_powerset, subset_sdiff, disjoint_comm]
  calc ∑ Y ∈ K.powerset, (-1 : ℤ) ^ Y.card * ((if Disjoint w.labels Y then 1 else 0 : ℕ) : ℤ)
      = ∑ Y ∈ K.powerset.filter (fun Y => Disjoint w.labels Y), (-1 : ℤ) ^ Y.card := by
        rw [sum_filter]
        refine sum_congr rfl fun Y _ => ?_
        split_ifs <;> simp
    _ = ((if K ⊆ w.labels then 1 else 0 : ℕ) : ℤ) := by
        rw [hfilt, sum_powerset_neg_one_pow_card]
        by_cases h : K ⊆ w.labels <;> simp [h, sdiff_eq_empty_iff_subset]

/-- `bIE … L ≠ 0` iff some walk of length `L` covers `K` (auxiliary). -/
theorem bIE_ne_zero_iff (φ : W → ℕ) (r : W) (K : Finset W) (L : ℕ) :
    bIE A (fun v => Fintype.card W * phi' φ r K v) K r L ≠ 0 ↔
      ∃ w : BTree W, w.root = r ∧ IsBW A w ∧ blen (arcLen φ r K) w = L ∧ K ⊆ w.labels := by
  have hfin : {w : BTree W | w.root = r ∧ IsBW A w ∧
      blen (fun u => Fintype.card W * phi' φ r K u + 1) w = L ∧ K ⊆ w.labels}.Finite := by
    refine (bw_count A (fun v => Fintype.card W * phi' φ r K v) ∅ L r).1.subset fun w hw => ?_
    exact ⟨hw.1, hw.2.1, hw.2.2.1, disjoint_empty_right _⟩
  rw [bIE_count, Nat.cast_ne_zero, ← Nat.pos_iff_ne_zero, Set.ncard_pos hfin]
  rfl

/-- Every feasible set gives an accepted length `≤ Lmax` (auxiliary). -/
theorem accepted_of_feasible (φ : W → ℕ) (r : W) (K D : Finset W) (hD : Feasible A r K D) :
    ∃ L, L ≤ Lmax φ ∧ bIE A (fun v => Fintype.card W * phi' φ r K v) K r L ≠ 0 ∧
      L ≤ Fintype.card W * ∑ v ∈ D, φ v + (Fintype.card W - 1) := by
  obtain ⟨w, hr, hw, hKw, hle⟩ := walk_of_feasible A φ r K D hD
  refine ⟨blen (arcLen φ r K) w, ?_, (bIE_ne_zero_iff A φ r K _).mpr ⟨w, hr, hw, rfl, hKw⟩, hle⟩
  have hsum : ∑ v ∈ D, φ v ≤ Fintype.card W * univ.sup φ := by
    calc ∑ v ∈ D, φ v ≤ D.card • univ.sup φ :=
          sum_le_card_nsmul _ _ _ fun v _ => le_sup (mem_univ v)
      _ ≤ Fintype.card W * univ.sup φ := by
          rw [smul_eq_mul]; exact Nat.mul_le_mul_right _ (card_le_univ D)
  have h2 := Nat.mul_le_mul_left (Fintype.card W) hsum
  have hn1 : 1 ≤ Fintype.card W := Fintype.card_pos_iff.mpr ⟨r⟩
  calc blen (arcLen φ r K) w ≤ Fintype.card W * ∑ v ∈ D, φ v + (Fintype.card W - 1) := hle
    _ ≤ Fintype.card W * (Fintype.card W * univ.sup φ) + (Fintype.card W - 1) :=
        Nat.add_le_add_right h2 _
    _ = Lmax φ := by rw [Lmax, Nat.add_sub_assoc hn1, pow_two, mul_assoc]

-- lem:cv-W, correctness

theorem steinerAlg_eq (φ : W → ℕ) (r : W) (K : Finset W) :
    steinerAlg A φ r K = optDir A φ r K := by
  have hn : 0 < Fintype.card W := Fintype.card_pos_iff.mpr ⟨r⟩
  rw [steinerAlg]
  by_cases hK : K = ∅
  · rw [if_pos hK]
    subst hK
    symm
    refine le_antisymm (sInf_le ⟨∅, ⟨notMem_empty r, disjoint_empty_left _,
      fun k hk => absurd hk (notMem_empty k)⟩, by simp⟩) zero_le
  rw [if_neg hK]
  set Ls := (range (Lmax φ + 1)).filter
    (fun L => bIE A (fun v => Fintype.card W * phi' φ r K v) K r L ≠ 0) with hLs
  show (if h : Ls.Nonempty then ((Ls.min' h / Fintype.card W : ℕ) : ℕ∞) else ⊤) = optDir A φ r K
  have hmemLs : ∀ D, Feasible A r K D → ∃ L ∈ Ls,
      L ≤ Fintype.card W * ∑ v ∈ D, φ v + (Fintype.card W - 1) := by
    intro D hD
    obtain ⟨L, hL1, hL2, hL3⟩ := accepted_of_feasible A φ r K D hD
    refine ⟨L, ?_, hL3⟩
    rw [hLs, mem_filter, mem_range]
    exact ⟨by omega, hL2⟩
  by_cases hne : Ls.Nonempty
  · rw [dif_pos hne]
    have hmin : Ls.min' hne ∈ Ls := min'_mem Ls hne
    obtain ⟨-, hbie⟩ := mem_filter.mp hmin
    rw [bIE_ne_zero_iff] at hbie
    obtain ⟨w, hr, hw, hlw, hKw⟩ := hbie
    unfold optDir
    obtain ⟨hD, hle⟩ := feasible_of_walk A φ r K w hr hw hKw
    apply le_antisymm
    · refine le_sInf ?_
      rintro _ ⟨D, hD', rfl⟩
      obtain ⟨L, hL, hLD⟩ := hmemLs D hD'
      have h1 := min'_le Ls L hL
      rw [Nat.cast_le]
      apply Nat.le_of_lt_succ
      rw [Nat.div_lt_iff_lt_mul hn]
      have h2 : Fintype.card W * ∑ v ∈ D, φ v + (Fintype.card W - 1) <
          (∑ v ∈ D, φ v).succ * Fintype.card W := by
        rw [Nat.succ_mul, mul_comm]; omega
      omega
    · have h1 : sInf ((fun D : Finset W => ((∑ v ∈ D, φ v : ℕ) : ℕ∞)) '' {D | Feasible A r K D})
          ≤ ((∑ v ∈ w.labels \ insert r K, φ v : ℕ) : ℕ∞) := sInf_le ⟨_, hD, rfl⟩
      refine h1.trans ?_
      rw [Nat.cast_le, Nat.le_div_iff_mul_le hn, mul_comm]
      rw [hlw] at hle
      exact hle
  · rw [dif_neg hne]
    symm
    rw [optDir, sInf_eq_top]
    rintro _ ⟨D, hD, rfl⟩
    obtain ⟨L, hL, -⟩ := hmemLs D hD
    exact absurd (⟨L, hL⟩ : Ls.Nonempty) hne

end MaxLeafFormal.SteinerDir