α : Type u_1
β : Type u_2
γ : Type ?u.4998
δ : Type ?u.5001
ι : Sort ?u.5004
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
⊢ Filter.prod f ⊤ = comap Prod.fst f
α : Type u_1
β : Type u_2
γ : Type ?u.4998
δ : Type ?u.5001
ι : Sort ?u.5004
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
⊢ f ×ˢ ⊤ = comap Prod.fst f
dsimp only [SProd.sprod]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4998
δ : Type ?u.5001
ι : Sort ?u.5004
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
⊢ Filter.prod f ⊤ = comap Prod.fst f
rw [Filter.prod, comap_top, inf_top_eq]