case zero
α : Type ?u.15094
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m : ℕ
⊢ a ^ (m * Nat.zero) = (a ^ m) ^ Nat.zero

case succ
α : Type ?u.15094
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
ih : a ^ (m * n) = (a ^ m) ^ n
⊢ a ^ (m * Nat.succ n) = (a ^ m) ^ Nat.succ n
α : Type ?u.15094
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
⊢ a ^ (m * n) = (a ^ m) ^ n
induction' n with n ih
no goals
case zero
α : Type ?u.15094
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m : ℕ
⊢ a ^ (m * Nat.zero) = (a ^ m) ^ Nat.zero
rw [Nat.mul_zero, pow_zero, pow_zero]
no goals
case succ
α : Type ?u.15094
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
ih : a ^ (m * n) = (a ^ m) ^ n
⊢ a ^ (m * Nat.succ n) = (a ^ m) ^ Nat.succ n
rw [Nat.mul_succ, pow_add, pow_succ', ih]