no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.206109
ι : Sort x
inst✝ : PartialOrder β
l : Filter α
f g : α → β
⊢ f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f
simp only [EventuallyEq, EventuallyLE, le_antisymm_iff, eventually_and]