case zero
α : Type ?u.18278
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 b : M
h : Commute a b
⊢ (a * b) ^ Nat.zero = a ^ Nat.zero * b ^ Nat.zero

case succ
α : Type ?u.18278
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 b : M
h : Commute a b
n : ℕ
ih : (a * b) ^ n = a ^ n * b ^ n
⊢ (a * b) ^ Nat.succ n = a ^ Nat.succ n * b ^ Nat.succ n
α : Type ?u.18278
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 b : M
h : Commute a b
n : ℕ
⊢ (a * b) ^ n = a ^ n * b ^ n
induction' n with n ih
no goals
case zero
α : Type ?u.18278
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 b : M
h : Commute a b
⊢ (a * b) ^ Nat.zero = a ^ Nat.zero * b ^ Nat.zero
rw [pow_zero, pow_zero, pow_zero, one_mul]
no goals
case succ
α : Type ?u.18278
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 b : M
h : Commute a b
n : ℕ
ih : (a * b) ^ n = a ^ n * b ^ n
⊢ (a * b) ^ Nat.succ n = a ^ Nat.succ n * b ^ Nat.succ n
simp only [pow_succ, ih, ← mul_assoc, (h.pow_left n).right_comm]