Theorem: exp_add_eq_mul_exp_exp (meetings/ex6.lean)

State before:
⊢ ∀ (r m n : ↑N0), exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
Tactic:
apply generic_recursor
State after:
case hz

⊢ ∀ (m n : ↑N0), exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))

case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (m, plus (n_1, n)) = mul (exp (m, n_1), exp (m, n))) →
      ∀ (m n_1 : ↑N0), exp (m, plus (n_1, S n)) = mul (exp (m, n_1), exp (m, S n))

State before:
case hz

⊢ ∀ (m n : ↑N0), exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))
Tactic:
intros m n
State after:
case hz
m n : ↑N0
⊢ exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))

State before:
case hz
m n : ↑N0
⊢ exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))
Tactic:
rw [zplus, zexp, smul, zmul, zero_plus_x_eq_eq]
State after:
no goals

State before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (m, plus (n_1, n)) = mul (exp (m, n_1), exp (m, n))) →
      ∀ (m n_1 : ↑N0), exp (m, plus (n_1, S n)) = mul (exp (m, n_1), exp (m, S n))
Tactic:
intros r hi m n
State after:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
m n : ↑N0
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))

State before:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
m n : ↑N0
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))
Tactic:
specialize hi m n
State after:
case hs
r m n : ↑N0
hi : exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))

State before:
case hs
r m n : ↑N0
hi : exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))
Tactic:
rw [splus, sexp, sexp, hi, mul_assoc']
State after:
no goals