no goals
α : Type u_1
β : Type u_2
γ : Type ?u.177408
δ : Type ?u.177411
ι : Type ?u.177414
R : Type ?u.177417
R' : Type ?u.177420
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
f : α → β
hf : Measurable f
⊢ map f (μ + ν) = map f μ + map f ν
simp [← mapₗ_apply_of_measurable hf]