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 :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
rcases :
  ∀ (p : E × E) (pt : p ∈ closedBall x t ×ˢ closedBall x t)
    (hp :
      IsMaxOn (β := ℝ)
        (fun (p : E × E) ↦
          ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖)
        (closedBall x t ×ˢ closedBall x t) p),
    ∃ b < s * r,
      ∀ 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
⊢ ∃ b < s * r,
    ∀ 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

Tactic:
rcases ((isCompact_closedBall x t).prod (isCompact_closedBall x t)).exists_isMaxOn
      C B.continuousOn with ⟨p, pt, hp⟩

Premises used: Continuous.continuousOn, IsCompact.prod, ProperSpace.isCompact_closedBall, IsCompact.exists_isMaxOn
-- 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 :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
pt : p ∈ closedBall x t ×ˢ closedBall x t
hp :
  IsMaxOn (β := ℝ)
    (fun (p : E × E) ↦
      ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖)
    (closedBall x t ×ˢ closedBall x t) p
⊢ dist p.1 x ≤ t ∧ dist p.2 x ≤ t

Tactic:
simp only [mem_prod, mem_closedBall] at pt

Premises used: Set.mem_prod, Metric.mem_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 :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
hp :
  IsMaxOn (β := ℝ)
    (fun (p : E × E) ↦
      ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖)
    (closedBall x t ×ˢ closedBall x t) p
pt : dist p.1 x ≤ t ∧ dist p.2 x ≤ t
⊢ ∃ b < s * r,
    ∀ 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

Tactic:
⟨‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖,
      hr p.1 (pt.1.trans_lt htr') p.2 (pt.2.trans_lt htr'), fun y hy z hz ↦ ?_⟩

Premises used: Norm.norm, HSub.hSub, Prod.fst, And.right, And.left, And.intro, Exists.intro, LE.le.trans_lt, Prod.snd, 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 : ℝ
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 :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
hp :
  IsMaxOn (β := ℝ)
    (fun (p : E × E) ↦
      ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖)
    (closedBall x t ×ˢ closedBall x t) p
pt : dist p.1 x ≤ t ∧ dist p.2 x ≤ t
refine :
  ∀ (y : E) (hy : y ∈ closedBall x t) (z : E) (hz : 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)‖ ≤
      ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
⊢ ∃ b < s * r,
    ∀ 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

Tactic:
refine ⟨‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖,
      hr p.1 (pt.1.trans_lt htr') p.2 (pt.2.trans_lt htr'), fun y hy z hz ↦ ?_⟩
-- 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 :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
hp :
  IsMaxOn (β := ℝ)
    (fun (p : E × E) ↦
      ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖)
    (closedBall x t ×ˢ closedBall x t) p
pt : dist p.1 x ≤ t ∧ dist p.2 x ≤ t
y : E
hy : y ∈ closedBall x t
z : E
hz : z ∈ closedBall x t
⊢ (y, z) ∈ closedBall x t ×ˢ closedBall x t

Tactic:
have D : (y, z) ∈ closedBall x t ×ˢ closedBall x t := mem_prod.2 ⟨hy, hz⟩
-- 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 :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
hp :
  IsMaxOn (β := ℝ)
    (fun (p : E × E) ↦
      ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖)
    (closedBall x t ×ˢ closedBall x t) p
pt : dist p.1 x ≤ t ∧ dist p.2 x ≤ t
y : E
hy : y ∈ closedBall x t
z : E
hz : z ∈ closedBall x t
D : (y, z) ∈ closedBall x t ×ˢ 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)‖ ≤
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖

Tactic:
hp D

Premises used: Set.Mem
-- 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 :
  Continuous[instTopologicalSpaceProd, _] fun (p : E × E) ↦
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
hp :
  IsMaxOn (β := ℝ)
    (fun (p : E × E) ↦
      ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖)
    (closedBall x t ×ˢ closedBall x t) p
pt : dist p.1 x ≤ t ∧ dist p.2 x ≤ t
y : E
hy : y ∈ closedBall x t
z : E
hz : z ∈ closedBall x t
D : (y, z) ∈ closedBall x t ×ˢ 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)‖ ≤
    ‖f a p.2 - f a p.1 - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) p.2 : F) ((L : (a : E) → F) p.1 : F)‖

