no goals
ι : Type ?u.290998
ι' : Type ?u.291001
α : Type u_1
β : Type ?u.291007
γ : Type ?u.291010
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]