awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
h : ((r - 1) * n + c) % r ∈ {i ∈ range r | c % r = (n + i) % r}
⊢ {i ∈ range r | c % r = (n + i) % r}.Nonempty

Tactic:
use ((r - 1) * n + c) % r

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
h : ((r - 1) * n + c) % r < r ∧ c % r = (n + ((r - 1) * n + c) % r) % r
⊢ ((r - 1) * n + c) % r ∈ {i ∈ range r | c % r = (n + i) % r}

Tactic:
simp only [mem_filter, mem_range]

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
⊢ ((r - 1) * n + c) % r < r ∧ c % r = (n + ((r - 1) * n + c) % r) % r

Tactic:
⟨Nat.mod_lt _ hr, ?_⟩

Premises used: Nat.mod_lt, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
h : c % r = (n + ((r - 1) * n + c) % r) % r
⊢ ((r - 1) * n + c) % r < r ∧ c % r = (n + ((r - 1) * n + c) % r) % r

Tactic:
refine ⟨Nat.mod_lt _ hr, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
⊢ 1 + (r - 1) = r

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
h₄ h₅ : c % r = c % r
⊢ c % r = (n + ((r - 1) * n + c) % r) % 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]

Premises used: Nat.mul_add_mod_self_left, add_assoc, Nat.add_mod_mod, one_add_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
rw :
  2 * Finset.card (α := Sym2 (Fin (n + r))) (edgeFinset (turanGraph (n + r) r)) =
    2 * (#(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2)
⊢ Finset.card (α := Sym2 (Fin (n + r))) (edgeFinset (turanGraph (n + r) r)) =
    #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2

Tactic:
rw [← mul_right_inj' two_ne_zero]

Premises used: two_ne_zero, mul_right_inj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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
⊢ 2 * Finset.card (α := Sym2 (Fin (n + r))) (edgeFinset (turanGraph (n + r) r)) =
    2 * (#(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2)

Tactic:
simp_rw [mul_add, ← sum_degrees_eq_twice_card_edges,
    degree, neighborFinset_eq_filter, turanGraph, card_filter]

Premises used: SimpleGraph.sum_degrees_eq_twice_card_edges, SimpleGraph.turanGraph, Finset.card_filter, mul_add, SimpleGraph.neighborFinset_eq_filter, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
h : ∀ (v : Fin (n + r)), ∑ i : Fin (n + r), if (↑v : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0
| ∑ x : Fin (n + r), ∑ i : Fin (n + r), if (↑x : ℕ) % r ≠ (↑i : ℕ) % r then 1 else 0

Tactic:
enter [2, v]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
v : Fin (n + r)
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)
| ∑ i : Fin (n + r), if (↑v : ℕ) % r ≠ (↑i : ℕ) % 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]

Premises used: Fin.sum_univ_eq_sum_range, Ne, Fin.val, HMod.hMod, Finset.sum_range_add, OfNat.ofNat, ite
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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)
| ∑ x : Fin (n + r), ∑ i : Fin (n + r), if (↑x : ℕ) % r ≠ (↑i : ℕ) % 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]

Premises used: Finset.sum_range_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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
⊢ (∑ 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:
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]

Premises used: Finset.sum_range_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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)
⊢ ∑ 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:
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]

