-- Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean
theorem measurableSet_lineDifferentiableAt (hf : Continuous f) :
    MeasurableSet {x : E | LineDifferentiableAt 𝕜 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
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E → 𝕜 → F := fun x t => f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ MeasurableSet {x | LineDifferentiableAt 𝕜 f x v}

Tactic:
exact measurable_prod_mk_right (measurableSet_of_differentiableAt_with_param 𝕜 hg)

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