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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
inst_8 : MeasurableSpace F
inst_9 : BorelSpace F
y : E
⊢ Measurable.{u_2, u_3} (β := F) fun (x : E) ↦ (fderiv 𝕜 f x : (a : E) → F) y

Tactic:
(ContinuousLinearMap.measurable_apply y).comp (measurable_fderiv 𝕜 f)

Premises used: Measurable.comp, ContinuousLinearMap.measurable_apply, measurable_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
f : 𝕜 → F
⊢ Measurable (deriv f)

Tactic:
simpa only [fderiv_apply_one_eq_deriv] using measurable_fderiv_apply_const 𝕜 f 1

Premises used: measurable_fderiv_apply_const, fderiv_apply_one_eq_deriv, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
⊢ let this := borel F;
  BorelSpace F

Tactic:
borelize F
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
inl : ∀ (h𝕜 : SecondCountableTopology 𝕜), StronglyMeasurable (deriv f)
inr : ∀ (hF : SecondCountableTopology F), StronglyMeasurable (deriv f)
⊢ StronglyMeasurable (deriv f)

Tactic:
rcases h.out with h𝕜 | hF

Premises used: SecondCountableTopologyEither.out
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
h𝕜 : SecondCountableTopology 𝕜
⊢ StronglyMeasurable (deriv f)

Tactic:
stronglyMeasurable_iff_measurable_separable.2
      ⟨measurable_deriv f, isSeparable_range_deriv _⟩

Premises used: Iff.mpr, measurable_deriv, stronglyMeasurable_iff_measurable_separable, isSeparable_range_deriv, And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
h𝕜 : SecondCountableTopology 𝕜
⊢ StronglyMeasurable (deriv f)

Tactic:
exact stronglyMeasurable_iff_measurable_separable.2
      ⟨measurable_deriv f, isSeparable_range_deriv _⟩

Premises used: Iff.mpr, measurable_deriv, stronglyMeasurable_iff_measurable_separable, isSeparable_range_deriv, And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)

Tactic:
(measurable_deriv f).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, measurable_deriv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)

Tactic:
exact (measurable_deriv f).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, measurable_deriv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
f : 𝕜 → F
μ : Measure 𝕜
⊢ AEMeasurable (deriv f) μ

Tactic:
(measurable_deriv f).aemeasurable

Premises used: Measurable.aemeasurable, measurable_deriv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : CompleteSpace F
inst_4 : MeasurableSpace 𝕜
inst_5 : OpensMeasurableSpace 𝕜
inst_6 : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
μ : Measure 𝕜
⊢ AEStronglyMeasurable (deriv f) μ

Tactic:
(stronglyMeasurable_deriv f).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_deriv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x : ℝ
hx : x ∈ A f L r ε
rcases :
  ∀ (r' : ℝ) (rr' : r' ∈ Ioc (r / 2) r)
    (hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r), A f L r ε ∈ 𝓝[>] x
⊢ A f L r ε ∈ 𝓝[>] x

Tactic:
rcases hx with ⟨r', rr', hr'⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ ∃ (s : ℝ), r / 2 < s ∧ s < r'

Tactic:
exists_between rr'.1

Premises used: exists_between, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
obtain : ∀ (s : ℝ) (s_gt : r / 2 < s) (s_lt : s < r'), A f L r ε ∈ 𝓝[>] x
⊢ A f L r ε ∈ 𝓝[>] x

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

Premises used: exists_between, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * 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 rr'.2)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
linarith : x + r' - s ≤ x → 2 / 2 = 1
linarith₁ : x + r' - s ≤ x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x + r' - s ≤ x → GT.gt (α := ℝ) 2 0
linarith₃ : x + r' - s ≤ x → s - r' + (x + r' - s - x) = 0
⊢ x < x + r' - s

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
h : ∀ (x' : ℝ) (hx' : x' ∈ Ioo x (x + r' - s)), x' ∈ A f L r ε
⊢ A f L r ε ∈ 𝓝[>] x

Tactic:
filter_upwards [Ioo_mem_nhdsGT <| show x < x + r' - s by linarith] with x' hx'

Premises used: Ioo_mem_nhdsGT
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
right : ∀ y ∈ Icc x' (x' + s), ∀ z ∈ Icc x' (x' + s), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x' ∈ A f L r ε

Tactic:
use s, this
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
apply : x' + s ≤ x + r'
⊢ Icc x' (x' + s) ⊆ Icc x (x + r')

Tactic:
apply Icc_subset_Icc hx'.1.le

Premises used: LT.lt.le, And.left, Set.Icc_subset_Icc
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
linarith : x + r' < x' + s → 2 / 2 = 1
linarith₁ : x + r' < x' + s → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x + r' < x' + s → GT.gt (α := ℝ) 2 0
linarith₃ : x + r' < x' + s → x + r' - (x' + s) + (x' - (x + r' - s)) = 0
⊢ x' + s ≤ x + r'

