∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ]
  [inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : MeasurableSpace β] [inst_6 : BorelSpace β]
  [inst_7 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_8 : SecondCountableTopologyEither β γ]
  [inst_9 : MeasurableSpace γ] [inst_10 : BorelSpace γ] [inst_11 : TopologicalSpace.PseudoMetrizableSpace δ]
  [inst_12 : SecondCountableTopology δ] [inst_13 : MeasurableSpace δ] [inst_14 : OpensMeasurableSpace δ] (g : β → γ → δ)
  (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ),
  (MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm