Theorem: exercise4_1 (LeanCourse/Assignments/Solutions/Solutions4.lean)

State before:
n : ℕ
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (∑ i in range (n + 1), ↑i) ^ 2
Tactic:
have : ∀ n, (∑ i in range (n + 1), i : ℚ) = n * (n + 1) / 2
State after:
case this
n : ℕ
⊢ ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2

n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (∑ i in range (n + 1), ↑i) ^ 2

State before:
n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (∑ i in range (n + 1), ↑i) ^ 2
Tactic:
rw [this]
State after:
n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2

State before:
n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [sum_range_succ, ih]
  push_cast
  ring
State after:
no goals

State before:
case this
n : ℕ
⊢ ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
Tactic:
intro n
State after:
case this
n✝ n : ℕ
⊢ ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2

State before:
case this
n✝ n : ℕ
⊢ ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
Tactic:
induction n with
| zero => simp
| succ n ih =>
rw [sum_range_succ, ih]
push_cast
ring
State after:
no goals

State before:
case this.zero
n : ℕ
⊢ ∑ i in range (0 + 1), ↑i = ↑0 * (↑0 + 1) / 2
Tactic:
simp
State after:
no goals

State before:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1 + 1), ↑i = ↑(n + 1) * (↑(n + 1) + 1) / 2
Tactic:
rw [sum_range_succ, ih]
State after:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + ↑(n + 1) = ↑(n + 1) * (↑(n + 1) + 1) / 2

State before:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + ↑(n + 1) = ↑(n + 1) * (↑(n + 1) + 1) / 2
Tactic:
push_cast
State after:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + (↑n + 1) = (↑n + 1) * (↑n + 1 + 1) / 2

State before:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + (↑n + 1) = (↑n + 1) * (↑n + 1 + 1) / 2
Tactic:
ring
State after:
no goals

State before:
case zero
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (0 + 1), ↑(i ^ 3) = (↑0 * (↑0 + 1) / 2) ^ 2
Tactic:
simp
State after:
no goals

State before:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ ∑ i in range (n + 1 + 1), ↑(i ^ 3) = (↑(n + 1) * (↑(n + 1) + 1) / 2) ^ 2
Tactic:
rw [sum_range_succ, ih]
State after:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + ↑((n + 1) ^ 3) = (↑(n + 1) * (↑(n + 1) + 1) / 2) ^ 2

State before:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + ↑((n + 1) ^ 3) = (↑(n + 1) * (↑(n + 1) + 1) / 2) ^ 2
Tactic:
push_cast
State after:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + (↑n + 1) ^ 3 = ((↑n + 1) * (↑n + 1 + 1) / 2) ^ 2

State before:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + (↑n + 1) ^ 3 = ((↑n + 1) * (↑n + 1 + 1) / 2) ^ 2
Tactic:
ring
State after:
no goals