ι : Type u_1
α : Type u_2
β : Type ?u.59011
F : Type ?u.59014
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ (∃ g x, ∏ i : ι, g i = a) ↔ ∃ g x, ∏ i : ι, g i = a
ι : Type u_1
α : Type u_2
β : Type ?u.59011
F : Type ?u.59014
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i : ι, f i ↔ ∃ g x, ∏ i : ι, g i = a
rw [mem_finset_prod]
no goals
ι : Type u_1
α : Type u_2
β : Type ?u.59011
F : Type ?u.59014
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ (∃ g x, ∏ i : ι, g i = a) ↔ ∃ g x, ∏ i : ι, g i = a
simp