case zero
α : Type ?u.41048
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 : a * b = 1
⊢ a ^ Nat.zero * b ^ Nat.zero = 1

case succ
α : Type ?u.41048
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 : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ Nat.succ n * b ^ Nat.succ n = 1
α : Type ?u.41048
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
n : ℕ
h : a * b = 1
⊢ a ^ n * b ^ n = 1
induction' n with n hn
no goals
case zero
α : Type ?u.41048
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 : a * b = 1
⊢ a ^ Nat.zero * b ^ Nat.zero = 1
simp
no goals
case succ
α : Type ?u.41048
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 : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ Nat.succ n * b ^ Nat.succ n = 1
calc
  a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n) := by rw [pow_succ', pow_succ]
  _ = a ^ n * (a * b) * b ^ n := by simp only [mul_assoc]
  _ = 1 := by simp [h, hn]
no goals
α : Type ?u.41048
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 : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ Nat.succ n * b ^ Nat.succ n = a ^ n * a * (b * b ^ n)
rw [pow_succ', pow_succ]
no goals
α : Type ?u.41048
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 : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ n * a * (b * b ^ n) = a ^ n * (a * b) * b ^ n
simp only [mul_assoc]
no goals
α : Type ?u.41048
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 : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ n * (a * b) * b ^ n = 1
simp [h, hn]