simp only [sum_succ, ih, pow_two, (show Nat.succ i = i + 1 from rfl)]
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
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)