-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurableSet_of_differentiableAt_of_isComplete_with_param
    (hf : Continuous f.uncurry) {K : Set (E →L[𝕜] F)} (hK : IsComplete K) :
    MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
x✝ : ℕ
⊢ MeasurableSet
    (⋃ i,
      ⋂ i_1,
        ⋂ (_ : i_1 ≥ i), ⋂ i_2, ⋂ (_ : i_2 ≥ i), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_1) ((1 / 2) ^ i_2) ((1 / 2) ^ x✝)})

Tactic:
refine MeasurableSet.iUnion (fun _ ↦ ?_)

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
x✝¹ x✝ : ℕ
⊢ MeasurableSet
    (⋂ i,
      ⋂ (_ : i ≥ x✝), ⋂ i_1, ⋂ (_ : i_1 ≥ x✝), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i) ((1 / 2) ^ i_1) ((1 / 2) ^ x✝¹)})

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet
    {p | ∀ (i : ℕ), ∃ i_1, ∀ i_2 ≥ i_1, ∀ i_4 ≥ i_1, p.2 ∈ B (f p.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_4) ((1 / 2) ^ i)}

Tactic:
simp only [setOf_forall, setOf_exists]

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet
    (⋂ i,
      ⋃ i_1,
        ⋂ i_2,
          ⋂ (_ : i_2 ≥ i_1),
            ⋂ i_3, ⋂ (_ : i_3 ≥ i_1), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_3) ((1 / 2) ^ i)})

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
x✝⁵ x✝⁴ x✝³ : ℕ
x✝² : x✝³ ≥ x✝⁴
x✝¹ : ℕ
x✝ : x✝¹ ≥ x✝⁴
⊢ MeasurableSet {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝³) ((1 / 2) ^ x✝¹) ((1 / 2) ^ x✝⁵)}

Tactic:
have : ProperSpace E := .of_locallyCompactSpace 𝕜

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this✝ : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
x✝⁵ x✝⁴ x✝³ : ℕ
x✝² : x✝³ ≥ x✝⁴
x✝¹ : ℕ
x✝ : x✝¹ ≥ x✝⁴
this : ProperSpace E
⊢ MeasurableSet {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝³) ((1 / 2) ^ x✝¹) ((1 / 2) ^ x✝⁵)}

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet
    (⋂ i,
      ⋃ i_1,
        ⋂ i_2,
          ⋂ (_ : i_2 ≥ i_1),
            ⋂ i_3, ⋂ (_ : i_3 ≥ i_1), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_3) ((1 / 2) ^ i)})

Tactic:
refine MeasurableSet.iInter (fun _ ↦ ?_)

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
x✝ : ℕ
⊢ MeasurableSet
    (⋃ i,
      ⋂ i_1,
        ⋂ (_ : i_1 ≥ i), ⋂ i_2, ⋂ (_ : i_2 ≥ i), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_1) ((1 / 2) ^ i_2) ((1 / 2) ^ x✝)})

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}

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
hf : Continuous (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet {p | p.2 ∈ D (f p.1) K}