M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.30867
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
⊢ 1 ∈ s
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.30867
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
⊢ a ^ 0 ∈ s
rw [pow_zero]
no goals
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.30867
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
⊢ 1 ∈ s
exact hs.one_mem
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.30867
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.30867
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
n : ℕ
⊢ a ^ (n + 1) ∈ s
rw [pow_succ]
no goals
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.30867
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s
exact hs.mul_mem h (IsSubmonoid.pow_mem hs h)