no goals
ι : Type ?u.302627
ι' : Type ?u.302630
α : Type u_1
β : Type ?u.302636
γ : Type ?u.302639
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ a, ∀ (k : α), k ≥ a → ∀ (l : α), l ≥ a → p (k, l)
simp only [eventually_atTop_prod_self, ball_cond_comm]