Tactic:
linarith [hx'.2]

Premises used: And.right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ Icc x' (x' + s) ⊆ Icc x (x + r')

Tactic:
have A : Icc x' (x' + s) ⊆ Icc x (x + r') := by
    apply Icc_subset_Icc hx'.1.le
    linarith [hx'.2]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
y : ℝ
hy : y ∈ Icc x' (x' + s)
z : ℝ
hz : z ∈ Icc x' (x' + s)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
hr' y (A hy) z (A hz)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
y : ℝ
hy : y ∈ Icc x' (x' + s)
z : ℝ
hz : z ∈ Icc x' (x' + s)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
exact hr' y (A hy) z (A hz)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
⊢ ∃ L ∈ K, x ∈ A f L r ε ∧ x ∈ A f L s ε

Tactic:
simpa only [B, mem_iUnion, mem_inter_iff, exists_prop] using hx

Premises used: Set.mem_inter_iff, Set.mem_iUnion, exists_prop, RightDerivMeasurableAux.B
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
obtain : ∀ (L : F) (LK : L ∈ K) (hL₁ : x ∈ A f L r ε) (hL₂ : x ∈ A f L s ε), B f K r s ε ∈ 𝓝[>] x
⊢ B f K r s ε ∈ 𝓝[>] x

Tactic:
obtain ⟨L, LK, hL₁, hL₂⟩ : ∃ L : F, L ∈ K ∧ x ∈ A f L r ε ∧ x ∈ A f L s ε := by
    simpa only [B, mem_iUnion, mem_inter_iff, exists_prop] using hx
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
h : ∀ (y : ℝ) (hy₁ : y ∈ A f L r ε) (hy₂ : y ∈ A f L s ε), y ∈ B f K r s ε
⊢ B f K r s ε ∈ 𝓝[>] x

Tactic:
filter_upwards [A_mem_nhdsGT hL₁, A_mem_nhdsGT hL₂] with y hy₁ hy₂

Premises used: RightDerivMeasurableAux.A_mem_nhdsGT
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
y : ℝ
hy₁ : y ∈ A f L r ε
hy₂ : y ∈ A f L s ε
h : ∃ i ∈ K, y ∈ A f i r ε ∧ y ∈ A f i s ε
⊢ y ∈ B f K r s ε

Tactic:
simp only [B, mem_iUnion, mem_inter_iff, exists_prop]

Premises used: Set.mem_inter_iff, Set.mem_iUnion, exists_prop, RightDerivMeasurableAux.B
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
y : ℝ
hy₁ : y ∈ A f L r ε
hy₂ : y ∈ A f L s ε
⊢ ∃ i ∈ K, y ∈ A f i r ε ∧ y ∈ A f i s ε

Tactic:
⟨L, LK, hy₁, hy₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
y : ℝ
hy₁ : y ∈ A f L r ε
hy₂ : y ∈ A f L s ε
⊢ ∃ i ∈ K, y ∈ A f i r ε ∧ y ∈ A f i s ε

Tactic:
exact ⟨L, LK, hy₁, hy₂⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε : ℝ
⊢ MeasurableSet (B f K r s ε)

Tactic:
.of_mem_nhdsGT fun _ hx => B_mem_nhdsGT hx

Premises used: MeasurableSet.of_mem_nhdsGT, RightDerivMeasurableAux.B_mem_nhdsGT
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x ∈ A f L r δ

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

