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
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
a'₃ : ε + ε + b < s * 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

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

Premises used: norm_add₃_le, HSub.hSub, DFunLike.coe
-- 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
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] (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})

Tactic:
H
-- 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
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})
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})
⊢ IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ B (f p.1) K r s t}

Tactic:
convert! H
-- 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
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})
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
⊢ 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:
ext p
-- 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
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})
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:
simp [B]

Premises used: FDerivMeasurableAux.B
-- 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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
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})
⊢ IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ B (f p.1) K r 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]
-- 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
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})

Tactic:
isOpen_biUnion (fun L _ ↦ ?_)

Premises used: isOpen_biUnion
-- 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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
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}
⊢ 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:
refine isOpen_biUnion (fun L _ ↦ ?_)

Premises used: isOpen_biUnion
-- 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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
h : 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:
(isOpen_A_with_param hf L).inter (isOpen_A_with_param hf L)

Premises used: Set.Mem, setOf, FDerivMeasurableAux.A, FDerivMeasurableAux.isOpen_A_with_param, Set.inter, IsOpen.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
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
h : 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:
exact (isOpen_A_with_param hf L).inter (isOpen_A_with_param hf L)

Premises used: FDerivMeasurableAux.isOpen_A_with_param, IsOpen.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
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
⊢ 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:
simp [← differentiable_set_eq_D K hK]

Premises used: FDerivMeasurableAux.differentiable_set_eq_D
-- 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
⊢ 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]
-- 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}
rw : MeasurableSet (α := α × E) {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}

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
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}
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)}
⊢ MeasurableSet (α := α × E) {p : α × E | p.2 ∈ D (f p.1) K}

Tactic:
simp only [D, mem_iInter, mem_iUnion]

Premises used: Set.mem_iUnion, Set.mem_iInter, FDerivMeasurableAux.D
-- 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}
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)})
⊢ 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 [setOf_forall, setOf_exists]

Premises used: Set.setOf_exists, Set.setOf_forall
-- 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}
⊢ 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:
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}
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)})
⊢ 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:
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 : ℕ
⊢ 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:
MeasurableSet.iUnion (fun _ ↦ ?_)

Premises used: MeasurableSet.iUnion
-- 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 : ℕ
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)})
⊢ 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.iUnion (fun _ ↦ ?_)

Premises used: MeasurableSet.iUnion
-- 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 : ℕ
⊢ 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:
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 : ℕ
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)})
⊢ 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.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 : ℕ
⊢ 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:
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 : ℕ
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)})
⊢ 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 _ ↦ ?_)

Premises used: MeasurableSet.iInter