import Mathlib
open Finset

/-!
Shared, PROVEN building blocks for IMO 2005 P6.
Compile read-only:  ./lc.sh Common.lean   (Lean 4.27.0 + prebuilt Mathlib v4.27).
`maxHeartbeats` is PER-DECLARATION — keep each heavy lemma its own `theorem`.
Gotchas: don't `rw` on a `Finset.filter` equality (whnf hang); keep the
`simp only [card_filter]; sum_comm` shape. `Nat.mul_sub_one : n*n-n = n*(n-1)`.
-/

namespace IMO2005P6

variable {C : Type*} [Fintype C] [DecidableEq C]

/-- # problems contestant `c` solved. -/
abbrev solvedCount (solved : C → Fin 6 → Prop) [DecidableRel solved] (c : C) : ℕ :=
  (univ.filter (fun p => solved c p)).card

/-- # contestants who solved exactly `k` problems. -/
abbrev numSolvedExactly (solved : C → Fin 6 → Prop) [DecidableRel solved] (k : ℕ) : ℕ :=
  (univ.filter (fun c => solvedCount solved c = k)).card

/-- Ordered-pair incidence count. -/
abbrev Ninc (solved : C → Fin 6 → Prop) [DecidableRel solved] : ℕ :=
  ∑ ij ∈ (univ : Finset (Fin 6)).offDiag,
    (univ.filter (fun c => solved c ij.1 ∧ solved c ij.2)).card

/-- Double count over contestants: `N = ∑_c k_c (k_c − 1)`. -/
theorem pairs_double_count
    (solved : C → Fin 6 → Prop) [DecidableRel solved] :
    Ninc solved = ∑ c : C, solvedCount solved c * (solvedCount solved c - 1) := by
  unfold Ninc solvedCount
  simp only [Finset.card_filter]
  rw [Finset.sum_comm]
  apply Finset.sum_congr rfl
  intro c _
  rw [← Finset.card_filter]
  have hset : ((univ : Finset (Fin 6)).offDiag.filter
            (fun ij => solved c ij.1 ∧ solved c ij.2))
          = (univ.filter (fun p => solved c p)).offDiag := by
    ext ij
    simp only [Finset.mem_filter, Finset.mem_offDiag, Finset.mem_univ, true_and]
    tauto
  rw [hset, Finset.offDiag_card]
  simp only [Finset.card_filter, Nat.mul_sub_one]

/-- Each contestant solved `< 7` problems (used to bound the partition range). -/
theorem solvedCount_lt_seven (solved : C → Fin 6 → Prop) [DecidableRel solved] (c : C) :
    solvedCount solved c < 7 := by
  have := Finset.card_filter_le (univ : Finset (Fin 6)) (fun p => solved c p)
  simp only [Finset.card_univ, Fintype.card_fin] at this
  unfold solvedCount; omega

/-- Partition contestants by solve-count: `∑_{k<7} a_k = |C|`. -/
theorem sum_numSolvedExactly (solved : C → Fin 6 → Prop) [DecidableRel solved] :
    ∑ k ∈ Finset.range 7, numSolvedExactly solved k = Fintype.card C := by
  unfold numSolvedExactly
  rw [← Finset.card_univ]
  rw [Finset.card_eq_sum_card_fiberwise
        (f := fun c => solvedCount solved c) (t := Finset.range 7)]
  intro c _
  simp only [Finset.coe_range, Set.mem_Iio]
  exact solvedCount_lt_seven solved c

/-- Fiber-regroup for the quadratic weight: `∑_c k_c(k_c−1) = ∑_{k<7} a_k·k(k−1)`. -/
theorem sum_quadratic_fiberwise
    (solved : C → Fin 6 → Prop) [DecidableRel solved] :
    ∑ c : C, solvedCount solved c * (solvedCount solved c - 1)
    = ∑ k ∈ Finset.range 7, numSolvedExactly solved k * (k * (k - 1)) := by
  set kc := fun c => solvedCount solved c with hkc
  have hk : ∀ c, kc c < 7 := solvedCount_lt_seven solved
  unfold numSolvedExactly
  rw [Finset.sum_comp (fun k => k * (k-1)) kc]
  have hsub : image kc univ ⊆ Finset.range 7 := by
    intro b hb; rw [Finset.mem_image] at hb
    obtain ⟨c, _, rfl⟩ := hb; rw [Finset.mem_range]; exact hk c
  rw [← Finset.sum_subset hsub]
  · apply Finset.sum_congr rfl; intro k _; rw [smul_eq_mul]
  · intro k _ hknot
    have : (univ.filter (fun c => kc c = k)) = ∅ := by
      rw [Finset.filter_eq_empty_iff]; intro c _ hc
      exact hknot (by rw [← hc]; exact Finset.mem_image_of_mem kc (mem_univ c))
    rw [this]; simp

/-- Nobody solved all 6 ⇒ a₆ = 0. -/
theorem numSolvedExactly_six_eq_zero
    (solved : C → Fin 6 → Prop) [DecidableRel solved]
    (hnall : ∀ c : C, ∃ p : Fin 6, ¬ solved c p) :
    numSolvedExactly solved 6 = 0 := by
  unfold numSolvedExactly
  rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
  intro c _ h6
  obtain ⟨p, hp⟩ := hnall c
  have hsub : (univ.filter (fun p => solved c p)) ⊂ univ := by
    rw [Finset.ssubset_univ_iff]
    intro he
    have : p ∈ univ.filter (fun p => solved c p) := by rw [he]; exact mem_univ p
    rw [Finset.mem_filter] at this; exact hp this.2
  have := Finset.card_lt_card hsub
  simp only [Finset.card_univ, Fintype.card_fin] at this
  unfold solvedCount at h6
  omega

