case zero
α : Type ?u.13242
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 * a ^ Nat.zero

case succ
α : Type ?u.13242
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 * a ^ n
⊢ a ^ (m + Nat.succ n) = a ^ m * a ^ Nat.succ n
α : Type ?u.13242
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 * a ^ n
induction' n with n ih
no goals
case zero
α : Type ?u.13242
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 * a ^ Nat.zero
rw [Nat.add_zero, pow_zero, mul_one]
no goals
case succ
α : Type ?u.13242
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 * a ^ n
⊢ a ^ (m + Nat.succ n) = a ^ m * a ^ Nat.succ n
rw [pow_succ', ← mul_assoc, ← ih, ← pow_succ', Nat.add_assoc]