Theorem: Usa1985P1.nicomachus (Compfiles/Usa1985P1.lean)

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

⊢ ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2

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

State before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
Tactic:
rw [Finset.sum_range_succ, ih, Finset.sum_range_succ]
State after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2

State before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2
Tactic:
have h1 : ((∑ x ∈ Finset.range n, x) + n) ^ 2 =
    ((∑ x ∈ Finset.range n, x))^2 +
       (2 * (∑ x ∈ Finset.range n, x) * n +
         n ^ 2) := by ring
State after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2

State before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2
Tactic:
rw [h1]
State after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)

State before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h2 : n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
Tactic:
omega
State after:
no goals

State before:
case zero

⊢ ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2
Tactic:
simp
State after:
no goals

State before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
Tactic:
ring
State after:
no goals

State before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
Tactic:
have h5 : 2 * ∑ x ∈ Finset.range n, x =
           (∑ x ∈ Finset.range n, x) * 2 := mul_comm _ _
State after:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2

State before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
Tactic:
rw [h5, Finset.sum_range_id_mul_two]
State after:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = n * (n - 1) * n + n ^ 2

State before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = n * (n - 1) * n + n ^ 2
Tactic:
cases' n with n
State after:
case zero
ih : ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2
h1 : (∑ x ∈ Finset.range 0, x + 0) ^ 2 = (∑ x ∈ Finset.range 0, x) ^ 2 + ((2 * ∑ x ∈ Finset.range 0, x) * 0 + 0 ^ 2)
h5 : 2 * ∑ x ∈ Finset.range 0, x = (∑ x ∈ Finset.range 0, x) * 2
⊢ 0 ^ 3 = 0 * (0 - 1) * 0 + 0 ^ 2

case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * (n + 1 - 1) * (n + 1) + (n + 1) ^ 2

State before:
case zero
ih : ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2
h1 : (∑ x ∈ Finset.range 0, x + 0) ^ 2 = (∑ x ∈ Finset.range 0, x) ^ 2 + ((2 * ∑ x ∈ Finset.range 0, x) * 0 + 0 ^ 2)
h5 : 2 * ∑ x ∈ Finset.range 0, x = (∑ x ∈ Finset.range 0, x) * 2
⊢ 0 ^ 3 = 0 * (0 - 1) * 0 + 0 ^ 2
Tactic:
simp
State after:
no goals

State before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * (n + 1 - 1) * (n + 1) + (n + 1) ^ 2
Tactic:
simp only [Nat.succ_sub_succ_eq_sub, tsub_zero, Nat.succ_eq_add_one]
State after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * n * (n + 1) + (n + 1) ^ 2

State before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * n * (n + 1) + (n + 1) ^ 2
Tactic:
ring
State after:
no goals