no goals
F : Type ?u.11956
α : Type u_1
β : Type ?u.11962
γ : Type ?u.11965
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]