no goals
α : Type u_2
β : Type ?u.400038
γ : Type ?u.400041
δ : Type ?u.400044
ι : Type ?u.400047
R : Type u_1
R' : Type ?u.400053
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : Monoid R
inst✝¹ : DistribMulAction R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : ↑↑ν s = 0
⊢ ↑↑(c • μ) s = 0
simp only [h hνs, smul_eq_mul, smul_apply, smul_zero]