awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 * (n' / r + 1) * (r - 1) + r * (r - 1) * HPow.hPow (β := ℕ) (n' / r + 1) 2 / 2
⊢ 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:
congr 1
-- 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
⊢ 2 ∣ r * (r - 1)

Tactic:
have rd : 2 ∣ r * (r - 1) := (Nat.even_mul_pred_self _).two_dvd
-- 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
rd : 2 ∣ r * (r - 1)
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
⊢ 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:
rw [← Nat.div_mul_right_comm rd, ← Nat.div_mul_right_comm rd, ← Nat.choose_two_right]

Premises used: Nat.choose_two_right, Nat.div_mul_right_comm
-- 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
rd : 2 ∣ r * (r - 1)
⊢ 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:
grind
-- 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
rd : 2 ∣ r * (r - 1)
⊢ 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
-- 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
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) + 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
⊢ 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 [ring₂, ← add_assoc]

Premises used: add_assoc
-- 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
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) + 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)
⊢ 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:
congr 1
-- 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
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 * (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
⊢ 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:
rw [← add_rotate, ← add_rotate _ _ (r.choose 2)]

Premises used: Nat.choose, add_rotate, OfNat.ofNat
-- 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
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 * (n' / r) * (r - 1) + n' * (r - 1) = r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1)
⊢ 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:
congr 1
-- 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
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 * (n' / r) * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r) + n' % r * (n' / r) * (r - 1)
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1)

Tactic:
rw [Nat.choose_two_right, Nat.div_mul_cancel rd, mul_add_one, add_mul, ← add_assoc,
        ← add_rotate, add_comm _ (_ * _)]

Premises used: add_mul, Nat.div_mul_cancel, HMul.hMul, add_assoc, Nat.choose_two_right, add_comm, add_rotate, mul_add_one
-- 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
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) + r * (r - 1) * (n' / r)
⊢ 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:
congr 1
-- 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
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)
inr₄ inr₅ : n' * (r - 1) = n' * (r - 1)
⊢ n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)

Tactic:
rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]

Premises used: add_mul, Nat.div_add_mod, add_comm, mul_comm, mul_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
grw :
  (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) + 2 * r * (n % r).choose 2 ≤
    (r - 1) * HPow.hPow (β := ℕ) n 2
⊢ 2 * r * #(turanGraph n r).edgeFinset ≤ (r - 1) * HPow.hPow (β := ℕ) n 2

Tactic:
grw [card_edgeFinset_turanGraph, mul_add, Nat.mul_div_le]

Premises used: mul_add, Nat.mul_div_le, SimpleGraph.card_edgeFinset_turanGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
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
rw₁ : HPow.hPow (β := ℕ) (n % r) 2 * (r - 1) ≤ HPow.hPow (β := ℕ) n 2 * (r - 1)
⊢ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) + 2 * r * (n % r).choose 2 ≤
    (r - 1) * HPow.hPow (β := ℕ) n 2

Tactic:
rw [tsub_mul, ← Nat.sub_add_comm]

Premises used: Nat.sub_add_comm, tsub_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
h₁ : LE.le (α := ℕ) 0 (n % r)
⊢ HPow.hPow (β := ℕ) (n % r) 2 * (r - 1) ≤ HPow.hPow (β := ℕ) n 2 * (r - 1)

Tactic:
grw [Nat.mod_le]

Premises used: Nat.mod_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
⊢ LE.le (α := ℕ) 0 (n % r)

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
⊢ LE.le (α := ℕ) 0 (n % r)

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
rw : (n % r - 1) * r * (n % r) ≤ (r - 1) * (n % r) * (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

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)]

Premises used: Nat.even_mul_pred_self, mul_assoc, Nat.choose_two_right, HSub.hSub, Nat.sub_le_iff_le_add, mul_div_cancel_left₀, sq, two_ne_zero, Nat.add_le_add_iff_left, Even.two_dvd, mul_comm, OfNat.ofNat, Nat.mul_div_assoc, mul_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
bc : (n % r - 1) * r ≤ (r - 1) * (n % r)
⊢ (n % r - 1) * r * (n % r) ≤ (r - 1) * (n % r) * (n % r)

