awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this :
  Eq (α := Set (α × E)) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
    {p : α × E | p.2 ∈ D (f p.1) K}
x x_1 x_2 : ℕ
h : x_2 ≥ x_1
⊢ MeasurableSet (α := α × E)
    (⋂ (i : ℕ), ⋂ (_ : i ≥ x_1), {x_3 : α × E | x_3.2 ∈ B (f x_3.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ i) ((1 / 2) ^ x)})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this :
  Eq (α := Set (α × E)) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
    {p : α × E | p.2 ∈ D (f p.1) K}
x x_1 x_2 : ℕ
h : x_2 ≥ x_1
refine :
  ∀ (x_3 : ℕ),
    MeasurableSet (α := α × E)
      (⋂ (_ : x_3 ≥ x_1), {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ x_3) ((1 / 2) ^ x)})
⊢ MeasurableSet (α := α × E)
    (⋂ (i : ℕ), ⋂ (_ : i ≥ x_1), {x_3 : α × E | x_3.2 ∈ B (f x_3.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ i) ((1 / 2) ^ x)})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this :
  Eq (α := Set (α × E)) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
    {p : α × E | p.2 ∈ D (f p.1) K}
x x_1 x_2 : ℕ
h : x_2 ≥ x_1
x_3 : ℕ
⊢ MeasurableSet (α := α × E)
    (⋂ (_ : x_3 ≥ x_1), {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ x_3) ((1 / 2) ^ x)})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this :
  Eq (α := Set (α × E)) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
    {p : α × E | p.2 ∈ D (f p.1) K}
x x_1 x_2 : ℕ
h : x_2 ≥ x_1
x_3 : ℕ
refine :
  x_3 ≥ x_1 →
    MeasurableSet (α := α × E) {x_5 : α × E | x_5.2 ∈ B (f x_5.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ x_3) ((1 / 2) ^ x)}
⊢ MeasurableSet (α := α × E)
    (⋂ (_ : x_3 ≥ x_1), {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ x_3) ((1 / 2) ^ x)})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this :
  Eq (α := Set (α × E)) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
    {p : α × E | p.2 ∈ D (f p.1) K}
x x_1 x_2 : ℕ
h : x_2 ≥ x_1
x_3 : ℕ
h_1 : x_3 ≥ x_1
⊢ ProperSpace E

Tactic:
have : ProperSpace E := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this_1 :
  Eq (α := Set (α × E)) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
    {p : α × E | p.2 ∈ D (f p.1) K}
x x_1 x_2 : ℕ
h : x_2 ≥ x_1
x_3 : ℕ
h_1 : x_3 ≥ x_1
this : ProperSpace E
⊢ MeasurableSet (α := α × E) {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ x_3) ((1 / 2) ^ x)}

Tactic:
(isOpen_B_with_param hf K).measurableSet

Premises used: IsOpen.measurableSet, FDerivMeasurableAux.isOpen_B_with_param
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this_1 :
  Eq (α := Set (α × E)) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
    {p : α × E | p.2 ∈ D (f p.1) K}
x x_1 x_2 : ℕ
h : x_2 ≥ x_1
x_3 : ℕ
h_1 : x_3 ≥ x_1
this : ProperSpace E
⊢ MeasurableSet (α := α × E) {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ x_3) ((1 / 2) ^ x)}

Tactic:
exact (isOpen_B_with_param hf K).measurableSet

Premises used: IsOpen.measurableSet, FDerivMeasurableAux.isOpen_B_with_param
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ IsComplete (α := E →L[𝕜] F) univ

Tactic:
have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : IsComplete (α := E →L[𝕜] F) univ
⊢ MeasurableSet (α := α × E)
    {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ Membership.mem (γ := Set (E →L[𝕜] F)) univ (fderiv 𝕜 (f p.1) p.2)}

Tactic:
measurableSet_of_differentiableAt_of_isComplete_with_param hf this

Premises used: measurableSet_of_differentiableAt_of_isComplete_with_param
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : IsComplete (α := E →L[𝕜] F) univ
h :
  ∀ (x : α × E),
    DifferentiableAt 𝕜 (f x.1) x.2 ↔
      DifferentiableAt 𝕜 (f x.1) x.2 ∧ Membership.mem (γ := Set (E →L[𝕜] F)) univ (fderiv 𝕜 (f x.1) x.2)
