F : Type ?u.259960
α : Type u_1
β : Type ?u.259966
γ : Type ?u.259969
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
ha : a ∈ s
⊢ 1 ∈ s ^ 0
F : Type ?u.259960
α : Type u_1
β : Type ?u.259966
γ : Type ?u.259969
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
ha : a ∈ s
⊢ a ^ 0 ∈ s ^ 0
rw [pow_zero]
no goals
F : Type ?u.259960
α : Type u_1
β : Type ?u.259966
γ : Type ?u.259969
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
ha : a ∈ s
⊢ 1 ∈ s ^ 0
exact one_mem_one
F : Type ?u.259960
α : Type u_1
β : Type ?u.259966
γ : Type ?u.259969
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s ^ (n + 1)
F : Type ?u.259960
α : Type u_1
β : Type ?u.259966
γ : Type ?u.259969
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a ^ (n + 1) ∈ s ^ (n + 1)
rw [pow_succ]
no goals
F : Type ?u.259960
α : Type u_1
β : Type ?u.259966
γ : Type ?u.259969
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s ^ (n + 1)
exact mul_mem_mul ha (pow_mem_pow ha n)