no goals
α : Type u_2
β : Type u_1
γ : Type ?u.178625
δ : Type ?u.178628
ι : Type ?u.178631
R : Type ?u.178634
R' : Type ?u.178637
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : α → β
⊢ map f 0 = 0
by_cases hf : AEMeasurable f (0 : Measure α) <;> simp [map, hf]