Theorem: exp_assoc (meetings/ex6.lean)

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

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

case hs

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

State before:
case hz

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

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

State before:
case hs

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

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

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