no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.444612
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
hg : Continuous g
f✝ : α →ₘ[μ] β
f : α → β
x✝ : AEStronglyMeasurable f μ
⊢ toGerm (comp g hg (mk f x✝)) = Germ.map g (toGerm (mk f x✝))
simp