no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.445345
inst✝¹⁰ : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : TopologicalSpace γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : BorelSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : PseudoMetrizableSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : MeasurableSpace γ
inst✝ : OpensMeasurableSpace γ
g : β → γ
hg : Measurable g
f✝ : α →ₘ[μ] β
f : α → β
x✝ : AEStronglyMeasurable f μ
⊢ toGerm (compMeasurable g hg (mk f x✝)) = Germ.map g (toGerm (mk f x✝))
simp