Tactic:
exact hp 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
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
obtain :
  ∀ (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),
    {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 ⟨b, b_lt, hb⟩ : ∃ b, b < s * r ∧ ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t,
      ‖f a z - f a y - (L z - L y)‖ ≤ b := by
    have B : Continuous (fun (p : E × E) ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖) := by fun_prop
    have C : (closedBall x t ×ˢ closedBall x t).Nonempty := by simp; linarith
    rcases ((isCompact_closedBall x t).prod (isCompact_closedBall x t)).exists_isMaxOn
      C B.continuousOn with ⟨p, pt, hp⟩
    simp only [mem_prod, mem_closedBall] at pt
    refine ⟨‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖,
      hr p.1 (pt.1.trans_lt htr') p.2 (pt.2.trans_lt htr'), fun y hy z hz ↦ ?_⟩
    have D : (y, z) ∈ closedBall x t ×ˢ closedBall x t := mem_prod.2 ⟨hy, hz⟩
    exact hp D

Premises used: Metric.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
linarith : (s * r - b) / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (s * r - b) / 3 ≤ 0 → 3 / 3 = 1
linarith₂ : (s * r - b) / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₃ : (s * r - b) / 3 ≤ 0 → GT.gt (α := ℝ) 3 0
linarith₄ : (s * r - b) / 3 ≤ 0 → 2 / 2 = 1
linarith₅ : (s * r - b) / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : (s * r - b) / 3 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₇ : (s * r - b) / 3 ≤ 0 → 2 / 2 = 1
linarith₈ : (s * r - b) / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : (s * r - b) / 3 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₁₀ : (s * r - b) / 3 ≤ 0 → 2 / 2 = 1
linarith₁₁ : (s * r - b) / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : (s * r - b) / 3 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₁₃ : (s * r - b) / 3 ≤ 0 → b - s * r + (1 * s * (1 * r) - 1 * b - HMul.hMul (α := ℝ) 3 0) = 0
⊢ 0 < (s * r - b) / 3

Tactic:
linarith
-- 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
linarith : s * r ≤ b + 2 * ((s * r - b) / 3) → HMul.hMul (α := ℝ) 1 3 = 3
linarith₁ : s * r ≤ b + 2 * ((s * r - b) / 3) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ : s * r ≤ b + 2 * ((s * r - b) / 3) → 3 / 3 = 1
linarith₃ linarith₄ : s * r ≤ b + 2 * ((s * r - b) / 3) → HMul.hMul (α := ℝ) 1 3 = 3
linarith₅ : s * r ≤ b + 2 * ((s * r - b) / 3) → GT.gt (α := ℝ) 3 0
linarith₆ : s * r ≤ b + 2 * ((s * r - b) / 3) → 2 / 2 = 1
linarith₇ : s * r ≤ b + 2 * ((s * r - b) / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : s * r ≤ b + 2 * ((s * r - b) / 3) → GT.gt (α := ℝ) 2 0
linarith₉ : s * r ≤ b + 2 * ((s * r - b) / 3) → 2 / 2 = 1
linarith₁₀ : s * r ≤ b + 2 * ((s * r - b) / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : s * r ≤ b + 2 * ((s * r - b) / 3) → GT.gt (α := ℝ) 2 0
linarith₁₂ : s * r ≤ b + 2 * ((s * r - b) / 3) → 2 / 2 = 1
linarith₁₃ : s * r ≤ b + 2 * ((s * r - b) / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₄ : s * r ≤ b + 2 * ((s * r - b) / 3) → GT.gt (α := ℝ) 2 0
linarith₁₅ :
  s * r ≤ b + 2 * ((s * r - b) / 3) →
    b - s * r + (1 * s * (3 * r) - (3 * b + HMul.hMul (α := ℝ) 1 2 * (1 * s * (1 * r) - 1 * b))) = 0
⊢ b + 2 * ((s * r - b) / 3) < s * r

Tactic:
linarith
-- 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
obtain :
  ∀ (ε : ℝ) (εpos : 0 < ε) (hε : b + 2 * ε < s * r),
    {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 ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ b + 2 * ε < s * r :=
    ⟨(s * r - b) / 3, by linarith, by linarith⟩
-- 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
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2

Tactic:
fun_prop
-- 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
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × E) ↦ f a p.2

Tactic:
have C : Continuous (fun (p : α × E) ↦ f a p.2) := by fun_prop