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 : 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_1 : ℝ
b_lt : b_1 < s * r
hb_1 :
  ∀ 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_1
ε : ℝ
εpos : 0 < ε
hε : b_1 + 2 * ε < s * r
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
b : α
y : E
hb : Membership.mem (γ := Set α) {a} (b, y).1
⊢ b = a

Tactic:
simp only [mem_singleton_iff] at hb

Premises used: Set.mem_singleton_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
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : 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_1 : ℝ
b_lt : b_1 < s * r
hb_1 :
  ∀ 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_1
ε : ℝ
εpos : 0 < ε
hε : b_1 + 2 * ε < s * r
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
b : α
y : E
hb : b = a
⊢ Function.uncurry f (b, y) = (fun (p : α × E) ↦ f a p.2) (b, y)

Tactic:
simp [hb]
-- 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 : 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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
⊢ EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))

Tactic:
have D : ({a} ×ˢ closedBall x t).EqOn f.uncurry (fun p ↦ f a p.2) := by
      rintro ⟨b, y⟩ ⟨hb, -⟩
      simp only [mem_singleton_iff] at hb
      simp [hb]
-- 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 : 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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
⊢ ∃ (v : Set (α × E)),
    IsOpen[instTopologicalSpaceProd] v ∧
      SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v ∧ ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε

Tactic:
Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq (s := {a} ×ˢ closedBall x t)
        (fun p _ ↦ hf.continuousAt) (fun p _ ↦ C.continuousAt) D (dist_mem_uniformity εpos)

Premises used: Set.Mem, Continuous.continuousAt, Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq, Metric.dist_mem_uniformity
-- 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 : 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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
obtain :
  ∀ (v : Set (α × E)) (v_open : IsOpen[instTopologicalSpaceProd] v)
    (sub_v : SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v)
    (hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε),
    ∃ (u : Set α),
      IsOpen[inst_6] u ∧
        a ∈ u ∧
          ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
⊢ ∃ (u : Set α),
    IsOpen[inst_6] u ∧
      a ∈ u ∧
        ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε

Tactic:
obtain ⟨v, v_open, sub_v, hv⟩ : ∃ v, IsOpen v ∧ {a} ×ˢ closedBall x t ⊆ v ∧
        ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε :=
      Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq (s := {a} ×ˢ closedBall x t)
        (fun p _ ↦ hf.continuousAt) (fun p _ ↦ C.continuousAt) D (dist_mem_uniformity εpos)

