no goals
α : Type u_1
β : Type ?u.137021
γ : Type ?u.137024
δ : Type ?u.137027
ι : Type ?u.137030
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
H : s ≤ᵐ[μ] t
⊢ ↑↑μ (s ∪ t) = ↑↑μ (t ∪ s \ t)
rw [union_diff_self, Set.union_comm]
no goals
α : Type u_1
β : Type ?u.137021
γ : Type ?u.137024
δ : Type ?u.137027
ι : Type ?u.137030
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
H : s ≤ᵐ[μ] t
⊢ ↑↑μ t + ↑↑μ (s \ t) = ↑↑μ t
rw [ae_le_set.1 H, add_zero]