awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n_1 r : ℕ
hr : r > 0
n : ℕ
⊢ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
have nth_rw : (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2) * r / (2 * r) =
  n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
Tactic: nth_rw 1 [← Nat.mod_add_div n r, Nat.sq_sub_sq, add_tsub_cancel_left,
        show (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) =
          (2 * ((n % r) * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r by grind]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n_1 r : ℕ
hr : r > 0
n : ℕ
⊢ (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2) * r / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
have rw : (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2) / 2 =
  n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
Tactic: rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n_1 r : ℕ
hr : r > 0
n : ℕ
rw :
  (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2) / 2 =
    n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
⊢ (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2) * r / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
have rw₁ : n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2 =
  n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
Tactic: rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r : ℕ
hr : r > 0
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have ring₁ : ∀ (n : ℕ),
  (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
Tactic: have ring₁ (n) : (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) =
        n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2 := by
      nth_rw 1 [← Nat.mod_add_div n r, Nat.sq_sub_sq, add_tsub_cancel_left,
        show (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) =
          (2 * ((n % r) * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r by grind]
      rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inr : ∀ (h : n < r),
  #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
Tactic: rcases lt_or_ge n r with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
inr :
  ∀ (h : n < r),
    #(turanGraph n r).edgeFinset =
      (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).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₁ : ∀ (h : r ≤ n),
  #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
Tactic: rcases lt_or_ge n r with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : n < r
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inr : #(turanGraph n r).edgeFinset = n.choose 2
Tactic: rw [Nat.mod_eq_of_lt h, tsub_self, zero_mul, Nat.zero_div, zero_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : n < r
⊢ #(turanGraph n r).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 r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : n < r
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = (Fintype.card (Fin n)).choose 2
⊢ #(turanGraph n r).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 r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : n < r
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
⊢ #(turanGraph n r).edgeFinset = n.choose 2
have h₁ : turanGraph n r = ⊤
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : n < r
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
⊢ turanGraph n r = ⊤
have h₁ : r = 0 ∨ n ≤ r
Tactic: rw [turanGraph_eq_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have n'r : n = n' + r
Tactic: have n'r : n = n' + r := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
have inr : n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r) 2 / 2) +
    (n' % r).choose 2 =
  n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r + 1) 2 / 2 + (n' % r).choose 2
Tactic: rw [n'r, card_edgeFinset_turanGraph_add, card_edgeFinset_turanGraph, ring₁, ring₁,
        add_rotate, ← add_assoc, Nat.add_mod_right, Nat.add_div_right _ hr]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r) 2 / 2) +
      (n' % r).choose 2 =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r + 1) 2 / 2 + (n' % r).choose 2
have inr : n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r) 2 / 2) =
  n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r + 1) 2 / 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r) 2 / 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r + 1) 2 / 2
have rd : 2 ∣ r * (r - 1)
Tactic: have rd : 2 ∣ r * (r - 1) := (Nat.even_mul_pred_self _).two_dvd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r) 2 / 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r + 1) 2 / 2
have inr : n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2) =
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2
Tactic: rw [← Nat.div_mul_right_comm rd, ← Nat.div_mul_right_comm rd, ← Nat.choose_two_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2) =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2
have ring₂ : n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
Tactic: have ring₂ : n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
          n' % r * (n' / r + 1) * (r - 1) + r.choose 2 +
          r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2 := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2) =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2