/-- The N identity: `N = 2 a₂ + 6 a₃ + 12 a₄ + 20 a₅`. -/
theorem Ninc_identity
    (solved : C → Fin 6 → Prop) [DecidableRel solved]
    (hnall : ∀ c : C, ∃ p : Fin 6, ¬ solved c p) :
    Ninc solved = 2 * numSolvedExactly solved 2 + 6 * numSolvedExactly solved 3
                + 12 * numSolvedExactly solved 4 + 20 * numSolvedExactly solved 5 := by
  rw [pairs_double_count, sum_quadratic_fiberwise]
  have h6 := numSolvedExactly_six_eq_zero solved hnall
  simp only [Finset.sum_range_succ, Finset.sum_range_zero]
  rw [h6]; ring


-- ===== per-problem incidence (agent A) =====
set_option maxHeartbeats 400000 in
theorem Mp_eq_sum_over_solvers
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (p : Fin 6) :
    (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
        (univ.filter (fun c => solved c p ∧ solved c q)).card)
    = ∑ c ∈ univ.filter (fun c => solved c p),
        (univ.filter (fun q => q ≠ p ∧ solved c q)).card := by
  simp only [Finset.card_filter]
  conv_lhs => rw [Finset.sum_comm]
  conv_rhs => rw [Finset.sum_filter]
  apply Finset.sum_congr rfl
  intro c _
  by_cases hp : solved c p
  · rw [if_pos hp]
    rw [Finset.sum_filter]
    apply Finset.sum_congr rfl
    intro q _
    by_cases hq : q ≠ p <;> by_cases hs : solved c q <;> simp [hp, hq, hs]
  · rw [if_neg hp]
    simp [hp]

-- ===== champion extraction (agent B) =====
theorem champion_exists
    (solved : C → Fin 6 → Prop) [DecidableRel solved]
    (hchamp : (univ.filter (fun c => (univ.filter (fun p => solved c p)).card = 5)).card = 1) :
    ∃ w : C, (univ.filter (fun p => solved w p)).card = 5 ∧
             ∃ t : Fin 6, (∀ c : C, (univ.filter (fun p => solved c p)).card = 5 → c = w) := by
  rw [Finset.card_eq_one] at hchamp
  obtain ⟨w, hw⟩ := hchamp
  have hwmem : w ∈ univ.filter (fun c => (univ.filter (fun p => solved c p)).card = 5) := by
    rw [hw]; exact Finset.mem_singleton_self w
  rw [Finset.mem_filter] at hwmem
  have hw5 : (univ.filter (fun p => solved w p)).card = 5 := hwmem.2
  -- champion missed some problem (solved 5 of 6, so not all)
  have hmiss : ∃ t : Fin 6, ¬ solved w t := by
    by_contra h
    push_neg at h
    have hall : (univ.filter (fun p => solved w p)) = univ :=
      Finset.filter_true_of_mem (fun p _ => h p)
    have hbad : (6 : ℕ) = 5 := by
      calc (6 : ℕ) = (univ : Finset (Fin 6)).card := by simp
        _ = (univ.filter (fun p => solved w p)).card := by rw [hall]
        _ = 5 := hw5
    omega
  obtain ⟨t, _ht⟩ := hmiss
  refine ⟨w, hw5, t, ?_⟩
  intro c hc
  have hcmem : c ∈ univ.filter (fun c => (univ.filter (fun p => solved c p)).card = 5) := by
    rw [Finset.mem_filter]; exact ⟨Finset.mem_univ c, hc⟩
  rw [hw, Finset.mem_singleton] at hcmem
  exact hcmem

theorem solved_five_misses_one
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (w : C)
    (h5 : (univ.filter (fun p => solved w p)).card = 5) :
    ∃! t : Fin 6, ¬ solved w t := by
  have h := Finset.filter_card_add_filter_neg_card_eq_card
              (s := (univ : Finset (Fin 6))) (p := fun p => solved w p)
  simp only [Finset.card_univ, Fintype.card_fin] at h
  have hcard : (univ.filter (fun t => ¬ solved w t)).card = 1 := by omega
  rw [Finset.card_eq_one] at hcard
  obtain ⟨a, ha⟩ := hcard
  refine ⟨a, ?_, ?_⟩
  · have hamem : a ∈ univ.filter (fun t => ¬ solved w t) := by
      rw [ha]; exact Finset.mem_singleton_self a
    rw [Finset.mem_filter] at hamem
    exact hamem.2
  · intro y hy
    have hymem : y ∈ univ.filter (fun t => ¬ solved w t) := by
      rw [Finset.mem_filter]; exact ⟨Finset.mem_univ y, hy⟩
    rw [ha, Finset.mem_singleton] at hymem
    exact hymem



-- ===== inner count + M_p machinery =====
theorem inner_count_solved
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (c : C) (p : Fin 6)
    (hp : solved c p) :
    (univ.filter (fun q => q ≠ p ∧ solved c q)).card
      = (univ.filter (fun q => solved c q)).card - 1 := by
  have hp_mem : p ∈ univ.filter (fun q => solved c q) := by
    rw [Finset.mem_filter]; exact ⟨mem_univ p, hp⟩
  have herase : (univ.filter (fun q => solved c q)).erase p
      = univ.filter (fun q => q ≠ p ∧ solved c q) := by
    ext q
    simp only [Finset.mem_erase, Finset.mem_filter, mem_univ, true_and]
  rw [← herase, Finset.card_erase_of_mem hp_mem]

-- M_p = Σ_{q≠p} #{c: solved both} ≥ 2n+1, from hpair applied to each of the 5 pairs.
theorem Mp_lower
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n : ℕ) (hn : n = Fintype.card C)
    (hpair : ∀ i j : Fin 6, i ≠ j →
      2 * n < 5 * (univ.filter (fun c => solved c i ∧ solved c j)).card)
    (p : Fin 6) :
    2*n + 1 ≤ ∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
                (univ.filter (fun c => solved c p ∧ solved c q)).card := by
  -- 5 * M_p = Σ 5*m_{p,q} ≥ Σ (2n+1) = 5*(2n+1), so M_p ≥ 2n+1.
  have hcard5 : ((univ : Finset (Fin 6)).filter (fun q => q ≠ p)).card = 5 := by
    rw [Finset.filter_ne']
    rw [Finset.card_erase_of_mem (mem_univ p)]
    simp
  have h5 : 5 * (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
                (univ.filter (fun c => solved c p ∧ solved c q)).card)
          ≥ 5 * (2*n+1) := by
    rw [Finset.mul_sum]
    calc ∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
            5 * (univ.filter (fun c => solved c p ∧ solved c q)).card
        ≥ ∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p), (2*n+1) := by
          apply Finset.sum_le_sum
          intro q hq
          rw [Finset.mem_filter] at hq
          have := hpair p q (Ne.symm hq.2)
          omega
      _ = 5 * (2*n+1) := by rw [Finset.sum_const, hcard5, smul_eq_mul]
  omega

