α : Type u_1
β : Type u_2
γ : Type ?u.5866
δ : Type ?u.5869
ι : Sort ?u.5872
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ Filter.prod f (g₁ ⊔ g₂) = Filter.prod f g₁ ⊔ Filter.prod f g₂
α : Type u_1
β : Type u_2
γ : Type ?u.5866
δ : Type ?u.5869
ι : Sort ?u.5872
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂
dsimp only [SProd.sprod]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.5866
δ : Type ?u.5869
ι : Sort ?u.5872
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ Filter.prod f (g₁ ⊔ g₂) = Filter.prod f g₁ ⊔ Filter.prod f g₂
rw [Filter.prod, comap_sup, inf_sup_left, ← Filter.prod, ← Filter.prod]