ι : Type ?u.304213
ι' : Type ?u.304216
α : Type u_1
β : Type u_2
γ : Type ?u.304225
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
ι : Type ?u.304213
ι' : Type ?u.304216
α : Type u_1
β : Type u_2
γ : Type ?u.304225
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
rw [← prod_atTop_atTop_eq] at hp
no goals
ι : Type ?u.304213
ι' : Type ?u.304216
α : Type u_1
β : Type u_2
γ : Type ?u.304225
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
exact hp.curry