Theorem: sum_squared_eq_sum_cubes (meetings/ex3.lean)

State before:
n : ℕ
⊢ (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
induction' n with n ih
State after:
case zero

⊢ (∑ x in Finset.range (Nat.zero + 1), x) ^ 2 = ∑ x in Finset.range (Nat.zero + 1), x ^ 3

case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (∑ x in Finset.range (Nat.succ n + 1), x) ^ 2 = ∑ x in Finset.range (Nat.succ n + 1), x ^ 3

State before:
case zero

⊢ (∑ x in Finset.range (Nat.zero + 1), x) ^ 2 = ∑ x in Finset.range (Nat.zero + 1), x ^ 3
Tactic:
ring_nf
State after:
case zero

⊢ (∑ x in Finset.range (1 + Nat.zero), x) ^ 2 = ∑ x in Finset.range (1 + Nat.zero), x ^ 3

State before:
case zero

⊢ (∑ x in Finset.range (1 + Nat.zero), x) ^ 2 = ∑ x in Finset.range (1 + Nat.zero), x ^ 3
Tactic:
simp only [Nat.zero_eq, add_zero, Finset.range_one, Finset.sum_singleton, ne_eq,
  OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow']
State after:
no goals

State before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (∑ x in Finset.range (Nat.succ n + 1), x) ^ 2 = ∑ x in Finset.range (Nat.succ n + 1), x ^ 3
Tactic:
rw [Finset.range_succ,
    Finset.sum_insert Finset.not_mem_range_self,
    Finset.sum_insert Finset.not_mem_range_self]
State after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1 + ∑ x in Finset.range (n + 1), x) ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3

State before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1 + ∑ x in Finset.range (n + 1), x) ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
rw [add_sq]
State after:
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

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

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

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

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

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

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

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

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

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]
State after:
no goals

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]
State after:
no goals

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

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

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
State after:
no goals

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

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)
State after:
no goals