-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurable_fderiv_with_param (hf : Continuous f.uncurry) :
    Measurable (fun (p : α × E) ↦ fderiv 𝕜 (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)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  (fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}
⊢ MeasurableSet
    ({p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s})

Tactic:
exact
  (measurableSet_of_differentiableAt_of_isComplete_with_param hf hs.isComplete).union
    ((measurableSet_of_differentiableAt_with_param _ hf).compl.inter (MeasurableSet.const _))

Result:
no goals

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)
⊢ Measurable fun p => fderiv 𝕜 (f p.1) p.2

Tactic:
refine measurable_of_isClosed (fun s hs ↦ ?_)

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)
s : Set (E →L[𝕜] F)
hs : IsClosed s
⊢ MeasurableSet ((fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s)

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)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  (fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}
⊢ MeasurableSet ((fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s)

Tactic:
rw [this]

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)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  (fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}
⊢ MeasurableSet
    ({p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s})

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)
s : Set (E →L[𝕜] F)
hs : IsClosed s
⊢ MeasurableSet ((fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s)

Tactic:
have :
  (fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s } ∪
      { p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ { _p | (0 : E →L[𝕜] F) ∈ s} :=
  Set.ext (fun x ↦ mem_preimage.trans fderiv_mem_iff)

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)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  (fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}
⊢ MeasurableSet ((fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s)