-- if the fiber for count k is empty, no contestant has that count
theorem no_contestant_with_count
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (k : ℕ)
    (hk : (univ.filter (fun c => (univ.filter (fun p => solved c p)).card = k)).card = 0)
    (c : C) : (univ.filter (fun p => solved c p)).card ≠ k := by
  rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff] at hk
  exact hk (mem_univ c)


-- ===== linking identity (agent C) =====
theorem N_eq_sum_Mp
    (solved : C → Fin 6 → Prop) [DecidableRel solved] :
    (∑ ij ∈ (univ : Finset (Fin 6)).offDiag,
        (univ.filter (fun c => solved c ij.1 ∧ solved c ij.2)).card)
    = ∑ p : Fin 6, ∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
        (univ.filter (fun c => solved c p ∧ solved c q)).card := by
  -- Rewrite LHS: offDiag = (univ ×ˢ univ).filter (x.1 ≠ x.2)
  have hoff : (univ : Finset (Fin 6)).offDiag
      = (univ ×ˢ univ).filter (fun x => x.1 ≠ x.2) := by
    ext x
    simp only [Finset.mem_offDiag, Finset.mem_filter, Finset.mem_product,
      Finset.mem_univ, true_and]
  rw [hoff]
  -- LHS = ∑ over univ ×ˢ univ of (if x.1 ≠ x.2 then card else 0)
  rw [Finset.sum_filter]
  rw [Finset.sum_product]
  -- Now RHS: turn inner filter into if-then-else
  refine Finset.sum_congr rfl (fun p _ => ?_)
  rw [Finset.sum_filter]
  refine Finset.sum_congr rfl (fun q _ => ?_)
  rcases eq_or_ne p q with h | h
  · subst h; simp
  · rw [if_pos h, if_pos (Ne.symm h)]

-- ===== reduced-world facts =====

theorem every_nonchampion_solved_four
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (w : C)
    (hle6 : ∀ c : C, (univ.filter (fun q => solved c q)).card < 7)
    (h0 : ∀ c : C, (univ.filter (fun q => solved c q)).card ≠ 0)
    (h1 : ∀ c : C, (univ.filter (fun q => solved c q)).card ≠ 1)
    (h2 : ∀ c : C, (univ.filter (fun q => solved c q)).card ≠ 2)
    (h3 : ∀ c : C, (univ.filter (fun q => solved c q)).card ≠ 3)
    (h6 : ∀ c : C, (univ.filter (fun q => solved c q)).card ≠ 6)
    (huniq : ∀ c : C, (univ.filter (fun q => solved c q)).card = 5 → c = w)
    (c : C) (hc : c ≠ w) :
    (univ.filter (fun q => solved c q)).card = 4 := by
  have hlt := hle6 c
  have := h0 c; have := h1 c; have := h2 c; have := h3 c; have := h6 c
  -- count ∈ {4,5}; if 5 then c=w contra
  by_cases h5 : (univ.filter (fun q => solved c q)).card = 5
  · exact absurd (huniq c h5) hc
  · omega


theorem sum_solvers_eq_sum_counts
    (solved : C → Fin 6 → Prop) [DecidableRel solved] :
    ∑ p : Fin 6, (univ.filter (fun c => solved c p)).card
    = ∑ c : C, (univ.filter (fun q => solved c q)).card := by
  simp only [Finset.card_filter]
  rw [Finset.sum_comm]


