-- Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean
theorem stronglyMeasurable_lineDeriv [SecondCountableTopologyEither E F] (hf : Continuous f) :
    StronglyMeasurable (fun x ↦ lineDeriv 𝕜 f x v)

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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
⊢ StronglyMeasurable fun x => lineDeriv 𝕜 f x v

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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
⊢ StronglyMeasurable fun x => lineDeriv 𝕜 f x v

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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
⊢ StronglyMeasurable fun x => lineDeriv 𝕜 f x v

Tactic:
let g : E → 𝕜 → F := fun x t ↦ f (x + t • v)

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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E → 𝕜 → F := fun x t => f (x + t • v)
⊢ StronglyMeasurable fun x => lineDeriv 𝕜 f x v

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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E → 𝕜 → F := fun x t => f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ StronglyMeasurable fun x => lineDeriv 𝕜 f x v

Tactic:
exact (stronglyMeasurable_deriv_with_param hg).comp_measurable 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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E → 𝕜 → F := fun x t => f (x + t • v)
⊢ Continuous (Function.uncurry g)

Tactic:
fun_prop

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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E → 𝕜 → F := fun x t => f (x + t • v)
⊢ StronglyMeasurable fun x => lineDeriv 𝕜 f x v

Tactic:
have hg : Continuous g.uncurry := by fun_prop

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
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E → 𝕜 → F := fun x t => f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ StronglyMeasurable fun x => lineDeriv 𝕜 f x v