Premises used: Fin.sum_univ_eq_sum_range, Finset.sum_add_distrib, add_assoc, Ne, Finset.range, HMod.hMod, HAdd.hAdd, Finset.sum_range_add, OfNat.ofNat, Finset.sum, ite
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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)
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
⊢ (∑ 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:
congr 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
⊢ 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:
simp [← Fin.sum_univ_eq_sum_range]

Premises used: Fin.sum_univ_eq_sum_range
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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
⊢ (∑ 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:
rw [← add_assoc, sum_comm]

Premises used: add_assoc, Finset.sum_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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
⊢ (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:
simp_rw [ne_comm, ← two_mul]

Premises used: two_mul, ne_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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)
e_a₁ : (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = 2 * r.choose 2
⊢ (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:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
rw : ∑ _x ∈ range n, (r - 1)
| n * (r - 1)

Tactic:
rw [← card_range n, ← smul_eq_mul, ← sum_const]

Premises used: Finset.card_range, smul_eq_mul, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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))
⊢ (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = n * (r - 1)

Tactic:
conv_rhs => rw [← card_range n, ← smul_eq_mul, ← sum_const]

Premises used: Finset.card_range, smul_eq_mul, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
e_a : ∀ x ∈ range n, (∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = r - 1
⊢ 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:
congr!
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r x : ℕ
h : x ∈ range n
⊢ (∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = r - 1

Tactic:
sum_ne_add_mod_eq_sub_one

Premises used: _private.0.SimpleGraph.sum_ne_add_mod_eq_sub_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r x : ℕ
h : x ∈ range n
⊢ (∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = r - 1

Tactic:
exact sum_ne_add_mod_eq_sub_one

Premises used: _private.0.SimpleGraph.sum_ne_add_mod_eq_sub_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
e_a : (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r * (r - 1)
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = 2 * r.choose 2

Tactic:
rw [mul_comm 2, Nat.choose_two_right, Nat.div_two_mul_two_of_even (Nat.even_mul_pred_self r)]

Premises used: Nat.even_mul_pred_self, Nat.choose_two_right, Nat.div_two_mul_two_of_even, mul_comm, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
enter : r
| r * (r - 1)

Tactic:
enter [1]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
rw : #(range r)
| r

Tactic:
rw [← card_range r]

Premises used: Finset.card_range
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
enter : #(range r)
| r * (r - 1)

Tactic:
enter [1]; rw [← card_range r]

Premises used: Finset.card_range
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
e_a : (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = #(range r) * (r - 1)
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r * (r - 1)

Tactic:
conv_rhs => enter [1]; rw [← card_range r]

Premises used: Finset.card_range
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
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))
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = #(range r) * (r - 1)

Tactic:
rw [← smul_eq_mul, ← sum_const]

Premises used: smul_eq_mul, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
e_a : ∀ x ∈ range r, (∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r - 1
⊢ Eq (α := ℕ) (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) (∑ _x ∈ range r, (r - 1))

Tactic:
congr!
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r x : ℕ
h : x ∈ range r
⊢ (∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
sum_ne_add_mod_eq_sub_one

Premises used: _private.0.SimpleGraph.sum_ne_add_mod_eq_sub_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r x : ℕ
h : x ∈ range r
⊢ (∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
exact sum_ne_add_mod_eq_sub_one

Premises used: _private.0.SimpleGraph.sum_ne_add_mod_eq_sub_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
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
⊢ #(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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
inl : #(turanGraph n 0).edgeFinset = n.choose 2
⊢ #(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:
rw [Nat.mod_zero, tsub_self, zero_mul, Nat.zero_div, zero_add]

Premises used: Nat.mod_zero, MulZeroClass.zero_mul, Nat.zero_div, tsub_self, zero_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
⊢ Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = (Fintype.card (Fin n)).choose 2

Tactic:
have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = (Fintype.card (Fin n)).choose 2
⊢ Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2

Tactic:
rw [Fintype.card_fin] at this

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
⊢ Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2

Tactic:
this
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
h : turanGraph n 0 = ⊤
⊢ #(turanGraph n 0).edgeFinset = n.choose 2

Tactic:
convert! this
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
⊢ turanGraph n 0 = ⊤

Tactic:
turanGraph_zero

Premises used: SimpleGraph.turanGraph_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
this : Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2
⊢ turanGraph n 0 = ⊤

Tactic:
exact turanGraph_zero

Premises used: SimpleGraph.turanGraph_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n_1 r : ℕ
hr : r > 0
n : ℕ
⊢ (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) =
    (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * HPow.hPow (β := ℕ) (n / r) 2) * r

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n_1 r : ℕ
hr : r > 0
n : ℕ
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
⊢ (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:
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]

Premises used: Nat.sq_sub_sq, add_tsub_cancel_left, Nat.mod_add_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
rw₁ 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
⊢ (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:
rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]

Premises used: Nat.mul_div_mul_right, Nat.mul_add_div, zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n 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

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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
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
⊢ #(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

Premises used: lt_or_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
inr : #(turanGraph n r).edgeFinset = n.choose 2
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
rw [Nat.mod_eq_of_lt h, tsub_self, zero_mul, Nat.zero_div, zero_add]

Premises used: MulZeroClass.zero_mul, Nat.zero_div, tsub_self, Nat.mod_eq_of_lt, zero_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
⊢ Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = (Fintype.card (Fin n)).choose 2

Tactic:
have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
⊢ Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2

Tactic:
rw [Fintype.card_fin] at this

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
⊢ Finset.card (α := Sym2 (Fin n)) (edgeFinset ⊤) = n.choose 2

Tactic:
this
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
h₁ : turanGraph n r = ⊤
⊢ #(turanGraph n r).edgeFinset = n.choose 2

Tactic:
convert! this
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
h₁ : r = 0 ∨ n ≤ r
⊢ turanGraph n r = ⊤

Tactic:
rw [turanGraph_eq_top]

Premises used: SimpleGraph.turanGraph_eq_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
⊢ r = 0 ∨ n ≤ r

Tactic:
.inr h.le

Premises used: LT.lt.le, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
⊢ r = 0 ∨ n ≤ r

Tactic:
exact .inr h.le
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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 = n' + r

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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 = n' + r

Tactic:
have n'r : n = n' + r := by lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
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
⊢ #(turanGraph n r).edgeFinset =
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (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]

Premises used: add_assoc, SimpleGraph.card_edgeFinset_turanGraph_add, Nat.add_mod_right, Nat.add_div_right, add_rotate