Premises used: Set.Mem, setOf, mul_le_mul_of_nonneg_right, And.intro, Exists.intro, RightDerivMeasurableAux.A, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
refine : ∀ (y : ℝ) (hy : y ∈ Icc x (x + r')) (z : ℝ) (hz : z ∈ Icc x (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 (mul_le_mul_of_nonneg_right h ?_)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
y : ℝ
hy : y ∈ Icc x (x + r')
z : ℝ
hz : z ∈ Icc x (x + r')
linarith : r < 0 → r - 0 + (x - y) + (y - (x + r')) + (r' - r) = 0
⊢ 0 ≤ r

Tactic:
linarith [hy.1, hy.2, r'r.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x : ℝ
hx : x ∈ A f L r ε
y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
rcases :
  ∀ (r' : ℝ) (r'mem : r' ∈ Ioc (r / 2) r)
    (hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r),
    ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
rcases hx with ⟨r', r'mem, hr'⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
linarith : x + r' < x + r / 2 → 2 / 2 = 1
linarith₁ : x + r' < x + r / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x + r' < x + r / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : x + r' < x + r / 2 → 2 / 2 = 1
linarith₄ : x + r' < x + r / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : x + r' < x + r / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : x + r' < x + r / 2 → 2 * x + 2 * r' - (2 * x + 1 * r) + (1 * r - 2 * r') = 0
⊢ x + r / 2 ≤ x + r'

Tactic:
linarith [r'mem.1]

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x + r / 2 ≤ x + r'

Tactic:
have A : x + r / 2 ≤ x + r' := by linarith [r'mem.1]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
A : x + r / 2 ≤ x + r'
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
hr' _ ((Icc_subset_Icc le_rfl A) hy) _ ((Icc_subset_Icc le_rfl A) hz)

Premises used: le_rfl, Set.Icc_subset_Icc
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
A : x + r / 2 ≤ x + r'
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
exact hr' _ ((Icc_subset_Icc le_rfl A) hy) _ ((Icc_subset_Icc le_rfl A) hz)

Premises used: le_rfl, Set.Icc_subset_Icc
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
⊢ HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x

Tactic:
have := hx.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖

Tactic:
simp_rw [hasDerivWithinAt_iff_isLittleO, isLittleO_iff] at this

Premises used: hasDerivWithinAt_iff_isLittleO, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
rcases :
  ∀ (m : ℝ) (xm : m ∈ Ioi x)
    (hm :
      Ico x m ⊆
        {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}),
    ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε

Tactic:
rcases mem_nhdsGE_iff_exists_Ico_subset.1 (this (half_pos hε)) with ⟨m, xm, hm⟩

Premises used: half_pos, mem_nhdsGE_iff_exists_Ico_subset, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
linarith : m - x ≤ 0 → m - x - 0 + (x - m) = 0
⊢ m - x > 0

Tactic:
linarith [show x < m from xm]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
refine : ∀ (r : ℝ) (hr : r ∈ Ioo 0 (m - x)), x ∈ A f (derivWithin f (Ici x) x) r ε
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε

Tactic:
refine ⟨m - x, by linarith [show x < m from xm], fun r hr => ?_⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
⊢ r ∈ Ioc (r / 2) r

Tactic:
have : r ∈ Ioc (r / 2) r := ⟨half_lt_self hr.1, le_rfl⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
⊢ x ∈ A f (derivWithin f (Ici x) x) r ε

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

Premises used: Set.Mem, setOf, And.intro, Exists.intro, RightDerivMeasurableAux.A
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
refine :
  ∀ (y : ℝ) (hy : y ∈ Icc x (x + r)) (z : ℝ) (hz : z ∈ Icc x (x + r)),
    ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ ≤ ε * r
⊢ x ∈ A f (derivWithin f (Ici x) x) r ε

Tactic:
refine ⟨r, this, fun y hy z hz => ?_⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
e_a :
  f z - f y - (z - y) • derivWithin f (Ici x) x =
    f z - f x - (z - x) • derivWithin f (Ici x) x - (f y - f x - (y - x) • derivWithin f (Ici x) x)
⊢ ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
    ‖f z - f x - (z - x) • derivWithin f (Ici x) x - (f y - f x - (y - x) • derivWithin f (Ici x) x)‖

Tactic:
congr 1