internlm/Lean-Github huggingface dataset:
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + (∑ x in Finset.range (n + 1), x) ^ 2 =
    (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
let S := ∑ x in Finset.range (n + 1), x
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + (∑ x in Finset.range (n + 1), x) ^ 2 =
    (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + (∑ x in Finset.range (n + 1), x) ^ 2 =
    (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
have hS : S = ∑ x in Finset.range (n + 1), x := rfl
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + (∑ x in Finset.range (n + 1), x) ^ 2 =
    (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + (∑ x in Finset.range (n + 1), x) ^ 2 =
    (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
nth_rewrite 2 [←hS]
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
have bigger (n : ℕ) : 1 ≤ n + 1 := by
  simp only [le_add_iff_nonneg_left, zero_le]
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
rw [Finset.sum_range_id]
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
zify [bigger]
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) + (∑ x in Finset.range (n + 1), ↑x) ^ 2 =
    (↑n + 1) ^ 3 + ∑ x in Finset.range (n + 1), ↑x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) + (∑ x in Finset.range (n + 1), ↑x) ^ 2 =
    (↑n + 1) ^ 3 + ∑ x in Finset.range (n + 1), ↑x ^ 3
Tactic:
have hring (n : ℤ):
  (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2)
  = (n + 1) ^ 3 := by
  have htwodvd : 2 ∣ ((n + 1) * (n + 1 - 1)) := by
    rw [add_sub_cancel, mul_comm]
    exact even_iff_two_dvd.1 (Int.even_mul_succ_self n)
  qify [htwodvd, bigger]
  push_cast
  ring_nf
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
hring : ∀ (n : ℤ), (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) + (∑ x in Finset.range (n + 1), ↑x) ^ 2 =
    (↑n + 1) ^ 3 + ∑ x in Finset.range (n + 1), ↑x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
hring : ∀ (n : ℤ), (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) + (∑ x in Finset.range (n + 1), ↑x) ^ 2 =
    (↑n + 1) ^ 3 + ∑ x in Finset.range (n + 1), ↑x ^ 3
Tactic:
zify at ih
Proof state after:
case succ
n : ℕ
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
hring : ∀ (n : ℤ), (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
ih : (∑ x in Finset.range (n + 1), ↑x) ^ 2 = ∑ x in Finset.range (n + 1), ↑x ^ 3
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) + (∑ x in Finset.range (n + 1), ↑x) ^ 2 =
    (↑n + 1) ^ 3 + ∑ x in Finset.range (n + 1), ↑x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
hring : ∀ (n : ℤ), (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
ih : (∑ x in Finset.range (n + 1), ↑x) ^ 2 = ∑ x in Finset.range (n + 1), ↑x ^ 3
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) + (∑ x in Finset.range (n + 1), ↑x) ^ 2 =
    (↑n + 1) ^ 3 + ∑ x in Finset.range (n + 1), ↑x ^ 3
Tactic:
rw [hring n, ih]
Proof state after:
no goals
Theorem: sum_squared_eq_sum_cubes
Proof state before:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
n : ℕ
⊢ 1 ≤ n + 1
Tactic:
simp only [le_add_iff_nonneg_left, zero_le]
Proof state after:
no goals
Theorem: sum_squared_eq_sum_cubes
Proof state before:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
Tactic:
have htwodvd : 2 ∣ ((n + 1) * (n + 1 - 1)) := by
  rw [add_sub_cancel, mul_comm]
  exact even_iff_two_dvd.1 (Int.even_mul_succ_self n)
Proof state after:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
htwodvd : 2 ∣ (n + 1) * (n + 1 - 1)
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
htwodvd : 2 ∣ (n + 1) * (n + 1 - 1)
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
Tactic:
qify [htwodvd, bigger]
Proof state after:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
htwodvd : 2 ∣ (n + 1) * (n + 1 - 1)
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) = (↑n + 1) ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
htwodvd : 2 ∣ (n + 1) * (n + 1 - 1)
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) = (↑n + 1) ^ 3
Tactic:
ring_nf
Proof state after:
no goals
Theorem: sum_squared_eq_sum_cubes
Proof state before:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
⊢ 2 ∣ (n + 1) * (n + 1 - 1)
Tactic:
rw [add_sub_cancel, mul_comm]
Proof state after:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
⊢ 2 ∣ n * (n + 1)
Theorem: sum_squared_eq_sum_cubes
Proof state before:
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
n : ℤ
⊢ 2 ∣ n * (n + 1)
Tactic:
exact even_iff_two_dvd.1 (Int.even_mul_succ_self n)
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
n : ℕ
⊢ 6 ∣ n ^ 3 - n
Tactic:
have gt_pow3 (n : ℕ) : n ≤ n ^ 3 := by
  apply Nat.le_self_pow
  simp
Proof state after:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ n ^ 3 - n
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ n ^ 3 - n
Tactic:
zify [gt_pow3 n]
Proof state after:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑n ^ 3 - ↑n
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑n ^ 3 - ↑n
Tactic:
induction' n using Nat.caseStrongInductionOn with n ih
Proof state after:
case zero
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑0 ^ 3 - ↑0

case ind
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
n✝ n : ℕ
⊢ n ≤ n ^ 3
Tactic:
apply Nat.le_self_pow
Proof state after:
case hn
n✝ n : ℕ
⊢ 3 ≠ 0
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case hn
n✝ n : ℕ
⊢ 3 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case zero
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑0 ^ 3 - ↑0
Tactic:
exact dvd_zero 6
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case ind
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
by_cases hp : n ≤ 3
Proof state after:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)

