Theorem: sumDrop_three (ListPowersProblem.lean)

State before:
⊢ sumDrop 3 pnats = powers 3
Tactic:
funext i
State after:
case h
i : ℕ
⊢ sumDrop 3 pnats i = powers 3 i

State before:
case h
i : ℕ
⊢ sumDrop 3 pnats i = powers 3 i
Tactic:
simp only [sumDrop, powers, pow_three, 
  dropEveryNth_eq_fun, pnats, Nat.div_one,
  sum_eq_three_even
]
State after:
case h
i : ℕ
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))

State before:
case h
i : ℕ
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
Tactic:
induction' i with i ih
State after:
case h.zero

⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) Nat.zero = (Nat.zero + 1) * ((Nat.zero + 1) * (Nat.zero + 1))

case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) (Nat.succ i) = (Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1))

State before:
case h.zero

⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) Nat.zero = (Nat.zero + 1) * ((Nat.zero + 1) * (Nat.zero + 1))
Tactic:
rfl
State after:
no goals

State before:
case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) (Nat.succ i) = (Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1))
Tactic:
simp [ih, show Nat.succ i = i + 1 from rfl]
State after:
case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ (i + 1) * ((i + 1) * (i + 1)) + (3 * ((i + 1) ^ 2 + (i + 1)) + 1) = (i + 1 + 1) * ((i + 1 + 1) * (i + 1 + 1))

State before:
case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ (i + 1) * ((i + 1) * (i + 1)) + (3 * ((i + 1) ^ 2 + (i + 1)) + 1) = (i + 1 + 1) * ((i + 1 + 1) * (i + 1 + 1))
Tactic:
ring
State after:
no goals