no goals
α : Type u_1
β : Type ?u.31164
γ : Type ?u.31167
δ : Type ?u.31170
ι : Type ?u.31173
R : Type ?u.31176
R' : Type ?u.31179
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s ∪ t =ᵐ[μ] t ↔ s ≤ᵐ[μ] t
rw [union_comm, union_ae_eq_left_iff_ae_subset]