theorem sum_counts_eq
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n : ℕ) (hn : n = Fintype.card C) (w : C)
    (hw5 : (univ.filter (fun q => solved w q)).card = 5)
    (hrest : ∀ c : C, c ≠ w → (univ.filter (fun q => solved c q)).card = 4) :
    ∑ c : C, (univ.filter (fun q => solved c q)).card = 4*n + 1 := by
  rw [← Finset.add_sum_erase univ _ (mem_univ w)]
  rw [hw5]
  have hrest' : ∑ c ∈ univ.erase w, (univ.filter (fun q => solved c q)).card
              = ∑ c ∈ univ.erase w, 4 := by
    apply Finset.sum_congr rfl
    intro c hc
    rw [Finset.mem_erase] at hc
    exact hrest c hc.1
  rw [hrest', Finset.sum_const, Finset.card_erase_of_mem (mem_univ w)]
  rw [Finset.card_univ, ← hn]
  -- 5 + (n-1)•4 = 4n+1
  have : 1 ≤ n := by rw [hn]; exact Fintype.card_pos_iff.mpr ⟨w⟩
  simp only [smul_eq_mul]
  omega



-- ===== solver-sum eval (agent D) =====
theorem solver_sum_eval
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (p : Fin 6) (w : C)
    (hw5 : (univ.filter (fun q => solved w q)).card = 5)
    (hrest : ∀ c : C, c ≠ w → (univ.filter (fun q => solved c q)).card = 4) :
    (∑ c ∈ univ.filter (fun c => solved c p),
        ((univ.filter (fun q => solved c q)).card - 1))
    = 3 * (univ.filter (fun c => solved c p)).card
      + (if solved w p then 1 else 0) := by
  rw [show (∑ c ∈ univ.filter (fun c => solved c p),
        ((univ.filter (fun q => solved c q)).card - 1))
      = ∑ c ∈ univ.filter (fun c => solved c p),
        (3 + (if c = w then 1 else 0)) from ?_]
  · rw [Finset.sum_add_distrib, Finset.sum_const, smul_eq_mul, mul_comm]
    rw [Finset.sum_ite_eq']
    congr 1
    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
  · apply Finset.sum_congr rfl
    intro c hc
    rcases eq_or_ne c w with h | h
    · subst h
      rw [if_pos rfl, hw5]
    · rw [if_neg h, hrest c h]

-- ===== champion solved-iff =====
theorem champion_solved_iff
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (w : C) (t : Fin 6)
    (hw5 : (univ.filter (fun q => solved w q)).card = 5)
    (ht : ¬ solved w t) :
    ∀ p : Fin 6, solved w p ↔ p ≠ t := by
  -- the missed set has card 1 and contains t, so it IS {t}; hence ¬solved w p ↔ p = t
  have h := Finset.filter_card_add_filter_neg_card_eq_card
              (s := (univ : Finset (Fin 6))) (p := fun q => solved w q)
  simp only [Finset.card_univ, Fintype.card_fin] at h
  have hmiss : (univ.filter (fun q => ¬ solved w q)).card = 1 := by omega
  rw [Finset.card_eq_one] at hmiss
  obtain ⟨t', ht'⟩ := hmiss
  have htmem : t ∈ univ.filter (fun q => ¬ solved w q) := by
    rw [Finset.mem_filter]; exact ⟨mem_univ t, ht⟩
  rw [ht', Finset.mem_singleton] at htmem
  subst htmem
  intro p
  constructor
  · intro hp hpt; subst hpt; exact ht hp
  · intro hpt
    by_contra hnp
    have : p ∈ univ.filter (fun q => ¬ solved w q) := by
      rw [Finset.mem_filter]; exact ⟨mem_univ p, hnp⟩
    rw [ht', Finset.mem_singleton] at this
    exact hpt this

-- ===== reduction (fibers + N lower) =====
/-- Lower bound 12n+6 ≤ N from hpair (5N ≥ 30(2n+1)). -/
theorem Ninc_lower
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n : ℕ) (hn : n = Fintype.card C)
    (hpair : ∀ i j : Fin 6, i ≠ j →
      2 * n < 5 * (univ.filter (fun c => solved c i ∧ solved c j)).card) :
    12 * n + 6 ≤ Ninc solved := by
  have hcard_off : ((univ : Finset (Fin 6)).offDiag).card = 30 := by
    rw [Finset.offDiag_card, Finset.card_univ, Fintype.card_fin]
  have h5 : 30 * (2*n+1) ≤ 5 * Ninc solved := by
    unfold Ninc
    rw [Finset.mul_sum]
    calc 30 * (2*n+1)
        = ∑ _ij ∈ (univ : Finset (Fin 6)).offDiag, (2*n+1) := by
          rw [Finset.sum_const, hcard_off, smul_eq_mul]
      _ ≤ ∑ ij ∈ (univ : Finset (Fin 6)).offDiag,
            5 * (univ.filter (fun c => solved c ij.1 ∧ solved c ij.2)).card := by
          apply Finset.sum_le_sum
          intro ij hij
          rw [Finset.mem_offDiag] at hij
          have := hpair ij.1 ij.2 hij.2.2
          omega
  omega

/-- Reduction: if exactly one contestant solved 5, the fibers for 0,1,2,3 are empty. -/
theorem champion_forces_fibers
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n : ℕ) (hn : n = Fintype.card C)
    (hpair : ∀ i j : Fin 6, i ≠ j →
      2 * n < 5 * (univ.filter (fun c => solved c i ∧ solved c j)).card)
    (hnall : ∀ c : C, ∃ p : Fin 6, ¬ solved c p)
    (ha5 : numSolvedExactly solved 5 = 1) :
    numSolvedExactly solved 0 = 0 ∧ numSolvedExactly solved 1 = 0
    ∧ numSolvedExactly solved 2 = 0 ∧ numSolvedExactly solved 3 = 0 := by
  have hpart := sum_numSolvedExactly solved
  have hNid := Ninc_identity solved hnall
  have hlow := Ninc_lower solved n hn hpair
  have h6 := numSolvedExactly_six_eq_zero solved hnall
  -- expand partition sum over range 7
  simp only [Finset.sum_range_succ, Finset.sum_range_zero] at hpart
  rw [← hn] at hpart
  omega


/-- Per-problem: `M_p = 3 b_p + (if p ≠ t then 1 else 0)` in the reduced world. -/
theorem Mp_formula
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (p : Fin 6) (w : C) (t : Fin 6)
    (hw5 : (univ.filter (fun q => solved w q)).card = 5)
    (ht : ¬ solved w t)
    (hrest : ∀ c : C, c ≠ w → (univ.filter (fun q => solved c q)).card = 4) :
    (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
        (univ.filter (fun c => solved c p ∧ solved c q)).card)
    = 3 * (univ.filter (fun c => solved c p)).card + (if p ≠ t then 1 else 0) := by
  rw [Mp_eq_sum_over_solvers solved p]
  have hstep : (∑ c ∈ univ.filter (fun c => solved c p),
                (univ.filter (fun q => q ≠ p ∧ solved c q)).card)
             = ∑ c ∈ univ.filter (fun c => solved c p),
                ((univ.filter (fun q => solved c q)).card - 1) := by
    apply Finset.sum_congr rfl
    intro c hc
    rw [Finset.mem_filter] at hc
    exact inner_count_solved solved c p hc.2
  rw [hstep, solver_sum_eval solved p w hw5 hrest]
  have hiff := champion_solved_iff solved w t hw5 ht p
  by_cases hp : p = t
  · subst hp; simp [ht]
  · rw [if_pos hp]
    have : solved w p := hiff.mpr hp
    rw [if_pos this]


-- ============ SPECIAL PAIR MACHINERY ============
noncomputable def pairCount (solved : C → Fin 6 → Prop) [DecidableRel solved] (P : Finset (Fin 6)) : ℕ :=
  (univ.filter (fun c => ∀ x ∈ P, solved c x)).card

theorem pairCount_pair
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (i j : Fin 6) :
    pairCount solved {i, j} = (univ.filter (fun c => solved c i ∧ solved c j)).card := by
  unfold pairCount
  congr 1; ext c
  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.forall_mem_insert,
    Finset.mem_singleton, forall_eq]

theorem Mp_eq_pairCount_sum
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (p : Fin 6) :
    (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
        (univ.filter (fun c => solved c p ∧ solved c q)).card)
    = ∑ P ∈ ((univ : Finset (Fin 6)).powersetCard 2).filter (fun P => p ∈ P),
        pairCount solved P := by
  -- reindex RHS: the pair-set is the image of {q ≠ p} under q ↦ {p,q}
  rw [show ((univ : Finset (Fin 6)).powersetCard 2).filter (fun P => p ∈ P)
        = ((univ : Finset (Fin 6)).filter (fun q => q ≠ p)).image (fun q => {p, q}) from ?_]
  · rw [Finset.sum_image ?_]
    · apply Finset.sum_congr rfl
      intro q hq
      rw [Finset.mem_filter] at hq
      rw [pairCount_pair]
    · -- injectivity of q ↦ {p,q} on {q≠p}
      intro a ha b hb hab
      simp only [Finset.coe_filter, Finset.mem_univ, true_and, Set.mem_setOf_eq] at ha hb
      simp only [] at hab
      have : a ∈ ({p, b} : Finset (Fin 6)) := by rw [← hab]; simp
      simp only [Finset.mem_insert, Finset.mem_singleton] at this
      rcases this with h | h
      · exact absurd h ha
      · exact h
  · -- set equality: {P : 2-subset, p∈P} = image (q↦{p,q}) {q≠p}
    ext P
    simp only [Finset.mem_filter, Finset.mem_powersetCard, Finset.mem_image, Finset.subset_univ,
      true_and, Finset.mem_univ]
    constructor
    · rintro ⟨hcard, hp⟩
      -- P has card 2 and p ∈ P, so P = {p, other}
      obtain ⟨x, y, hxy, hP⟩ := Finset.card_eq_two.mp hcard
      subst hP
      simp only [Finset.mem_insert, Finset.mem_singleton] at hp
      rcases hp with h | h
      · subst h; exact ⟨y, fun he => hxy he.symm, rfl⟩
      · subst h; exact ⟨x, fun he => hxy he, by rw [Finset.pair_comm]⟩
    · rintro ⟨q, hqp, rfl⟩
      refine ⟨?_, ?_⟩
      · rw [Finset.card_eq_two]; exact ⟨p, q, fun h => hqp (h.symm), rfl⟩
      · simp

theorem sum_pairCount_eq
    (solved : C → Fin 6 → Prop) [DecidableRel solved] :
    ∑ P ∈ (univ : Finset (Fin 6)).powersetCard 2, pairCount solved P
    = ∑ c : C, ((univ.filter (fun q => solved c q)).card).choose 2 := by
  have key : ∀ c : C,
      (∑ P ∈ (univ : Finset (Fin 6)).powersetCard 2,
          if (∀ x ∈ P, solved c x) then (1 : ℕ) else 0)
        = ((univ.filter (fun q => solved c q)).card).choose 2 := by
    intro c
    rw [← Finset.card_filter]
    have hset : ((univ : Finset (Fin 6)).powersetCard 2).filter
          (fun P => ∀ x ∈ P, solved c x)
        = (univ.filter (fun q => solved c q)).powersetCard 2 := by
      ext P
      simp only [Finset.mem_filter, Finset.mem_powersetCard,
        true_and, Finset.subset_univ]
      constructor
      · rintro ⟨hcard, hall⟩
        refine ⟨fun x hx => Finset.mem_filter.mpr ⟨Finset.mem_univ x, hall x hx⟩, hcard⟩
      · rintro ⟨hsub, hcard⟩
        exact ⟨hcard, fun x hx => (Finset.mem_filter.mp (hsub hx)).2⟩
    rw [hset, Finset.card_powersetCard]
  have hexpand : (∑ P ∈ (univ : Finset (Fin 6)).powersetCard 2, pairCount solved P)
      = ∑ P ∈ (univ : Finset (Fin 6)).powersetCard 2,
          ∑ c : C, if (∀ x ∈ P, solved c x) then (1 : ℕ) else 0 := by
    apply Finset.sum_congr rfl
    intro P _
    rw [pairCount, Finset.card_filter]
  rw [hexpand, Finset.sum_comm]
  exact Finset.sum_congr rfl (fun c _ => key c)

theorem sum_choose_eq
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n : ℕ) (hn : n = Fintype.card C) (w : C)
    (hw5 : (univ.filter (fun q => solved w q)).card = 5)
    (hrest : ∀ c : C, c ≠ w → (univ.filter (fun q => solved c q)).card = 4) :
    ∑ c : C, ((univ.filter (fun q => solved c q)).card).choose 2 = 6*n + 4 := by
  rw [← Finset.add_sum_erase univ _ (mem_univ w)]
  rw [hw5]
  have hrest' : ∑ c ∈ univ.erase w, ((univ.filter (fun q => solved c q)).card).choose 2
              = ∑ c ∈ univ.erase w, 6 := by
    apply Finset.sum_congr rfl
    intro c hc
    rw [Finset.mem_erase] at hc
    rw [hrest c hc.1]  -- now Nat.choose 4 2 = 6
    rfl
  rw [hrest', Finset.sum_const, Finset.card_erase_of_mem (mem_univ w)]
  rw [Finset.card_univ, ← hn]
  have : 1 ≤ n := by rw [hn]; exact Fintype.card_pos_iff.mpr ⟨w⟩
  simp only [smul_eq_mul]
  -- Nat.choose 5 2 = 10 ; goal: 10 + (n-1)*6 = 6n+4
  norm_num [Nat.choose]
  omega

theorem pairCount_ge_B
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n B : ℕ) (hn : n = Fintype.card C)
    (hB : 5*B = 2*n+1)
    (hpair : ∀ i j : Fin 6, i ≠ j →
      2 * n < 5 * (univ.filter (fun c => solved c i ∧ solved c j)).card)
    (P : Finset (Fin 6)) (hP : P ∈ (univ : Finset (Fin 6)).powersetCard 2) :
    B ≤ pairCount solved P := by
  rw [Finset.mem_powersetCard] at hP
  obtain ⟨_, hcard⟩ := hP
  rw [Finset.card_eq_two] at hcard
  obtain ⟨i, j, hij, rfl⟩ := hcard
  rw [pairCount_pair solved i j]
  have := hpair i j hij
  omega

