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

case succ
α : Type ?u.9841
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
n : ℕ
ih : 1 ^ n = 1
⊢ 1 ^ Nat.succ n = 1
α : Type ?u.9841
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
n : ℕ
⊢ 1 ^ n = 1
induction' n with n ih
no goals
case zero
α : Type ?u.9841
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
⊢ 1 ^ Nat.zero = 1
exact pow_zero _
no goals
case succ
α : Type ?u.9841
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
n : ℕ
ih : 1 ^ n = 1
⊢ 1 ^ Nat.succ n = 1
rw [pow_succ, ih, one_mul]