F : Type ?u.406111
α : Type u_1
β : Type ?u.406117
γ : Type ?u.406120
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a✝ : α
m n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
F : Type ?u.406111
α : Type u_1
β : Type ?u.406117
γ : Type ?u.406120
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a✝ : α
m n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
no goals
F : Type ?u.406111
α : Type u_1
β : Type ?u.406117
γ : Type ?u.406120
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a✝ : α
m n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
rfl