no goals
F : Type ?u.408308
α : Type u_1
β : Type ?u.408314
γ : Type ?u.408317
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
simp [← mem_coe, coe_pow, Set.mem_pow]