no goals
α : Type u_2
β : Type ?u.579678
γ : Type ?u.579681
δ : Type ?u.579684
ι : Type ?u.579687
R : Type u_1
R' : Type ?u.579693
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
inst✝² : Monoid R
inst✝¹ : DistribMulAction R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
⊢ ↑↑(c • μ) {a | ¬p a} = 0
rw [smul_apply, ae_iff.1 h, smul_zero]