Theorem: exp_distrib_mul (meetings/ex6.lean)

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

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

case hs

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

State before:
case hz

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

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

State before:
case hs

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

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

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