no goals
ι : Type ?u.301355
ι' : Type ?u.301358
α : Type u_1
β : Type ?u.301364
γ : Type ?u.301367
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k : α), k ≤ a → ∀ (l : α), l ≤ a → p (k, l)
simp only [eventually_atBot_prod_self, ball_cond_comm]