theorem Mp_upper_core
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n B : ℕ) (p : Fin 6)
    (hB : 5*B = 2*n+1)
    (hge : ∀ P ∈ (univ : Finset (Fin 6)).powersetCard 2, B ≤ pairCount solved P)
    (htot : ∑ P ∈ (univ : Finset (Fin 6)).powersetCard 2, pairCount solved P = 6*n+4)
    (hbridge : (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
        (univ.filter (fun c => solved c p ∧ solved c q)).card)
      = ∑ P ∈ ((univ : Finset (Fin 6)).powersetCard 2).filter (fun P => p ∈ P), pairCount solved P) :
    (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
        (univ.filter (fun c => solved c p ∧ solved c q)).card) ≤ 2*n+2 := by
  rw [hbridge]
  -- total excess over all pairs = 1
  set all15 := (univ : Finset (Fin 6)).powersetCard 2 with hall
  set T := all15.filter (fun P => p ∈ P) with hT
  have hcard15 : all15.card = 15 := by rw [hall]; decide
  have htot' : ∑ P ∈ all15, pairCount solved P = all15.card * B + 1 := by
    rw [hcard15, htot]; omega
  have hexcess : ∑ P ∈ all15, (pairCount solved P - B) = 1 := by
    have h1 : ∑ P ∈ all15, (pairCount solved P - B)
            = (∑ P ∈ all15, pairCount solved P) - ∑ P ∈ all15, B := by
      rw [← Finset.sum_tsub_distrib]; intro P hP; exact hge P hP
    rw [h1, htot', Finset.sum_const, smul_eq_mul]; omega
  have hTsub : T ⊆ all15 := Finset.filter_subset _ _
  have hTcard : T.card = 5 := by rw [hT, hall]; fin_cases p <;> decide
  have hsubex : ∑ P ∈ T, (pairCount solved P - B) ≤ ∑ P ∈ all15, (pairCount solved P - B) :=
    Finset.sum_le_sum_of_subset_of_nonneg hTsub (fun i _ _ => Nat.zero_le _)
  rw [hexcess] at hsubex
  have hsplit : ∑ P ∈ T, pairCount solved P = ∑ P ∈ T, (pairCount solved P - B) + ∑ P ∈ T, B := by
    rw [← Finset.sum_add_distrib]; apply Finset.sum_congr rfl; intro P hP
    have := hge P (hTsub hP); omega
  rw [hsplit, Finset.sum_const, hTcard, smul_eq_mul]; omega


/-- `M_p ≤ 2n+2` in the reduced world (champion w solved 5, rest solved 4, 5∣2n+1). -/
theorem Mp_upper
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n B : ℕ) (hn : n = Fintype.card C) (w : C)
    (hB : 5*B = 2*n+1)
    (hpair : ∀ i j : Fin 6, i ≠ j →
      2 * n < 5 * (univ.filter (fun c => solved c i ∧ solved c j)).card)
    (hw5 : (univ.filter (fun q => solved w q)).card = 5)
    (hrest : ∀ c : C, c ≠ w → (univ.filter (fun q => solved c q)).card = 4)
    (p : Fin 6) :
    (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ p),
        (univ.filter (fun c => solved c p ∧ solved c q)).card) ≤ 2*n+2 := by
  have htot : ∑ P ∈ (univ : Finset (Fin 6)).powersetCard 2, pairCount solved P = 6*n+4 := by
    rw [sum_pairCount_eq, sum_choose_eq solved n hn w hw5 hrest]
  have hge : ∀ P ∈ (univ : Finset (Fin 6)).powersetCard 2, B ≤ pairCount solved P :=
    fun P hP => pairCount_ge_B solved n B hn hB hpair P hP
  have hbridge := Mp_eq_pairCount_sum solved p
  exact Mp_upper_core solved n B p hB hge htot hbridge



