no goals
α : Type u_1
β : Type ?u.107971
γ : Type ?u.107974
δ : Type ?u.107977
ι : Type ?u.107980
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
⊢ s =ᵐ[μ] t ↔ ↑↑μ (s \ t) = 0 ∧ ↑↑μ (t \ s) = 0
simp [eventuallyLE_antisymm_iff, ae_le_set]