Theorem: mul_distrib_add (meetings/ex6.lean)

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

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

case hs

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

State before:
case hz

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

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

State before:
case hs

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

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

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