-- ============ HARD-BRANCH ARITHMETIC ============
set_option maxHeartbeats 2000000 in
theorem five_way_hex
    (n m0 m1 m2 m3 m4 m5 : ℕ)
    (L0 : 2*n+1 ≤ m0) (L1 : 2*n+1 ≤ m1) (L2 : 2*n+1 ≤ m2)
    (L3 : 2*n+1 ≤ m3) (L4 : 2*n+1 ≤ m4) (L5 : 2*n+1 ≤ m5)
    (U0 : m0 ≤ 2*n+2) (U1 : m1 ≤ 2*n+2) (U2 : m2 ≤ 2*n+2)
    (U3 : m3 ≤ 2*n+2) (U4 : m4 ≤ 2*n+2) (U5 : m5 ≤ 2*n+2)
    (hMsum : m0+m1+m2+m3+m4+m5 = 12*n+8) :
    (m1=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1)
  ∧ (m0=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1)
  ∧ (m0=2*n+1 ∨ m1=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1)
  ∧ (m0=2*n+1 ∨ m1=2*n+1 ∨ m2=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1)
  ∧ (m0=2*n+1 ∨ m1=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m5=2*n+1)
  ∧ (m0=2*n+1 ∨ m1=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1) := by
  have c0 : m1=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1 := by omega
  have c1 : m0=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1 := by omega
  have c2 : m0=2*n+1 ∨ m1=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1 := by omega
  have c3 : m0=2*n+1 ∨ m1=2*n+1 ∨ m2=2*n+1 ∨ m4=2*n+1 ∨ m5=2*n+1 := by omega
  have c4 : m0=2*n+1 ∨ m1=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m5=2*n+1 := by omega
  have c5 : m0=2*n+1 ∨ m1=2*n+1 ∨ m2=2*n+1 ∨ m3=2*n+1 ∨ m4=2*n+1 := by omega
  exact ⟨c0,c1,c2,c3,c4,c5⟩

