no goals
α : Type u_1
β : Type ?u.106226
γ : Type ?u.106229
δ : Type ?u.106232
ι : Type ?u.106235
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s \ t =ᵐ[μ] s ↔ ↑↑μ (s ∩ t) = 0
simp [eventuallyLE_antisymm_iff, ae_le_set, diff_diff_right, diff_diff,
  diff_eq_empty.2 (Set.subset_union_right _ _)]