no goals
α : Type u_1
β : Type ?u.105395
γ : Type ?u.105398
δ : Type ?u.105401
ι : Type ?u.105404
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s ∪ t =ᵐ[μ] t ↔ ↑↑μ (s \ t) = 0
simp [eventuallyLE_antisymm_iff, ae_le_set, union_diff_right,
  diff_eq_empty.2 (Set.subset_union_right _ _)]