no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.389331
inst✝¹⁰ : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : TopologicalSpace γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ compMeasurable g hg f = mk (g ∘ ↑f) (_ : AEStronglyMeasurable (g ∘ ↑f) μ)
rw [← compMeasurable_mk g hg f f.aestronglyMeasurable, mk_coeFn]