awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑f : (a : E) → F) x = f

Tactic:
exact f.fderiv

Premises used: ContinuousLinearMap.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : Filter (E × E)
h : IsBoundedLinearMap 𝕜 f
⊢ HasFDerivAtFilter f (toContinuousLinearMap f h) L

Tactic:
h.toContinuousLinearMap.hasFDerivAtFilter

Premises used: IsBoundedLinearMap.toContinuousLinearMap, ContinuousLinearMap.hasFDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : IsBoundedLinearMap 𝕜 f
⊢ HasFDerivWithinAt f (toContinuousLinearMap f h) s x

Tactic:
h.hasFDerivAtFilter

Premises used: HasFDerivWithinAt, IsBoundedLinearMap.hasFDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : IsBoundedLinearMap 𝕜 f
⊢ HasFDerivAt f (toContinuousLinearMap f h) x

Tactic:
h.hasFDerivAtFilter

Premises used: HasFDerivAt, IsBoundedLinearMap.hasFDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : IsBoundedLinearMap 𝕜 f
⊢ DifferentiableAt 𝕜 f x

Tactic:
h.hasFDerivAt.differentiableAt

Premises used: HasFDerivAt.differentiableAt, IsBoundedLinearMap.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : IsBoundedLinearMap 𝕜 f
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
h.differentiableAt.differentiableWithinAt

Premises used: IsBoundedLinearMap.differentiableAt, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : IsBoundedLinearMap 𝕜 f
⊢ fderiv 𝕜 f x = toContinuousLinearMap f h

Tactic:
HasFDerivAt.fderiv h.hasFDerivAt

Premises used: HasFDerivAt.fderiv, IsBoundedLinearMap.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
rw : fderiv 𝕜 f x = toContinuousLinearMap f h
⊢ fderivWithin 𝕜 f s x = toContinuousLinearMap f h

Tactic:
rw [DifferentiableAt.fderivWithin h.differentiableAt hxs]

Premises used: IsBoundedLinearMap.differentiableAt, DifferentiableAt.fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 f x = toContinuousLinearMap f h

Tactic:
h.fderiv

Premises used: IsBoundedLinearMap.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 f x = toContinuousLinearMap f h

Tactic:
exact h.fderiv

Premises used: IsBoundedLinearMap.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
h : IsBoundedLinearMap 𝕜 f
⊢ Differentiable 𝕜 f

Tactic:
fun _ => h.differentiableAt

Premises used: IsBoundedLinearMap.differentiableAt, Differentiable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : IsBoundedLinearMap 𝕜 f
⊢ DifferentiableOn 𝕜 f s

Tactic:
h.differentiable.differentiableOn

Premises used: IsBoundedLinearMap.differentiable, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : SecondCountableTopologyEither (E →L[𝕜] F) E
inst_8 : MeasurableSpace F
inst_9 : BorelSpace F
⊢ Measurable (β := F) fun (p : (E →L[𝕜] F) × E) ↦ (p.1 : (a : E) → F) p.2

Tactic:
isBoundedBilinearMap_apply.continuous.measurable

Premises used: IsBoundedBilinearMap.continuous, isBoundedBilinearMap_apply, Continuous.measurable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
rw : ∀ x ∈ A f L r ε, ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (A f L r ε)

Tactic:
rw [Metric.isOpen_iff]

Premises used: Metric.isOpen_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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ ∃ (s : ℝ), r / 2 < s ∧ s < r'

Tactic:
exists_between r'_mem.1