⊢ MeasurableSet (α := α × E) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2}

Tactic:
convert! measurableSet_of_differentiableAt_of_isComplete_with_param hf this

Premises used: measurableSet_of_differentiableAt_of_isComplete_with_param
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : IsComplete (α := E →L[𝕜] F) univ
x : α × E
⊢ DifferentiableAt 𝕜 (f x.1) x.2 ↔
    DifferentiableAt 𝕜 (f x.1) x.2 ∧ Membership.mem (γ := Set (E →L[𝕜] F)) univ (fderiv 𝕜 (f x.1) x.2)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ Measurable (β := E →L[𝕜] F) fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2

Tactic:
measurable_of_isClosed (fun s hs ↦ ?_)

Premises used: measurable_of_isClosed
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
refine :
  ∀ (s : Set (E →L[𝕜] F)) (hs : IsClosed s), MeasurableSet (α := α × E) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
⊢ Measurable (β := E →L[𝕜] F) fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2

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

Premises used: measurable_of_isClosed
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
s : Set (E →L[𝕜] F)
hs : IsClosed s
⊢ Eq (α := Set (α × E)) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
    ({p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p : α × E | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p : α × E | 0 ∈ 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)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  Eq (α := Set (α × E)) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
    ({p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p : α × E | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p : α × E | 0 ∈ s})
rw :
  MeasurableSet (α := α × E)
    ({p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p : α × E | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p : α × E | 0 ∈ s})
⊢ MeasurableSet (α := α × E) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  Eq (α := Set (α × E)) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
    ({p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p : α × E | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p : α × E | 0 ∈ s})
⊢ MeasurableSet (α := α × E)
    ({p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p : α × E | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p : α × E | 0 ∈ s})

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

Premises used: setOf, MeasurableSet.compl, MeasurableSet.const, MeasurableSet.union, measurableSet_of_differentiableAt_of_isComplete_with_param, IsClosed.isComplete, measurableSet_of_differentiableAt_with_param, MeasurableSet.inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  Eq (α := Set (α × E)) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
    ({p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p : α × E | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p : α × E | 0 ∈ s})
⊢ MeasurableSet (α := α × E)
    ({p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p : α × E | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p : α × E | 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 _))

Premises used: MeasurableSet.compl, MeasurableSet.const, MeasurableSet.union, measurableSet_of_differentiableAt_of_isComplete_with_param, IsClosed.isComplete, measurableSet_of_differentiableAt_with_param, MeasurableSet.inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
inst_7 : MeasurableSpace α
inst_8 : OpensMeasurableSpace α
inst_9 : MeasurableSpace E
inst_10 : OpensMeasurableSpace E
inst_11 : CompleteSpace F
inst_12 : MeasurableSpace F
inst_13 : BorelSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
y : E
⊢ Measurable (β := F) fun (p : α × E) ↦ (fderiv 𝕜 (f p.1) p.2 : (a : E) → F) y

Tactic:
(ContinuousLinearMap.measurable_apply y).comp (measurable_fderiv_with_param 𝕜 hf)

Premises used: Measurable.comp, ContinuousLinearMap.measurable_apply, measurable_fderiv_with_param
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ Measurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2

Tactic:
simpa only [fderiv_apply_one_eq_deriv] using measurable_fderiv_apply_const_with_param 𝕜 hf 1

Premises used: fderiv_apply_one_eq_deriv, OfNat.ofNat, measurable_fderiv_apply_const_with_param
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ let this := borel F;
  BorelSpace F

Tactic:
borelize F
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
inl : ∀ (hα : SecondCountableTopology α), StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
inr : ∀ (hF : SecondCountableTopology F), StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2

Tactic:
rcases h.out with hα | hF

Premises used: SecondCountableTopologyEither.out
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
hα : SecondCountableTopology α
⊢ ProperSpace 𝕜

Tactic:
have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
apply : IsSeparable.{u_3} (α := F) (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2

Tactic:
apply stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_deriv_with_param hf, ?_⟩

Premises used: Iff.mpr, measurable_deriv_with_param, stronglyMeasurable_iff_measurable_separable, And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
rw :
  deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f p.1 '' univ)) : Set F)
⊢ deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