Theorem: sum_odds_eq_square (LAMR/Examples/using_lean_as_a_proof_assistant/induction.lean)

State before:
n : ℕ
⊢ sum_odds n = n ^ 2
Tactic:
induction n with
| zero =>
    rw [sum_odds, Nat.zero_eq, pow_two, zero_mul]
| succ n ih =>
    rw [sum_odds, ih, Nat.succ_eq_add_one]
    ring
State after:
no goals

State before:
case zero

⊢ sum_odds Nat.zero = Nat.zero ^ 2
Tactic:
rw [sum_odds, Nat.zero_eq, pow_two, zero_mul]
State after:
no goals

State before:
case succ
n : ℕ
ih : sum_odds n = n ^ 2
⊢ sum_odds (Nat.succ n) = Nat.succ n ^ 2
Tactic:
rw [sum_odds, ih, Nat.succ_eq_add_one]
State after:
case succ
n : ℕ
ih : sum_odds n = n ^ 2
⊢ 2 * n + 1 + n ^ 2 = (n + 1) ^ 2

State before:
case succ
n : ℕ
ih : sum_odds n = n ^ 2
⊢ 2 * n + 1 + n ^ 2 = (n + 1) ^ 2
Tactic:
ring
State after:
no goals