case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
let k : ℕ := n - 3
Proof state after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
have hk : Nat.succ n = k + 4 := by
  zify [le_of_not_le hp]
  ring_nf
Proof state after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
rw [hk]
Proof state after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(k + 4) ^ 3 - ↑(k + 4)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(k + 4) ^ 3 - ↑(k + 4)
Tactic:
push_cast (config := { zeta := false })
Proof state after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)
Tactic:
have hring (k : ℤ) :
  (k + 4) ^ 3 - (k + 4)
  = (k ^ 3 - k) + 6 * (2 * k ^ 2 + 8 * k + 10) := by
  ring_nf
Proof state after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)
Tactic:
rw [hring k]
Proof state after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)
Tactic:
rcases ih k (by simp) with ⟨m, hm⟩
Proof state after:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)
Tactic:
rw [hm, ←mul_add]
Proof state after:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ 6 * (m + (2 * ↑k ^ 2 + 8 * ↑k + 10))
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ 6 * (m + (2 * ↑k ^ 2 + 8 * ↑k + 10))
Tactic:
simp only [ge_iff_le, dvd_mul_right]
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
rw [Nat.succ_eq_add_one]
Proof state after:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rcases hp with _ | hp
Proof state after:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(3 + 1) ^ 3 - ↑(3 + 1)

case pos.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 2
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(3 + 1) ^ 3 - ↑(3 + 1)
Tactic:
ring_nf
Proof state after:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 60
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 60
Tactic:
have : (60 : ℤ) = 6 * 10 := by ring
Proof state after:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
this : 60 = 6 * 10
⊢ 6 ∣ 60
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
this : 60 = 6 * 10
⊢ 6 ∣ 60
Tactic:
simp_rw [this, dvd_mul_right]
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 60 = 6 * 10
Tactic:
ring
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 2
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rcases hp with _ | hp
Proof state after:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(2 + 1) ^ 3 - ↑(2 + 1)

case pos.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 1
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(2 + 1) ^ 3 - ↑(2 + 1)
Tactic:
ring_nf
Proof state after:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 24
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 24
Tactic:
have : (24 : ℤ) = 6 * 4 := by ring
Proof state after:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
this : 24 = 6 * 4
⊢ 6 ∣ 24
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
this : 24 = 6 * 4
⊢ 6 ∣ 24
Tactic:
simp_rw [this, dvd_mul_right]
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 24 = 6 * 4
Tactic:
ring
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 1
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rcases hp with _ | hp
Proof state after:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(1 + 1) ^ 3 - ↑(1 + 1)

case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(1 + 1) ^ 3 - ↑(1 + 1)
Tactic:
ring_nf
Proof state after:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 6
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 6
Tactic:
exact Int.dvd_refl 6
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
simp at hp
Proof state after:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rw [hp]
Proof state after:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(0 + 1) ^ 3 - ↑(0 + 1)
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(0 + 1) ^ 3 - ↑(0 + 1)
Tactic:
exact dvd_zero 6
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ Nat.succ n = k + 4
Tactic:
zify [le_of_not_le hp]
Proof state after:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ ↑n + 1 = ↑n - 3 + 4
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ ↑n + 1 = ↑n - 3 + 4
Tactic:
ring_nf
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k✝ : ℕ := n - 3
hk : Nat.succ n = k✝ + 4
k : ℤ
⊢ (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: six_dvd_n_cubed_minus_n
Proof state before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ k ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: binomial_theorem
Proof state before:
x y n : ℕ
⊢ (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
Tactic:
induction' n with n ih
Proof state after:
case zero
x y : ℕ
⊢ (x + y) ^ Nat.zero = ∑ k in Finset.range (Nat.zero + 1), Nat.choose Nat.zero k * x ^ (Nat.zero - k) * y ^ k

case succ
x y n : ℕ
ih : (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
⊢ (x + y) ^ Nat.succ n = ∑ k in Finset.range (Nat.succ n + 1), Nat.choose (Nat.succ n) k * x ^ (Nat.succ n - k) * y ^ k
Theorem: binomial_theorem
Proof state before:
case zero
x y : ℕ
⊢ (x + y) ^ Nat.zero = ∑ k in Finset.range (Nat.zero + 1), Nat.choose Nat.zero k * x ^ (Nat.zero - k) * y ^ k
Tactic:
simp
Proof state after:
no goals