-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurableSet_of_differentiableAt_with_param (hf : Continuous f.uncurry) :
    MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2}

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : LocallyCompactSpace E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁵ : TopologicalSpace α
f : α → E → F
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous (Function.uncurry f)
this : IsComplete univ
⊢ MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2}

Tactic:
convert measurableSet_of_differentiableAt_of_isComplete_with_param hf this

Result:
case h.e'_3.h.e'_2.h.a
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : LocallyCompactSpace E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁵ : TopologicalSpace α
f : α → E → F
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous (Function.uncurry f)
this : IsComplete univ
x✝ : α × E
⊢ DifferentiableAt 𝕜 (f x✝.1) x✝.2 ↔ DifferentiableAt 𝕜 (f x✝.1) x✝.2 ∧ fderiv 𝕜 (f x✝.1) x✝.2 ∈ univ

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : LocallyCompactSpace E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁵ : TopologicalSpace α
f : α → E → F
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous (Function.uncurry f)
⊢ MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2}

Tactic:
have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : LocallyCompactSpace E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁵ : TopologicalSpace α
f : α → E → F
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous (Function.uncurry f)
this : IsComplete univ
⊢ MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2}

Proof state:
case h.e'_3.h.e'_2.h.a
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : LocallyCompactSpace E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁵ : TopologicalSpace α
f : α → E → F
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous (Function.uncurry f)
this : IsComplete univ
x✝ : α × E
⊢ DifferentiableAt 𝕜 (f x✝.1) x✝.2 ↔ DifferentiableAt 𝕜 (f x✝.1) x✝.2 ∧ fderiv 𝕜 (f x✝.1) x✝.2 ∈ univ

Tactic:
simp

Result:
no goals