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