have inr : n' * (r - 1) + r.choose 2 + n' % r * (n' / r) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2 =
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
Tactic: rw [ring₂, ← add_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
⊢ n' * (r - 1) + r.choose 2 + n' % r * (n' / r) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
have inr : n' * (r - 1) + r.choose 2 + n' % r * (n' / r) * (r - 1) =
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
⊢ n' * (r - 1) + r.choose 2 + n' % r * (n' / r) * (r - 1) =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r)
have inr : n' % r * (n' / r) * (r - 1) + n' * (r - 1) + r.choose 2 =
  r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1) + r.choose 2
Tactic: rw [← add_rotate, ← add_rotate _ _ (r.choose 2)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) + r.choose 2 =
    r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1) + r.choose 2
have inr : n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1)
have inr : n' * (r - 1) + n' % r * (n' / r) * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r) + n' % r * (n' / r) * (r - 1)
Tactic: rw [Nat.choose_two_right, Nat.div_mul_cancel rd, mul_add_one, add_mul, ← add_assoc,
        ← add_rotate, add_comm _ (_ * _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
⊢ n' * (r - 1) + n' % r * (n' / r) * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r) + n' % r * (n' / r) * (r - 1)
have inr : n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
⊢ n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)
have inr : n' * (r - 1) = n' % r * (r - 1) + n' / r * r * (r - 1)
Tactic: rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
inr : n' * (r - 1) = n' % r * (r - 1) + n' / r * r * (r - 1)
⊢ n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)
have inr₁ : n' * (r - 1) = (n' % r + n' / r * r) * (r - 1)
Tactic: rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
inr : n' * (r - 1) = n' % r * (r - 1) + n' / r * r * (r - 1)
inr₁ : n' * (r - 1) = (n' % r + n' / r * r) * (r - 1)
⊢ n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)
have inr₂ : n' * (r - 1) = (n' / r * r + n' % r) * (r - 1)
Tactic: rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
inr : n' * (r - 1) = n' % r * (r - 1) + n' / r * r * (r - 1)
inr₁ : n' * (r - 1) = (n' % r + n' / r * r) * (r - 1)
inr₂ : n' * (r - 1) = (n' / r * r + n' % r) * (r - 1)
⊢ n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)
have inr₃ : n' * (r - 1) = (r * (n' / r) + n' % r) * (r - 1)
Tactic: rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : r > 0
ring₁ :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) =
      n % r * (n / r) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * HPow.hPow (β := ℕ) (n' / r + 1) 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) +
      r.choose 2 * HPow.hPow (β := ℕ) (n' / r) 2
inr : n' * (r - 1) = n' % r * (r - 1) + n' / r * r * (r - 1)
inr₁ : n' * (r - 1) = (n' % r + n' / r * r) * (r - 1)
inr₂ : n' * (r - 1) = (n' / r * r + n' % r) * (r - 1)
inr₃ : n' * (r - 1) = (r * (n' / r) + n' % r) * (r - 1)
⊢ n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)
have inr₄ : n' * (r - 1) = n' * (r - 1)
Tactic: rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ 2 * r * #(turanGraph n r).edgeFinset ≤ (r - 1) * HPow.hPow (β := ℕ) n 2
have grw : (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) + 2 * r * (n % r).choose 2 ≤
  (r - 1) * HPow.hPow (β := ℕ) n 2
Tactic: grw [card_edgeFinset_turanGraph, mul_add, Nat.mul_div_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) + 2 * r * (n % r).choose 2 ≤
    (r - 1) * HPow.hPow (β := ℕ) n 2
have rw : HPow.hPow (β := ℕ) n 2 * (r - 1) + 2 * r * (n % r).choose 2 - HPow.hPow (β := ℕ) (n % r) 2 * (r - 1) ≤
  (r - 1) * HPow.hPow (β := ℕ) n 2
Tactic: rw [tsub_mul, ← Nat.sub_add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
rw :
  HPow.hPow (β := ℕ) n 2 * (r - 1) + 2 * r * (n % r).choose 2 - HPow.hPow (β := ℕ) (n % r) 2 * (r - 1) ≤
    (r - 1) * HPow.hPow (β := ℕ) n 2
⊢ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) + 2 * r * (n % r).choose 2 ≤
    (r - 1) * HPow.hPow (β := ℕ) n 2
have rw₁ : HPow.hPow (β := ℕ) (n % r) 2 * (r - 1) ≤ HPow.hPow (β := ℕ) n 2 * (r - 1)
Tactic: rw [tsub_mul, ← Nat.sub_add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ HPow.hPow (β := ℕ) (n % r) 2 * (r - 1) ≤ HPow.hPow (β := ℕ) n 2 * (r - 1)
have h₁ : LE.le (α := ℕ) 0 (n % r)
Tactic: grw [Nat.mod_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ HPow.hPow (β := ℕ) n 2 * (r - 1) + 2 * r * (n % r).choose 2 - HPow.hPow (β := ℕ) (n % r) 2 * (r - 1) ≤
    (r - 1) * HPow.hPow (β := ℕ) n 2
have rw : (n % r - 1) * r * (n % r) ≤ (r - 1) * (n % r) * (n % r)
Tactic: rw [Nat.sub_le_iff_le_add, mul_comm, Nat.add_le_add_iff_left, Nat.choose_two_right,
    ← Nat.mul_div_assoc _ (Nat.even_mul_pred_self _).two_dvd, mul_assoc,
    mul_div_cancel_left₀ _ two_ne_zero, ← mul_assoc, ← mul_rotate, sq, ← mul_rotate (r - 1)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (n % r - 1) * r * (n % r) ≤ (r - 1) * (n % r) * (n % r)
have bc : (n % r - 1) * r ≤ (r - 1) * (n % r)
Tactic: gcongr ?_ * _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)
have bc : (n % 0 - 1) * 0 ≤ HSub.hSub (α := ℕ) 0 1 * (n % 0)
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 : ℕ
bc : (n % 0 - 1) * 0 ≤ HSub.hSub (α := ℕ) 0 1 * (n % 0)
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)
have bc₁ : ∀ (hr : r > 0), (n % r - 1) * r ≤ (r - 1) * (n % r)
Tactic: rcases r.eq_zero_or_pos with rfl | hr