α : 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₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) (_ : AEStronglyMeasurable (fun x => uncurry g (↑f₁ x, ↑f₂ x)) μ) =
    mk (fun a => g (↑f₁ a) (↑f₂ a)) (_ : AEStronglyMeasurable (fun x => uncurry g (↑f₁ x, ↑f₂ x)) μ)
α : 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₂ : α →ₘ[μ] γ
⊢ comp₂ g hg f₁ f₂ = mk (fun a => g (↑f₁ a) (↑f₂ a)) (_ : AEStronglyMeasurable (fun x => uncurry g (↑f₁ x, ↑f₂ x)) μ)
rw [comp₂_eq_pair, pair_eq_mk, comp_mk]
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₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) (_ : AEStronglyMeasurable (fun x => uncurry g (↑f₁ x, ↑f₂ x)) μ) =
    mk (fun a => g (↑f₁ a) (↑f₂ a)) (_ : AEStronglyMeasurable (fun x => uncurry g (↑f₁ x, ↑f₂ x)) μ)
rfl