Theorem: procedure_two_eq_squares (ListPowersProblem.lean)

State before:
⊢ sum (dropEveryNth 2 pnats) = powers 2
Tactic:
funext i
State after:
case h
i : ℕ
⊢ sum (dropEveryNth 2 pnats) i = powers 2 i

State before:
case h
i : ℕ
⊢ sum (dropEveryNth 2 pnats) i = powers 2 i
Tactic:
simp [dropEveryNth_two_eq_mul_two, powers, pnats]
State after:
case h
i : ℕ
⊢ sum (fun i => i * 2 + 1) i = (i + 1) ^ 2

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

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

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

State before:
case h.zero

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

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

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