set_option maxHeartbeats 2000000 in
theorem hard_arith
    (n : ℕ) (t : Fin 6) (m0 m1 m2 m3 m4 m5 b0 b1 b2 b3 b4 b5 : ℕ)
    (F0 : m0 = 3*b0 + (if (0:Fin 6) ≠ t then 1 else 0))
    (F1 : m1 = 3*b1 + (if (1:Fin 6) ≠ t then 1 else 0))
    (F2 : m2 = 3*b2 + (if (2:Fin 6) ≠ t then 1 else 0))
    (F3 : m3 = 3*b3 + (if (3:Fin 6) ≠ t then 1 else 0))
    (F4 : m4 = 3*b4 + (if (4:Fin 6) ≠ t then 1 else 0))
    (F5 : m5 = 3*b5 + (if (5:Fin 6) ≠ t then 1 else 0))
    (L0 : 2*n+1 ≤ m0) (L1 : 2*n+1 ≤ m1) (L2 : 2*n+1 ≤ m2)
    (L3 : 2*n+1 ≤ m3) (L4 : 2*n+1 ≤ m4) (L5 : 2*n+1 ≤ m5)
    (U0 : m0 ≤ 2*n+2) (U1 : m1 ≤ 2*n+2) (U2 : m2 ≤ 2*n+2)
    (U3 : m3 ≤ 2*n+2) (U4 : m4 ≤ 2*n+2) (U5 : m5 ≤ 2*n+2)
    (hMsum : m0+m1+m2+m3+m4+m5 = 12*n+8) : False := by
  obtain ⟨e0,e1,e2,e3,e4,e5⟩ :=
    five_way_hex n m0 m1 m2 m3 m4 m5 L0 L1 L2 L3 L4 L5 U0 U1 U2 U3 U4 U5 hMsum
  fin_cases t
  · norm_num [Fin.ext_iff, Fin.val_ofNat] at F0 F1 F2 F3 F4 F5
    rcases e0 with h|h|h|h|h <;> omega
  · norm_num [Fin.ext_iff, Fin.val_ofNat] at F0 F1 F2 F3 F4 F5
    rcases e1 with h|h|h|h|h <;> omega
  · norm_num [Fin.ext_iff, Fin.val_ofNat] at F0 F1 F2 F3 F4 F5
    rcases e2 with h|h|h|h|h <;> omega
  · norm_num [Fin.ext_iff, Fin.val_ofNat] at F0 F1 F2 F3 F4 F5
    rcases e3 with h|h|h|h|h <;> omega
  · norm_num [Fin.ext_iff, Fin.val_ofNat] at F0 F1 F2 F3 F4 F5
    rcases e4 with h|h|h|h|h <;> omega
  · norm_num [Fin.ext_iff, Fin.val_ofNat] at F0 F1 F2 F3 F4 F5
    rcases e5 with h|h|h|h|h <;> omega

-- ============ HARD BRANCH (a5 = 1 impossible) ============
set_option maxHeartbeats 4000000 in
theorem not_exactly_one_champion
    (solved : C → Fin 6 → Prop) [DecidableRel solved] (n : ℕ) (hn : n = Fintype.card C)
    (hpair : ∀ i j : Fin 6, i ≠ j →
      2 * n < 5 * (univ.filter (fun c => solved c i ∧ solved c j)).card)
    (hnall : ∀ c : C, ∃ p : Fin 6, ¬ solved c p)
    (hdvd : 5 ∣ (2*n+1))
    (ha5 : numSolvedExactly solved 5 = 1) : False := by
  obtain ⟨B, hB⟩ := hdvd
  obtain ⟨w, hw5, _t, huniq⟩ := champion_exists solved ha5
  obtain ⟨t0, ht0, _⟩ := solved_five_misses_one solved w hw5
  obtain ⟨f0, f1, f2, f3⟩ := champion_forces_fibers solved n hn hpair hnall ha5
  have hrest : ∀ c : C, c ≠ w → (univ.filter (fun q => solved c q)).card = 4 := by
    apply every_nonchampion_solved_four solved w
    · intro c; exact solvedCount_lt_seven solved c
    · intro c; exact no_contestant_with_count solved 0 f0 c
    · intro c; exact no_contestant_with_count solved 1 f1 c
    · intro c; exact no_contestant_with_count solved 2 f2 c
    · intro c; exact no_contestant_with_count solved 3 f3 c
    · intro c; exact no_contestant_with_count solved 6 (numSolvedExactly_six_eq_zero solved hnall) c
    · intro c hc; exact huniq c hc
  have F0 := Mp_formula solved 0 w t0 hw5 ht0 hrest
  have F1 := Mp_formula solved 1 w t0 hw5 ht0 hrest
  have F2 := Mp_formula solved 2 w t0 hw5 ht0 hrest
  have F3 := Mp_formula solved 3 w t0 hw5 ht0 hrest
  have F4 := Mp_formula solved 4 w t0 hw5 ht0 hrest
  have F5 := Mp_formula solved 5 w t0 hw5 ht0 hrest
  have L0 := Mp_lower solved n hn hpair 0
  have L1 := Mp_lower solved n hn hpair 1
  have L2 := Mp_lower solved n hn hpair 2
  have L3 := Mp_lower solved n hn hpair 3
  have L4 := Mp_lower solved n hn hpair 4
  have L5 := Mp_lower solved n hn hpair 5
  have hBeq : 5*B = 2*n+1 := hB.symm
  have U0 := Mp_upper solved n B hn w hBeq hpair hw5 hrest 0
  have U1 := Mp_upper solved n B hn w hBeq hpair hw5 hrest 1
  have U2 := Mp_upper solved n B hn w hBeq hpair hw5 hrest 2
  have U3 := Mp_upper solved n B hn w hBeq hpair hw5 hrest 3
  have U4 := Mp_upper solved n B hn w hBeq hpair hw5 hrest 4
  have U5 := Mp_upper solved n B hn w hBeq hpair hw5 hrest 5
  -- N = 12n+8
  have hNid := Ninc_identity solved hnall
  have hpart := sum_numSolvedExactly solved
  simp only [Finset.sum_range_succ, Finset.sum_range_zero] at hpart
  rw [← hn] at hpart
  have h6z := numSolvedExactly_six_eq_zero solved hnall
  have hNval : Ninc solved = 12*n + 8 := by rw [hNid]; omega
  have hlink := N_eq_sum_Mp solved
  unfold Ninc at hNval
  rw [hlink, Fin.sum_univ_six] at hNval
  -- generalize the six M-sums to opaque nats
  generalize hm0 : (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ (0:Fin 6)),
      (univ.filter (fun c => solved c 0 ∧ solved c q)).card) = M0 at F0 L0 U0 hNval
  generalize hm1 : (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ (1:Fin 6)),
      (univ.filter (fun c => solved c 1 ∧ solved c q)).card) = M1 at F1 L1 U1 hNval
  generalize hm2 : (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ (2:Fin 6)),
      (univ.filter (fun c => solved c 2 ∧ solved c q)).card) = M2 at F2 L2 U2 hNval
  generalize hm3 : (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ (3:Fin 6)),
      (univ.filter (fun c => solved c 3 ∧ solved c q)).card) = M3 at F3 L3 U3 hNval
  generalize hm4 : (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ (4:Fin 6)),
      (univ.filter (fun c => solved c 4 ∧ solved c q)).card) = M4 at F4 L4 U4 hNval
  generalize hm5 : (∑ q ∈ (univ : Finset (Fin 6)).filter (fun q => q ≠ (5:Fin 6)),
      (univ.filter (fun c => solved c 5 ∧ solved c q)).card) = M5 at F5 L5 U5 hNval
  generalize hb0 : (univ.filter (fun c => solved c (0:Fin 6))).card = b0 at F0
  generalize hb1 : (univ.filter (fun c => solved c (1:Fin 6))).card = b1 at F1
  generalize hb2 : (univ.filter (fun c => solved c (2:Fin 6))).card = b2 at F2
  generalize hb3 : (univ.filter (fun c => solved c (3:Fin 6))).card = b3 at F3
  generalize hb4 : (univ.filter (fun c => solved c (4:Fin 6))).card = b4 at F4
  generalize hb5 : (univ.filter (fun c => solved c (5:Fin 6))).card = b5 at F5
  exact hard_arith n t0 M0 M1 M2 M3 M4 M5 b0 b1 b2 b3 b4 b5
    F0 F1 F2 F3 F4 F5 L0 L1 L2 L3 L4 L5 U0 U1 U2 U3 U4 U5 hNval

