awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
a'₁ :
  ‖f a' z - f a' y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ =
    ‖f a' z - f a z + (f a y - f a' y) +
        (f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F))‖
a'₂ :
  ‖f a' z - f a z‖ + ‖f a y - f a' y‖ +
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤
    ε + ε + b
⊢ ‖f (a', x').1 z - f (a', x').1 y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
    s * r
have a'₃ : ε + ε + b < s * r
Tactic: calc
  ‖f a' z - f a' y - (L z - L y)‖ =
    ‖(f a' z - f a z) + (f a y - f a' y) + (f a z - f a y - (L z - L y))‖ := by congr; abel
  _ ≤ ‖f a' z - f a z‖ + ‖f a y - f a' y‖ + ‖f a z - f a y - (L z - L y)‖ := norm_add₃_le
  _ ≤ ε + ε + b := by
      gcongr
      · rw [← dist_eq_norm]
        change dist (f.uncurry (a', z)) (f.uncurry (a, z)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dzx]
      · rw [← dist_eq_norm']
        change dist (f.uncurry (a', y)) (f.uncurry (a, y)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dyx]
      · simp [hb, dyx, dzx]
  _ < s * r := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
⊢ IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ B (f p.1) K r s t}
have h : Eq (α := Set (α × E)) {p : α × E | p.2 ∈ B (f p.1) K r s t}
  (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
Tactic: convert! H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
⊢ Eq (α := Set (α × E)) {p : α × E | p.2 ∈ B (f p.1) K r s t}
    (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
have h : ∀ (p : α × E),
  Membership.mem (γ := Set (α × E)) {p : α × E | p.2 ∈ B (f p.1) K r s t} p ↔
    Membership.mem (γ := Set (α × E)) (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
⊢ IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ B (f p.1) K r s t}
have suffices : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
Tactic: suffices H : IsOpen (⋃ L ∈ K,
      {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}) by
    convert! H; ext p; simp [B]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
⊢ IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
have refine : ∀ L ∈ K, IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}
Tactic: refine isOpen_biUnion (fun L _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ MeasurableSet (α := α × E) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
have 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}
Tactic: have : {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
          = {p : α × E | p.2 ∈ D (f p.1) K} := by simp [← differentiable_set_eq_D K hK]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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}
⊢ MeasurableSet (α := α × E) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
have rw : MeasurableSet (α := α × E) {p : α × E | p.2 ∈ D (f p.1) K}
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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}
⊢ MeasurableSet (α := α × E) {p : α × E | p.2 ∈ D (f p.1) K}
have simp : MeasurableSet (α := α × E)
  {p : α × E |
    ∀ (i : ℕ),
      ∃ (i_1 : ℕ),
        ∀ (i_2 : ℕ) (i_3 : i_2 ≥ i_1) (i_4 : ℕ) (i_5 : 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 [D, mem_iInter, mem_iUnion]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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}
⊢ MeasurableSet (α := α × E)
    {p : α × E |
      ∀ (i : ℕ),
        ∃ (i_1 : ℕ),
          ∀ (i_2 : ℕ) (i_3 : i_2 ≥ i_1) (i_4 : ℕ) (i_5 : i_4 ≥ i_1),
            p.2 ∈ B (f p.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_4) ((1 / 2) ^ i)}
have simp : MeasurableSet (α := α × E)
  (⋂ (i : ℕ),
    ⋃ (i_1 : ℕ),
      ⋂ (i_2 : ℕ),
        ⋂ (_ : i_2 ≥ i_1),
          ⋂ (i_3 : ℕ), ⋂ (_ : i_3 ≥ i_1), {x : α × E | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_3) ((1 / 2) ^ i)})
Tactic: simp only [setOf_forall, setOf_exists]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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}
⊢ MeasurableSet (α := α × E)
    (⋂ (i : ℕ),
      ⋃ (i_1 : ℕ),
        ⋂ (i_2 : ℕ),
          ⋂ (_ : i_2 ≥ i_1),
            ⋂ (i_3 : ℕ),
              ⋂ (_ : i_3 ≥ i_1), {x : α × E | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_3) ((1 / 2) ^ i)})
have refine : ∀ (x : ℕ),
  MeasurableSet (α := α × E)
    (⋃ (i : ℕ),
      ⋂ (i_1 : ℕ),
        ⋂ (_ : i_1 ≥ i),
          ⋂ (i_2 : ℕ),
            ⋂ (_ : i_2 ≥ i), {x_2 : α × E | x_2.2 ∈ B (f x_2.1) K ((1 / 2) ^ i_1) ((1 / 2) ^ i_2) ((1 / 2) ^ x)})
Tactic: refine MeasurableSet.iInter (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 : ℕ
⊢ MeasurableSet (α := α × E)
    (⋃ (i : ℕ),
      ⋂ (i_1 : ℕ),
        ⋂ (_ : i_1 ≥ i),
          ⋂ (i_2 : ℕ),
            ⋂ (_ : i_2 ≥ i), {x_2 : α × E | x_2.2 ∈ B (f x_2.1) K ((1 / 2) ^ i_1) ((1 / 2) ^ i_2) ((1 / 2) ^ x)})
have refine : ∀ (x_1 : ℕ),
  MeasurableSet (α := α × E)
    (⋂ (i : ℕ),
      ⋂ (_ : i ≥ x_1),
        ⋂ (i_1 : ℕ),
          ⋂ (_ : i_1 ≥ x_1), {x_3 : α × E | x_3.2 ∈ B (f x_3.1) K ((1 / 2) ^ i) ((1 / 2) ^ i_1) ((1 / 2) ^ x)})
Tactic: refine MeasurableSet.iUnion (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 : ℕ
⊢ MeasurableSet (α := α × E)
    (⋂ (i : ℕ),
      ⋂ (_ : i ≥ x_1),
        ⋂ (i_1 : ℕ),
          ⋂ (_ : i_1 ≥ x_1), {x_3 : α × E | x_3.2 ∈ B (f x_3.1) K ((1 / 2) ^ i) ((1 / 2) ^ i_1) ((1 / 2) ^ x)})
have refine : ∀ (x_2 : ℕ),
  MeasurableSet (α := α × E)
    (⋂ (_ : x_2 ≥ x_1),
      ⋂ (i : ℕ), ⋂ (_ : i ≥ x_1), {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ i) ((1 / 2) ^ x)})
Tactic: refine MeasurableSet.iInter (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 : ℕ
⊢ MeasurableSet (α := α × E)
    (⋂ (_ : x_2 ≥ x_1),
      ⋂ (i : ℕ), ⋂ (_ : i ≥ x_1), {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ i) ((1 / 2) ^ x)})
have refine : x_2 ≥ x_1 →
  MeasurableSet (α := α × E)
    (⋂ (i : ℕ), ⋂ (_ : i ≥ x_1), {x_4 : α × E | x_4.2 ∈ B (f x_4.1) K ((1 / 2) ^ x_2) ((1 / 2) ^ i) ((1 / 2) ^ x)})
Tactic: refine MeasurableSet.iInter (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)})
have 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)})
Tactic: refine MeasurableSet.iInter (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)})
have 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)}
Tactic: refine MeasurableSet.iInter (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ 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)}
have this₁ : ProperSpace E
Tactic: have : ProperSpace E := .of_locallyCompactSpace 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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)
⊢ MeasurableSet (α := α × E) {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2}
have this : IsComplete (α := E →L[𝕜] F) univ
Tactic: have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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}
have 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)
Tactic: convert! measurableSet_of_differentiableAt_of_isComplete_with_param hf this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
have refine : ∀ (s : Set (E →L[𝕜] F)) (hs : IsClosed s), MeasurableSet (α := α × E) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
Tactic: refine measurable_of_isClosed (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ MeasurableSet (α := α × E) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
have 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})
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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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) ((fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
have 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})
Tactic: rw [this]