Tactic:
gcongr ?_ * _
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
bc : (n % 0 - 1) * 0 ≤ HSub.hSub (α := ℕ) 0 1 * (n % 0)
bc₁ : ∀ (hr : r > 0), (n % r - 1) * r ≤ (r - 1) * (n % r)
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)

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 : ℕ
⊢ (n % 0 - 1) * 0 ≤ HSub.hSub (α := ℕ) 0 1 * (n % 0)

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : r > 0
bc : r * (n % r) - r ≤ r * (n % r) - n % r
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)

Tactic:
rw [Nat.sub_one_mul, Nat.sub_one_mul, mul_comm]

Premises used: Nat.sub_one_mul, mul_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : r > 0
⊢ r * (n % r) - r ≤ r * (n % r) - n % r

Tactic:
Nat.sub_le_sub_left (Nat.mod_lt _ hr).le _

Premises used: Nat.sub_le_sub_left, LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : r > 0
⊢ r * (n % r) - r ≤ r * (n % r) - n % r

Tactic:
exact Nat.sub_le_sub_left (Nat.mod_lt _ hr).le _

Premises used: Nat.sub_le_sub_left, LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
inl :
  ∀ (cf : G.CliqueFree (HAdd.hAdd (α := ℕ) 0 1)),
    let n := Fintype.card V;
    #G.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),
    let n := Fintype.card V;
    #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
⊢ let n := Fintype.card V;
  #G.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:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
cf : G.CliqueFree (HAdd.hAdd (α := ℕ) 0 1)
⊢ Fintype.card V = 0

Tactic:
rw [cliqueFree_one, ← Fintype.card_eq_zero_iff] at cf

Premises used: Fintype.card_eq_zero_iff, SimpleGraph.cliqueFree_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
cf : Fintype.card V = 0
inl : #G.edgeFinset ≤ (Fintype.card V).choose 2
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤
    (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % 0) 2) * HSub.hSub (α := ℕ) 0 1 / HMul.hMul (α := ℕ) 2 0 +
      (n % 0).choose 2

Tactic:
simp_rw [zero_tsub, mul_zero, Nat.mod_zero, Nat.div_zero, zero_add]

Premises used: Nat.mod_zero, zero_add, MulZeroClass.mul_zero, Nat.div_zero, zero_tsub
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
card_edgeFinset_le_card_choose_two

Premises used: SimpleGraph.card_edgeFinset_le_card_choose_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
exact card_edgeFinset_le_card_choose_two

Premises used: SimpleGraph.card_edgeFinset_le_card_choose_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
inr :
  ∀ (H : SimpleGraph V) (w : DecidableRel H.Adj) (maxH : H.IsTuranMaximal r),
    let n := Fintype.card V;
    #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
obtain ⟨H, _, maxH⟩ := exists_isTuranMaximal (V := V) hr

Premises used: SimpleGraph.exists_isTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ #G.edgeFinset ≤ #H.edgeFinset