-- ============ TOP-LEVEL THEOREM ============
set_option maxHeartbeats 1000000 in
/-- **IMO 2005 Problem 6.** In a competition with 6 problems where every pair of problems
    was solved by more than 2/5 of the contestants and nobody solved all 6, at least two
    contestants each solved exactly 5 problems. -/
theorem imo2005_p6
    (solved : C → Fin 6 → Prop) [DecidableRel solved]
    (n : ℕ) (hn : n = Fintype.card C)
    (hpair : ∀ i j : Fin 6, i ≠ j →
      2 * n < 5 * (univ.filter (fun c => solved c i ∧ solved c j)).card)
    (hnall : ∀ c : C, ∃ p : Fin 6, ¬ solved c p) :
    2 ≤ numSolvedExactly solved 5 := by
  rcases Nat.lt_or_ge (numSolvedExactly solved 5) 2 with h | h
  · exfalso
    interval_cases hc : (numSolvedExactly solved 5)
    · -- a5 = 0 : contradicts easy half
      have hpart := sum_numSolvedExactly solved
      have hNid := Ninc_identity solved hnall
      have hlow := Ninc_lower solved n hn hpair
      have h6z := numSolvedExactly_six_eq_zero solved hnall
      simp only [Finset.sum_range_succ, Finset.sum_range_zero] at hpart
      rw [← hn] at hpart
      omega
    · -- a5 = 1 : need 5 ∣ (2n+1), else the not-dvd branch already gives ≥2 (contradiction with =1).
      -- Case on divisibility:
      by_cases hd : 5 ∣ (2*n+1)
      · exact not_exactly_one_champion solved n hn hpair hnall hd hc
      · -- 5 ∤ (2n+1): sharper bound gives a5 ≥ 2, contradicting a5 = 1
        -- reuse the strengthened lower bound directly
        have hpart := sum_numSolvedExactly solved
        have hNid := Ninc_identity solved hnall
        have h6z := numSolvedExactly_six_eq_zero solved hnall
        simp only [Finset.sum_range_succ, Finset.sum_range_zero] at hpart
        rw [← hn] at hpart
        -- strengthened N lower bound: 30*(2n+2) ≤ 5N when 5∤(2n+1)
        have hcard_off : ((univ : Finset (Fin 6)).offDiag).card = 30 := by
          rw [Finset.offDiag_card, Finset.card_univ, Fintype.card_fin]
        have hlow2 : 30 * (2*n+2) ≤ 5 * Ninc solved := by
          unfold Ninc; rw [Finset.mul_sum]
          calc 30 * (2*n+2)
              = ∑ _ij ∈ (univ : Finset (Fin 6)).offDiag, (2*n+2) := by
                rw [Finset.sum_const, hcard_off, smul_eq_mul]
            _ ≤ ∑ ij ∈ (univ : Finset (Fin 6)).offDiag,
                  5 * (univ.filter (fun c => solved c ij.1 ∧ solved c ij.2)).card := by
                apply Finset.sum_le_sum
                intro ij hij
                rw [Finset.mem_offDiag] at hij
                have := hpair ij.1 ij.2 hij.2.2
                omega
        omega
  · exact h

end IMO2005P6

#print axioms IMO2005P6.imo2005_p6