no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.392686
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ pair f g = mk (fun x => (↑f x, ↑g x)) (_ : AEStronglyMeasurable (fun x => (↑f x, ↑g x)) μ)
simp only [← pair_mk_mk, mk_coeFn, f.aestronglyMeasurable, g.aestronglyMeasurable]