no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.349637
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ comp g hg f = mk (g ∘ ↑f) (_ : AEStronglyMeasurable (fun x => g (↑f x)) μ)
rw [← comp_mk g hg f f.aestronglyMeasurable, mk_coeFn]