α : Type u_1
β : Type u_2
γ : Type ?u.43185
δ : Type ?u.43188
ι : Sort ?u.43191
s✝ : Set α
t✝ : Set β
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = prod s t
α : Type u_1
β : Type u_2
γ : Type ?u.43185
δ : Type ?u.43188
ι : Sort ?u.43191
s✝ : Set α
t✝ : Set β
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)
simp only [SProd.sprod, Filter.prod, comap_principal, principal_eq_iff_eq, comap_principal,
  inf_principal]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.43185
δ : Type ?u.43188
ι : Sort ?u.43191
s✝ : Set α
t✝ : Set β
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = prod s t
rfl