-- Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean
theorem measurable_lineDeriv_uncurry [MeasurableSpace F] [BorelSpace F]
    (hf : Continuous f) : Measurable (fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2)

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
⊢ Measurable fun p => lineDeriv 𝕜 f p.1 p.2

Tactic:
borelize 𝕜

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
⊢ Measurable fun p => lineDeriv 𝕜 f p.1 p.2

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ Measurable fun p => lineDeriv 𝕜 f p.1 p.2

Tactic:
exact (measurable_deriv_with_param this).comp measurable_prod_mk_right

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
⊢ Measurable fun p => lineDeriv 𝕜 f p.1 p.2

Tactic:
let g : (E × E) → 𝕜 → F := fun p t ↦ f (p.1 + t • p.2)

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)
⊢ Measurable fun p => lineDeriv 𝕜 f p.1 p.2

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)
⊢ Measurable fun p => lineDeriv 𝕜 f p.1 p.2

Tactic:
have : Continuous g.uncurry :=
  hf.comp <| (continuous_fst.comp continuous_fst).add
  <| continuous_snd.smul (continuous_snd.comp continuous_fst)

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ Measurable fun p => lineDeriv 𝕜 f p.1 p.2