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