Premises used: exists_between, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
obtain : ∀ (s : ℝ) (s_gt : r / 2 < s) (s_lt : s < r'), ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
⊢ ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε

Tactic:
obtain ⟨s, s_gt, s_lt⟩ : ∃ s : ℝ, r / 2 < s ∧ s < r' := exists_between r'_mem.1

Premises used: exists_between, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
⊢ s ∈ Ioc (r / 2) r

Tactic:
have : s ∈ Ioc (r / 2) r := ⟨s_gt, le_of_lt (s_lt.trans_le r'_mem.2)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
linarith : r' - s ≤ 0 → 2 / 2 = 1
linarith₁ : r' - s ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : r' - s ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : r' - s ≤ 0 → s - r' + (r' - s - 0) = 0
⊢ r' - s > 0

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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
refine :
  ∀ (x' : E) (hx' : x' ∈ ball x (r' - s)),
    ∀ y ∈ ball x' s, ∀ z ∈ ball x' s, ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε

Tactic:
refine ⟨r' - s, by linarith, fun x' hx' => ⟨s, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
⊢ ball x' s ⊆ ball x r'

Tactic:
have B : ball x' s ⊆ ball x r' := ball_subset (le_of_lt hx')
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
y : E
hy : y ∈ ball x' s
z : E
hz : z ∈ ball x' s
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r

Tactic:
hr' y (B hy) z (B 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
y : E
hy : y ∈ ball x' s
z : E
hz : z ∈ ball x' s
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r

Tactic:
exact hr' y (B hy) z (B 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
r s ε : ℝ
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B f K r s ε)

Tactic:
simp [B, isOpen_biUnion, IsOpen.inter, isOpen_A]

Premises used: FDerivMeasurableAux.isOpen_A, IsOpen.inter, FDerivMeasurableAux.B, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ x ∈ A f L r δ

Tactic:
⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans_le (mul_le_mul_of_nonneg_right h ?_)⟩

Premises used: Set.Mem, setOf, FDerivMeasurableAux.A, mul_le_mul_of_nonneg_right, LT.lt.trans_le, And.intro, Exists.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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
refine : ∀ (y : E) (hy : y ∈ ball x r') (z : E) (hz : z ∈ ball x r'), 0 ≤ r
⊢ x ∈ A f L r δ

Tactic:
refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans_le (mul_le_mul_of_nonneg_right 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
y : E
hy : y ∈ ball x r'
z : E
hz : z ∈ ball x r'
linarith : r < 0 → r - 0 + (dist y x - r') + (r' - r) + (0 - dist y x) = 0
⊢ 0 ≤ r

Tactic:
linarith [mem_ball.1 hy, r'r.2, @dist_nonneg _ _ y x]

Premises used: dist_nonneg, Metric.mem_ball, And.right, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x : E
hx : x ∈ A f L r ε
y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
rcases :
  ∀ (r' : ℝ) (r'mem : r' ∈ Ioc (r / 2) r)
    (hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r),
    ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ ≤ ε * r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ ≤ ε * r

Tactic:
rcases hx with ⟨r', r'mem, hr'⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
hab : ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ ≤ ε * r

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r

Tactic:
hr' _ ((mem_closedBall.1 hy).trans_lt r'mem.1) _ ((mem_closedBall.1 hz).trans_lt r'mem.1)

Premises used: And.left, Iff.mp, Metric.mem_closedBall, LE.le.trans_lt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((L : (a : E) → F) (z - y) : F)‖ < ε * r

Tactic:
exact hr' _ ((mem_closedBall.1 hy).trans_lt r'mem.1) _ ((mem_closedBall.1 hz).trans_lt r'mem.1)

Premises used: And.left, Iff.mp, Metric.mem_closedBall, LE.le.trans_lt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
⊢ 0 < δ

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
obtain :
  ∀ (R : ℝ) (R_pos : R > 0)
    (hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖),
    ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε

Tactic:
obtain ⟨R, R_pos, hR⟩ :
      ∃ R > 0, ∀ y ∈ ball x R, ‖f y - f x - fderiv 𝕜 f x (y - x)‖ ≤ δ * ‖y - x‖ :=
    eventually_nhds_iff_ball.1 <| hx.hasFDerivAt.isLittleO.bound <| by positivity

Premises used: Asymptotics.IsLittleO.bound, DifferentiableAt.hasFDerivAt, Iff.mp, Metric.eventually_nhds_iff_ball, HasFDerivAt.isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε

Tactic:
⟨R, R_pos, fun r hr => ?_⟩

Premises used: And.intro, Exists.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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
refine : ∀ (r : ℝ) (hr : r ∈ Ioo 0 R), x ∈ A f (fderiv 𝕜 f x) r ε
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε

Tactic:
refine ⟨R, R_pos, fun r hr => ?_⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
⊢ r ∈ Ioc (r / 2) r

Tactic:
have : r ∈ Ioc (r / 2) r := right_mem_Ioc.2 <| half_lt_self hr.1
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
⊢ x ∈ A f (fderiv 𝕜 f x) r ε

Tactic:
⟨r, this, fun y hy z hz => ?_⟩

Premises used: Set.Mem, setOf, FDerivMeasurableAux.A, And.intro, Exists.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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
refine :
  ∀ (y : E) (hy : y ∈ ball x r) (z : E) (hz : z ∈ ball x r),
    ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ < ε * r
⊢ x ∈ A f (fderiv 𝕜 f x) r ε

Tactic:
refine ⟨r, this, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
simp :
  ‖f z - f y - HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) z : F) ((fderiv 𝕜 f x : (a : E) → F) y : F)‖ =
    ‖f z - f x - HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) z : F) ((fderiv 𝕜 f x : (a : E) → F) x : F) -
        (f y - f x -
          HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) y : F) ((fderiv 𝕜 f x : (a : E) → F) x : F))‖
⊢ ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ =
    ‖HSub.hSub (β := F) (f z - f x) ((fderiv 𝕜 f x : (a : E) → F) (z - x) : F) -
        HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖

Tactic:
simp only [map_sub]

Premises used: map_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ‖f z - f y - HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) z : F) ((fderiv 𝕜 f x : (a : E) → F) y : F)‖ =
    ‖f z - f x - HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) z : F) ((fderiv 𝕜 f x : (a : E) → F) x : F) -
        (f y - f x -
          HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) y : F) ((fderiv 𝕜 f x : (a : E) → F) x : F))‖

Tactic:
abel_nf