awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
rw :
  Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    G.IsTuranMaximal (Fintype.card α - 1)
⊢ Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) (Fintype.card α - 1)))
have rw₁ : Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
  G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤)
Tactic: rw [← isTuranMaximal_iff_nonempty_iso_turanGraph (Nat.sub_pos_iff_lt.mpr one_lt_card),
    ← isExtremal_top_free_iff_isTuranMaximal, isExtremal_free_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
rw :
  Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    G.IsTuranMaximal (Fintype.card α - 1)
rw₁ :
  Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤)
⊢ Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) (Fintype.card α - 1)))
have rw₂ : Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
  Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤
Tactic: rw [← isTuranMaximal_iff_nonempty_iso_turanGraph (Nat.sub_pos_iff_lt.mpr one_lt_card),
    ← isExtremal_top_free_iff_isTuranMaximal, isExtremal_free_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
have inl : (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = HSub.hSub (α := ℕ) 0 1
Tactic: rcases r.eq_zero_or_pos with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
inl : (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = HSub.hSub (α := ℕ) 0 1
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
have inr : ∀ (hr : r > 0), (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
Tactic: rcases r.eq_zero_or_pos with rfl | hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
have rw : #({i ∈ range r | c % r ≠ (n + i) % r}) = r - #({i ∈ range r | c % r = (n + i) % r})
Tactic: rw [← card_filter, ← this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #({i ∈ range r | c % r ≠ (n + i) % r}) = r - #({i ∈ range r | c % r = (n + i) % r})
have h : #({i ∈ range r | c % r = (n + i) % r}) + #({i ∈ range r | c % r ≠ (n + i) % r}) = r
Tactic: apply Nat.eq_sub_of_add_eq'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #({i ∈ range r | c % r = (n + i) % r}) + #({i ∈ range r | c % r ≠ (n + i) % r}) = r
have h : #(range r) = r
Tactic: rw [card_filter_add_card_filter_not, card_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
h : #(range r) = r
⊢ #({i ∈ range r | c % r = (n + i) % r}) + #({i ∈ range r | c % r ≠ (n + i) % r}) = r
have h₁ : r = r
Tactic: rw [card_filter_add_card_filter_not, card_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
have inr : #({i ∈ range r | c % r = (n + i) % r}) = 1
Tactic: suffices #{i ∈ range r | c % r = (n + i) % r} = 1 by
    rw [← card_filter, ← this]; apply Nat.eq_sub_of_add_eq'
    rw [card_filter_add_card_filter_not, card_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ #({i ∈ range r | c % r = (n + i) % r}) = 1
have inr : #({i ∈ range r | c % r = (n + i) % r}) ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
inr : #({i ∈ range r | c % r = (n + i) % r}) ≤ 1
⊢ #({i ∈ range r | c % r = (n + i) % r}) = 1
have inr₁ : 1 ≤ #({i ∈ range r | c % r = (n + i) % r})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ #({i ∈ range r | c ≡ n + i [MOD r]}) ≤ 1
have inr : ∀ {a b : ℕ}, a ∈ {i ∈ range r | c ≡ n + i [MOD r]} → b ∈ {i ∈ range r | c ≡ n + i [MOD r]} → a = b
Tactic: rw [card_le_one_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w ∈ {i ∈ range r | c ≡ n + i [MOD r]}
mx : x ∈ {i ∈ range r | c ≡ n + i [MOD r]}
⊢ w = x
have mw₁ : w < r ∧ c ≡ n + w [MOD r]
Tactic: simp only [mem_filter, mem_range] at mw mx
Cleared hypotheses: mw, mx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w ∈ {i ∈ range r | c ≡ n + i [MOD r]}
mx : x ∈ {i ∈ range r | c ≡ n + i [MOD r]}
mw₁ : w < r ∧ c ≡ n + w [MOD r]
⊢ w = x
have mx₁ : x < r ∧ c ≡ n + x [MOD r]
Tactic: simp only [mem_filter, mem_range] at mw mx
Cleared hypotheses: mw, mx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
⊢ w = x
have this : n + w ≡ n + x [MOD r]
Tactic: have := mw.2.symm.trans mx.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : n + w ≡ n + x [MOD r]
⊢ w = x
have this₁ : w ≡ x [MOD r]
Tactic: rw [Nat.ModEq.add_iff_left rfl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w ≡ x [MOD r]
⊢ w = x
have this₁ : w % r = x % r
Tactic: change w % r = x % r at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w % r = x % r
⊢ w = x
have inr : ∀ (this : w = x % r), w = x
Tactic: rwa [Nat.mod_eq_of_lt mw.1, Nat.mod_eq_of_lt mx.1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w % r = x % r
inr : ∀ (this : w = x % r), w = x
⊢ w = x
have inr₁ : ∀ (this : w = x), w = x
Tactic: rwa [Nat.mod_eq_of_lt mw.1, Nat.mod_eq_of_lt mx.1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ 1 ≤ #({i ∈ range r | c % r = (n + i) % r})
have inr : {i ∈ range r | c % r = (n + i) % r}.Nonempty
Tactic: rw [one_le_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ {i ∈ range r | c % r = (n + i) % r}.Nonempty
have h : ((r - 1) * n + c) % r ∈ {i ∈ range r | c % r = (n + i) % r}
Tactic: use ((r - 1) * n + c) % r
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ ((r - 1) * n + c) % r ∈ {i ∈ range r | c % r = (n + i) % r}
have h : ((r - 1) * n + c) % r < r ∧ c % r = (n + ((r - 1) * n + c) % r) % r
Tactic: simp only [mem_filter, mem_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ ((r - 1) * n + c) % r < r ∧ c % r = (n + ((r - 1) * n + c) % r) % r
have h : c % r = (n + ((r - 1) * n + c) % r) % r
Tactic: refine ⟨Nat.mod_lt _ hr, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
⊢ c % r = (n + ((r - 1) * n + c) % r) % r
have h : c % r = (n + ((r - 1) * n + c)) % r
Tactic: rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
      Nat.mul_add_mod_self_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
h : c % r = (n + ((r - 1) * n + c)) % r
⊢ c % r = (n + ((r - 1) * n + c) % r) % r
have h₁ : c % r = (n + (r - 1) * n + c) % r
Tactic: rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
      Nat.mul_add_mod_self_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
h : c % r = (n + ((r - 1) * n + c)) % r
h₁ : c % r = (n + (r - 1) * n + c) % r
⊢ c % r = (n + ((r - 1) * n + c) % r) % r
have h₂ : c % r = ((1 + (r - 1)) * n + c) % r
Tactic: rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
      Nat.mul_add_mod_self_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
h : c % r = (n + ((r - 1) * n + c)) % r
h₁ : c % r = (n + (r - 1) * n + c) % r
h₂ : c % r = ((1 + (r - 1)) * n + c) % r
⊢ c % r = (n + ((r - 1) * n + c) % r) % r
have h₃ : c % r = (r * n + c) % r
Tactic: rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
      Nat.mul_add_mod_self_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r c : ℕ
hr : r > 0
h : c % r = (n + ((r - 1) * n + c)) % r
h₁ : c % r = (n + (r - 1) * n + c) % r
h₂ : c % r = ((1 + (r - 1)) * n + c) % r
h₃ : c % r = (r * n + c) % r
⊢ c % r = (n + ((r - 1) * n + c) % r) % r
have h₄ : c % r = c % r
Tactic: rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
      Nat.mul_add_mod_self_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ Finset.card (α := Sym2 (Fin (n + r))) (edgeFinset (turanGraph (n + r) r)) =
    #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2
have rw : 2 * Finset.card (α := Sym2 (Fin (n + r))) (edgeFinset (turanGraph (n + r) r)) =
  2 * (#(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2)
Tactic: rw [← mul_right_inj' two_ne_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ 2 * Finset.card (α := Sym2 (Fin (n + r))) (edgeFinset (turanGraph (n + r) r)) =
    2 * (#(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2)
have simp_rw : (∑ x : Fin (n + r), ∑ i : Fin (n + r), if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) =
  (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2
Tactic: simp_rw [mul_add, ← sum_degrees_eq_twice_card_edges,
    degree, neighborFinset_eq_filter, turanGraph, card_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
| ∑ x : Fin (n + r), ∑ i : Fin (n + r), if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0
have h : ∀ (v : Fin (n + r)), ∑ i : Fin (n + r), if (↑v : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0
Tactic: enter [2, v]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
v : Fin (n + r)
| ∑ i : Fin (n + r), if (↑v : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0
have h : HAdd.hAdd (α := ℕ) (∑ x ∈ range n, if (↑v : ℕ) % r ≠ x % r then 1 else 0)
  (∑ x ∈ range r, if (↑v : ℕ) % r ≠ (n + x) % r then 1 else 0)
Tactic: rw [Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0, sum_range_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
| ∑ x : Fin (n + r), ∑ i : Fin (n + r), if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0
have h : ∀ (v : Fin (n + r)),
  HAdd.hAdd (α := ℕ) (∑ x ∈ range n, if (↑v : ℕ) % r ≠ x % r then 1 else 0)
    (∑ x ∈ range r, if (↑v : ℕ) % r ≠ (n + x) % r then 1 else 0)
Tactic: enter [2, v]
    rw [Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0, sum_range_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∑ x : Fin (n + r), ∑ i : Fin (n + r), if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) =
    (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2
have conv_lhs : ∑ v : Fin (n + r),
    HAdd.hAdd (α := ℕ) (∑ x ∈ range n, if (↑v : ℕ) % r ≠ x % r then 1 else 0)
      (∑ x ∈ range r, if (↑v : ℕ) % r ≠ (n + x) % r then 1 else 0) =
  (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2
Tactic: conv_lhs =>
    enter [2, v]
    rw [Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0, sum_range_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ ∑ v : Fin (n + r),
      HAdd.hAdd (α := ℕ) (∑ x ∈ range n, if (↑v : ℕ) % r ≠ x % r then 1 else 0)
        (∑ x ∈ range r, if (↑v : ℕ) % r ≠ (n + x) % r then 1 else 0) =
    (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2
have rw : (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
    ((∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      HAdd.hAdd (α := ℕ) (∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0)
        (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0)) =
  (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) + (2 * (n * (r - 1)) + 2 * r.choose 2)
Tactic: rw [sum_add_distrib,
    Fin.sum_univ_eq_sum_range fun v ↦ ∑ w ∈ range n, if v % r ≠ w % r then 1 else 0,
    Fin.sum_univ_eq_sum_range fun v ↦ ∑ w ∈ range r, if v % r ≠ (n + w) % r then 1 else 0,
    sum_range_add, sum_range_add, add_assoc, add_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
        HAdd.hAdd (α := ℕ) (∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0)
          (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0)) =
    (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) + (2 * (n * (r - 1)) + 2 * r.choose 2)
have e_a : Eq (α := ℕ) (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0)
  (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
e_a :
  Eq (α := ℕ) (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0)
    (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0)
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
        HAdd.hAdd (α := ℕ) (∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0)
          (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0)) =
    (∑ x : Fin n, ∑ i : Fin n, if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0) + (2 * (n * (r - 1)) + 2 * r.choose 2)
have e_a₁ : (∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
    HAdd.hAdd (α := ℕ) (∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0)
      (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
  2 * (n * (r - 1)) + 2 * r.choose 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      HAdd.hAdd (α := ℕ) (∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0)
        (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
have e_a : (HAdd.hAdd (α := ℕ) (∑ y ∈ range n, ∑ x ∈ range r, if (n + x) % r ≠ y % r then 1 else 0)
      (∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
    ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
  2 * (n * (r - 1)) + 2 * r.choose 2
Tactic: rw [← add_assoc, sum_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (HAdd.hAdd (α := ℕ) (∑ y ∈ range n, ∑ x ∈ range r, if (n + x) % r ≠ y % r then 1 else 0)
        (∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
have e_a : (HMul.hMul (α := ℕ) 2 (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
    ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
  2 * (n * (r - 1)) + 2 * r.choose 2
Tactic: simp_rw [ne_comm, ← two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (HMul.hMul (α := ℕ) 2 (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
have e_a : (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = n * (r - 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
e_a : (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = n * (r - 1)
⊢ (HMul.hMul (α := ℕ) 2 (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
have e_a₁ : (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = 2 * r.choose 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
| n * (r - 1)
have rw : ∑ _x ∈ range n, (r - 1)
Tactic: rw [← card_range n, ← smul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = n * (r - 1)
have e_a : Eq (α := ℕ) (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) (∑ _x ∈ range n, (r - 1))
Tactic: conv_rhs => rw [← card_range n, ← smul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) (∑ _x ∈ range n, (r - 1))
have e_a : ∀ x ∈ range n, (∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = r - 1
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = 2 * r.choose 2
have e_a : (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r * (r - 1)
Tactic: rw [mul_comm 2, Nat.choose_two_right, Nat.div_two_mul_two_of_even (Nat.even_mul_pred_self r)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
| r * (r - 1)
have enter : r
Tactic: enter [1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
| r
have rw : #(range r)
Tactic: rw [← card_range r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
| r * (r - 1)
have enter : #(range r)
Tactic: enter [1]; rw [← card_range r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r * (r - 1)
have e_a : (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = #(range r) * (r - 1)
Tactic: conv_rhs => enter [1]; rw [← card_range r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = #(range r) * (r - 1)
have e_a : Eq (α := ℕ) (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) (∑ _x ∈ range r, (r - 1))
Tactic: rw [← smul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) (∑ _x ∈ range r, (r - 1))
have e_a : ∀ x ∈ range r, (∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r - 1
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inl : #(turanGraph n 0).edgeFinset =
  (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
    (n % 0).choose 2
Tactic: rcases r.eq_zero_or_pos with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
inl :
  #(turanGraph n 0).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
      (n % 0).choose 2
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inr : ∀ (hr : r > 0),
  #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
Tactic: rcases r.eq_zero_or_pos with rfl | hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n : ℕ
⊢ #(turanGraph n 0).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
      (n % 0).choose 2
have inl : #(turanGraph n 0).edgeFinset = n.choose 2
Tactic: rw [Nat.mod_zero, tsub_self, zero_mul, Nat.zero_div, zero_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n : ℕ
⊢ #(turanGraph n 0).edgeFinset = n.choose 2
have this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = (Fintype.card (Fin n)).choose 2
Tactic: have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n : ℕ
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = (Fintype.card (Fin n)).choose 2
⊢ #(turanGraph n 0).edgeFinset = n.choose 2
have this₁ : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
Tactic: rw [Fintype.card_fin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n : ℕ
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
⊢ #(turanGraph n 0).edgeFinset = n.choose 2
have h : turanGraph n 0 = ⊤
Tactic: convert! this