Theorem: MyNat.succ_mul (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ succ a * b = a * b + b
Tactic:
induction b with
| zero =>
  rw [mul_zero, mul_zero, add_zero]
| succ b' ih =>
  show succ a * succ b' = a * succ b' + succ b'
  exact
    calc
      succ a * succ b' = succ a * (b' + one) := by rw [succ_eq_add_one b']
      _                = succ a * b' + succ a * one := by rw [mul_add]
      _                = succ a * b' + succ a := by rw [mul_one]
      _                = a * b' + b' + succ a := by rw [ih]
      _                = a * b' + succ a + b' := by rw [add_comm_right]
      _                = a * b' + (a + one) + b' := by rw [succ_eq_add_one]
      _                = a * b' + a + one + b' := by simp only [add_assoc]
      _                = a * succ b' + one + b' := by rw [← mul_succ]
      _                = a * succ b' + b' + one := by rw [add_comm_right]
      _                = a * succ b' + (b' + one) := by rw [add_assoc]
      _                = a * succ b' + succ b' := by rw [succ_eq_add_one]
State after:
no goals

State before:
case zero
a : Nat
⊢ succ a * zero = a * zero + zero
Tactic:
rw [mul_zero, mul_zero, add_zero]
State after:
no goals

State before:
case succ
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * succ b' = a * succ b' + succ b'
Tactic:
exact
  calc
    succ a * succ b' = succ a * (b' + one) := by rw [succ_eq_add_one b']
    _                = succ a * b' + succ a * one := by rw [mul_add]
    _                = succ a * b' + succ a := by rw [mul_one]
    _                = a * b' + b' + succ a := by rw [ih]
    _                = a * b' + succ a + b' := by rw [add_comm_right]
    _                = a * b' + (a + one) + b' := by rw [succ_eq_add_one]
    _                = a * b' + a + one + b' := by simp only [add_assoc]
    _                = a * succ b' + one + b' := by rw [← mul_succ]
    _                = a * succ b' + b' + one := by rw [add_comm_right]
    _                = a * succ b' + (b' + one) := by rw [add_assoc]
    _                = a * succ b' + succ b' := by rw [succ_eq_add_one]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * succ b' = succ a * (b' + one)
Tactic:
rw [succ_eq_add_one b']
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * (b' + one) = succ a * b' + succ a * one
Tactic:
rw [mul_add]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * b' + succ a * one = succ a * b' + succ a
Tactic:
rw [mul_one]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * b' + succ a = a * b' + b' + succ a
Tactic:
rw [ih]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + b' + succ a = a * b' + succ a + b'
Tactic:
rw [add_comm_right]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + succ a + b' = a * b' + (a + one) + b'
Tactic:
rw [succ_eq_add_one]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + (a + one) + b' = a * b' + a + one + b'
Tactic:
simp only [add_assoc]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + a + one + b' = a * succ b' + one + b'
Tactic:
rw [← mul_succ]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * succ b' + one + b' = a * succ b' + b' + one
Tactic:
rw [add_comm_right]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * succ b' + b' + one = a * succ b' + (b' + one)
Tactic:
rw [add_assoc]
State after:
no goals

State before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * succ b' + (b' + one) = a * succ b' + succ b'
Tactic:
rw [succ_eq_add_one]
State after:
no goals