Tactic:
maxH.2 cf

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
h :
  (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2 =
    #H.edgeFinset
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) (n % r) 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
convert! maxH.2 cf

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
h :
  (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2 =
    Finset.card (α := Sym2 (Fin (Fintype.card V))) (edgeFinset (turanGraph (Fintype.card V) r))
h₁ h₂ :
  (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2 =
    (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2
⊢ (HPow.hPow (β := ℕ) (Fintype.card V) 2 - HPow.hPow (β := ℕ) (Fintype.card V % r) 2) * (r - 1) / (2 * r) +
      (Fintype.card V % r).choose 2 =
    #H.edgeFinset

Tactic:
rw [((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,
      card_edgeFinset_turanGraph]

Premises used: SimpleGraph.Iso.card_edgeFinset_eq, Nonempty.some, SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph, Iff.mp, SimpleGraph.card_edgeFinset_turanGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
hf :
  ∀ n ≥ 2,
    HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
      HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
⊢ AntitoneOn (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) (Set.Ici 2)

Tactic:
apply antitoneOn_nat_Ici_of_succ_le

Premises used: antitoneOn_nat_Ici_of_succ_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
enter : extremalNumber (n + 1) H
| HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ)

Tactic:
enter [1, 1]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
rw : extremalNumber (Fintype.card (Fin (n + 1))) H
| extremalNumber (n + 1) H

Tactic:
rw [← Fintype.card_fin (n + 1)]

Premises used: Fintype.card_fin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
enter : extremalNumber (Fintype.card (Fin (n + 1))) H
| HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ)

Tactic:
enter [1, 1]
    rw [← Fintype.card_fin (n + 1)]

Premises used: Fintype.card_fin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
hf :
  HDiv.hDiv (α := ℝ) (↑(extremalNumber (Fintype.card (Fin (n + 1))) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(extremalNumber (n + 1) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)

Tactic:
conv_lhs =>
    enter [1, 1]
    rw [← Fintype.card_fin (n + 1)]

Premises used: Fintype.card_fin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
linarith :
  n + 1 < 2 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑n : ℤ) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - 2) = 0
linarith₁ : n + 1 < 2 → GT.gt (α := ℤ) 2 0
⊢ 2 ≤ n + 1

Tactic:
linarith
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) * (↑((n + 1).choose 2) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
hf :
  ∀ ⦃G : SimpleGraph (Fin (n + 1))⦄ [inst : DecidableRel G.Adj],
    H.Free G →
      (↑(#G.edgeFinset) : ℝ) ≤
        HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) * (↑((n + 1).choose 2) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(extremalNumber (Fintype.card (Fin (n + 1))) H) : ℝ) (↑((n + 1).choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)

Tactic:
rw [div_le_iff₀ (mod_cast Nat.choose_pos (by linarith)),
    extremalNumber_le_iff_of_nonneg H (by positivity)]

Premises used: div_le_iff₀, SimpleGraph.extremalNumber_le_iff_of_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
hf :
  ∀ [inst : DecidableRel G.Adj],
    H.Free G →
      (↑(#G.edgeFinset) : ℝ) ≤
        HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) * (↑((n + 1).choose 2) : ℝ)
⊢ ∀ [inst : DecidableRel G.Adj],
    H.Free G →
      (↑(#G.edgeFinset) : ℝ) ≤
        HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) * (↑((n + 1).choose 2) : ℝ)

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
⊢ 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) 2

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
⊢ 0 < n

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
hf : #G.edgeFinset * (n - 1) ≤ (n + 1) * extremalNumber n H
⊢ (↑(#G.edgeFinset) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) * (↑((n + 1).choose 2) : ℝ)

Tactic:
rw [mul_comm, ← mul_div_assoc, le_div_iff₀' (mod_cast Nat.choose_pos hn), Nat.cast_choose_two,
    Nat.cast_choose_two, Nat.cast_add_one, add_sub_cancel_right (n : ℝ) 1,
    mul_comm _ (n - 1 : ℝ), ← mul_div (n - 1 : ℝ), mul_comm _ (n / 2 : ℝ), mul_assoc,
    mul_comm (n - 1 : ℝ), ← mul_div (n + 1 : ℝ), mul_comm _ (n / 2 : ℝ), mul_assoc,
    mul_le_mul_iff_right₀ (by positivity), ← Nat.cast_pred (by positivity), ← Nat.cast_mul,
    ← Nat.cast_add_one, ← Nat.cast_mul, Nat.cast_le]

Premises used: mul_div, le_div_iff₀', mul_assoc, mul_div_assoc, Nat.cast_pred, HSub.hSub, HDiv.hDiv, Nat.cast, Nat.cast_mul, HAdd.hAdd, mul_comm, Nat.cast_choose_two, Nat.cast_le, add_sub_cancel_right, OfNat.ofNat, Nat.cast_add_one, mul_le_mul_iff_right₀