Theorem: mul_assoc' (meetings/ex6.lean)

State before:
⊢ ∀ (c a b : ↑N0), mul (mul (a, b), c) = mul (a, mul (b, c))
Tactic:
apply generic_recursor
State after:
case hz

⊢ ∀ (a b : ↑N0), mul (mul (a, b), z) = mul (a, mul (b, z))

case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), mul (mul (a, b), n) = mul (a, mul (b, n))) →
      ∀ (a b : ↑N0), mul (mul (a, b), S n) = mul (a, mul (b, S n))

State before:
case hz

⊢ ∀ (a b : ↑N0), mul (mul (a, b), z) = mul (a, mul (b, z))
Tactic:
intro a b
State after:
case hz
a b : ↑N0
⊢ mul (mul (a, b), z) = mul (a, mul (b, z))

State before:
case hz
a b : ↑N0
⊢ mul (mul (a, b), z) = mul (a, mul (b, z))
Tactic:
rw [zmul, zmul, zmul]
State after:
no goals

State before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), mul (mul (a, b), n) = mul (a, mul (b, n))) →
      ∀ (a b : ↑N0), mul (mul (a, b), S n) = mul (a, mul (b, S n))
Tactic:
intro c hi a b
State after:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), mul (mul (a, b), c) = mul (a, mul (b, c))
a b : ↑N0
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))

State before:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), mul (mul (a, b), c) = mul (a, mul (b, c))
a b : ↑N0
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))
Tactic:
specialize hi a b
State after:
case hs
c a b : ↑N0
hi : mul (mul (a, b), c) = mul (a, mul (b, c))
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))

State before:
case hs
c a b : ↑N0
hi : mul (mul (a, b), c) = mul (a, mul (b, c))
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))
Tactic:
rw [smul, smul, hi, mul_distrib_add]
State after:
no goals