no goals
α : Type u_1
β : Type u_2
γ : Type ?u.329647
δ : Type ?u.329650
ι : Type ?u.329653
R : Type ?u.329656
R' : Type ?u.329659
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f (dirac a)) s = ↑↑(dirac (f a)) s
simp [hs, map_apply hf hs, hf hs, indicator_apply]