Premises used: Continuous.continuousAt, Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq, Metric.closedBall, Metric.dist_mem_uniformity
-- 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 : 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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
v : Set (α × E)
v_open : IsOpen[instTopologicalSpaceProd] v
sub_v : SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v
hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε
⊢ ∃ (w : Set α) (w' : Set E),
    IsOpen[inst_6] w ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w' ∧ {a} ⊆ w ∧ closedBall x t ⊆ w' ∧ w ×ˢ w' ⊆ v

Tactic:
generalized_tube_lemma isCompact_singleton (isCompact_closedBall x t) v_open sub_v

Premises used: isCompact_singleton, generalized_tube_lemma, ProperSpace.isCompact_closedBall
-- 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 : 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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
v : Set (α × E)
v_open : IsOpen[instTopologicalSpaceProd] v
sub_v : SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v
hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε
obtain :
  ∀ (w : Set α) (w' : Set E) (w_open : IsOpen[inst_6] w) (sub_w : {a} ⊆ w) (sub_w' : closedBall x t ⊆ w')
    (hww' : w ×ˢ w' ⊆ v),
    ∃ (u : Set α),
      IsOpen[inst_6] u ∧
        a ∈ u ∧
          ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
⊢ ∃ (u : Set α),
    IsOpen[inst_6] u ∧
      a ∈ u ∧
        ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε

Tactic:
obtain ⟨w, w', w_open, -, sub_w, sub_w', hww'⟩ : ∃ (w : Set α) (w' : Set E),
        IsOpen w ∧ IsOpen w' ∧ {a} ⊆ w ∧ closedBall x t ⊆ w' ∧ w ×ˢ w' ⊆ v :=
      generalized_tube_lemma isCompact_singleton (isCompact_closedBall x t) v_open sub_v

Premises used: isCompact_singleton, generalized_tube_lemma, ProperSpace.isCompact_closedBall, Metric.closedBall, Set
-- 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 : 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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
v : Set (α × E)
v_open : IsOpen[instTopologicalSpaceProd] v
sub_v : SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v
hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε
w : Set α
w' : Set E
w_open : IsOpen[inst_6] w
sub_w : {a} ⊆ w
sub_w' : closedBall x t ⊆ w'
hww' : w ×ˢ w' ⊆ v
⊢ ∃ (u : Set α),
    IsOpen[inst_6] u ∧
      a ∈ u ∧
        ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε

Tactic:
⟨w, w_open, sub_w rfl, ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- 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 : 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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
v : Set (α × E)
v_open : IsOpen[instTopologicalSpaceProd] v
sub_v : SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v
hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε
w : Set α
w' : Set E
w_open : IsOpen[inst_6] w
sub_w : {a} ⊆ w
sub_w' : closedBall x t ⊆ w'
hww' : w ×ˢ w' ⊆ v
refine : ∀ (p : α × E), p.1 ∈ w → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
⊢ ∃ (u : Set α),
    IsOpen[inst_6] u ∧
      a ∈ u ∧
        ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε

Tactic:
refine ⟨w, w_open, sub_w rfl, ?_⟩
-- 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 : 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_1 : ℝ
b_lt : b_1 < 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_1
ε : ℝ
εpos : 0 < ε
hε : b_1 + 2 * ε < s * r
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
v : Set (α × E)
v_open : IsOpen[instTopologicalSpaceProd] v
sub_v : SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v
hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε
w : Set α
w' : Set E
w_open : IsOpen[inst_6] w
sub_w : {a} ⊆ w
sub_w' : closedBall x t ⊆ w'
hww' : w ×ˢ w' ⊆ v
b : α
y : E
h : (b, y).1 ∈ w
hby : (b, y).2 ∈ closedBall x t
⊢ dist (Function.uncurry f (b, y)) (Function.uncurry f (a, (b, y).2)) < ε

Tactic:
hv _ (hww' ⟨h, sub_w' hby⟩)

Premises used: And.intro
-- 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 : 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_1 : ℝ
b_lt : b_1 < 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_1
ε : ℝ
εpos : 0 < ε
hε : b_1 + 2 * ε < s * r
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2
D : EqOn (Function.uncurry f) (fun (p : α × E) ↦ f a p.2) (SProd.sprod (α := Set α) {a} (closedBall x t))
v : Set (α × E)
v_open : IsOpen[instTopologicalSpaceProd] v
sub_v : SProd.sprod (α := Set α) {a} (closedBall x t) ⊆ v
hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε
w : Set α
w' : Set E
w_open : IsOpen[inst_6] w
sub_w : {a} ⊆ w
sub_w' : closedBall x t ⊆ w'
hww' : w ×ˢ w' ⊆ v
b : α
y : E
h : (b, y).1 ∈ w
hby : (b, y).2 ∈ closedBall x t
⊢ dist (Function.uncurry f (b, y)) (Function.uncurry f (a, (b, y).2)) < ε

Tactic:
exact hv _ (hww' ⟨h, sub_w' hby⟩)

Premises used: And.intro
-- 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 : 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
obtain :
  ∀ (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)) < ε),
    {p : α × E |
        ∃ (r' : ℝ),
          (r / 2 < r' ∧ r' ≤ r) ∧
            ∀ (y : E),
              dist y p.2 < r' →
                ∀ (z : E),
                  dist z p.2 < r' →
                    ‖f p.1 z - f p.1 y -
                          HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                      s * r} ∈
      𝓝 (a, x)
⊢ {p : α × E |
      ∃ (r' : ℝ),
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E),
            dist y p.2 < r' →
              ∀ (z : E),
                dist z p.2 < r' →
                  ‖f p.1 z - f p.1 y -
                        HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                    s * r} ∈
    𝓝 (a, x)

Tactic:
obtain ⟨u, u_open, au, hu⟩ : ∃ u, IsOpen u ∧ a ∈ u ∧ ∀ (p : α × E),
      p.1 ∈ u → p.2 ∈ closedBall x t → dist (f.uncurry p) (f.uncurry (a, p.2)) < ε := by
    have C : Continuous (fun (p : α × E) ↦ f a p.2) := by fun_prop
    have D : ({a} ×ˢ closedBall x t).EqOn f.uncurry (fun p ↦ f a p.2) := by
      rintro ⟨b, y⟩ ⟨hb, -⟩
      simp only [mem_singleton_iff] at hb
      simp [hb]
    obtain ⟨v, v_open, sub_v, hv⟩ : ∃ v, IsOpen v ∧ {a} ×ˢ closedBall x t ⊆ v ∧
        ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε :=
      Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq (s := {a} ×ˢ closedBall x t)
        (fun p _ ↦ hf.continuousAt) (fun p _ ↦ C.continuousAt) D (dist_mem_uniformity εpos)
    obtain ⟨w, w', w_open, -, sub_w, sub_w', hww'⟩ : ∃ (w : Set α) (w' : Set E),
        IsOpen w ∧ IsOpen w' ∧ {a} ⊆ w ∧ closedBall x t ⊆ w' ∧ w ×ˢ w' ⊆ v :=
      generalized_tube_lemma isCompact_singleton (isCompact_closedBall x t) v_open sub_v
    refine ⟨w, w_open, sub_w rfl, ?_⟩
    rintro ⟨b, y⟩ h hby
    exact hv _ (hww' ⟨h, sub_w' hby⟩)