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