no goals
α : Type u_2
β : Type u_1
γ : Type ?u.53677
δ : Type ?u.53680
ι : Sort ?u.53683
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ Filter.coprod f g ↔ (∃ t₁, t₁ ∈ f ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, t₂ ∈ g ∧ Prod.snd ⁻¹' t₂ ⊆ s
simp [Filter.coprod]