awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ StronglyMeasurable (deriv f)
have this : let this := borel F;
BorelSpace F
Tactic: borelize F
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ StronglyMeasurable (deriv f)
have inl : ∀ (h𝕜 : SecondCountableTopology 𝕜), StronglyMeasurable (deriv f)
Tactic: rcases h.out with h𝕜 | hF
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ StronglyMeasurable (deriv f)
have inr : ∀ (hF : SecondCountableTopology F), StronglyMeasurable (deriv f)
Tactic: rcases h.out with h𝕜 | hF
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x : ℝ
hx : x ∈ A f L r ε
⊢ A f L r ε ∈ 𝓝[>] x
have 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
Tactic: rcases hx with ⟨r', rr', hr'⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ A f L r ε ∈ 𝓝[>] x
have obtain : ∀ (s : ℝ) (s_gt : r / 2 < s) (s_lt : s < r'), A f L r ε ∈ 𝓝[>] x
Tactic: obtain ⟨s, s_gt, s_lt⟩ : ∃ s : ℝ, r / 2 < s ∧ s < r' := exists_between rr'.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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'
⊢ A f L r ε ∈ 𝓝[>] x
have this : s ∈ Ioc (r / 2) r
Tactic: have : s ∈ Ioc (r / 2) r := ⟨s_gt, le_of_lt (s_lt.trans_le rr'.2)⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 < x + r' - s
have linarith : x + r' - s ≤ x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x < x + r' - s
have linarith₁ : x + r' - s ≤ x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x < x + r' - s
have linarith₂ : x + r' - s ≤ x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x < x + r' - s
have linarith₃ : x + r' - s ≤ x → s - r' + (x + r' - s - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ A f L r ε ∈ 𝓝[>] x
have h : ∀ (x' : ℝ) (hx' : x' ∈ Ioo x (x + r' - s)), x' ∈ A f L r ε
Tactic: filter_upwards [Ioo_mem_nhdsGT <| show x < x + r' - s by linarith] with x' hx'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ x' ∈ A f L r ε
have right : ∀ y ∈ Icc x' (x' + s), ∀ z ∈ Icc x' (x' + s), ‖f z - f y - (z - y) • L‖ ≤ ε * r
Tactic: use s, this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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')
have apply : x' + s ≤ x + r'
Tactic: apply Icc_subset_Icc hx'.1.le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ x' + s ≤ x + r'
have linarith : x + r' < x' + s → 2 / 2 = 1
Tactic: linarith [hx'.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x' + s ≤ x + r'
have linarith₁ : x + r' < x' + s → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hx'.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x' + s ≤ x + r'
have linarith₂ : x + r' < x' + s → GT.gt (α := ℝ) 2 0
Tactic: linarith [hx'.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x' + s ≤ x + r'
have linarith₃ : x + r' < x' + s → x + r' - (x' + s) + (x' - (x + r' - s)) = 0
Tactic: linarith [hx'.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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)
⊢ ∀ y ∈ Icc x' (x' + s), ∀ z ∈ Icc x' (x' + s), ‖f z - f y - (z - y) • L‖ ≤ ε * r
have A : 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 ε
⊢ B f K r s ε ∈ 𝓝[>] x
have obtain : ∀ (L : F) (LK : L ∈ K) (hL₁ : x ∈ A f L r ε) (hL₂ : x ∈ A f L s ε), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 ε
⊢ B f K r s ε ∈ 𝓝[>] x
have h : ∀ (y : ℝ) (hy₁ : y ∈ A f L r ε) (hy₂ : y ∈ A f L s ε), y ∈ B f K r s ε
Tactic: filter_upwards [A_mem_nhdsGT hL₁, A_mem_nhdsGT hL₂] with y hy₁ hy₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 ε
⊢ y ∈ B f K r s ε
have h : ∃ i ∈ K, y ∈ A f i r ε ∧ y ∈ A f i s ε
Tactic: simp only [B, mem_iUnion, mem_inter_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 δ
have refine : ∀ (y : ℝ) (hy : y ∈ Icc x (x + r')) (z : ℝ) (hz : z ∈ Icc x (x + r')), 0 ≤ r
Tactic: refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans (mul_le_mul_of_nonneg_right h ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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')
⊢ 0 ≤ r
have linarith : r < 0 → r - 0 + (x - y) + (y - (x + r')) + (r' - r) = 0
Tactic: linarith [hy.1, hy.2, r'r.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r
have 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
Tactic: rcases hx with ⟨r', r'mem, hr'⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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'
have linarith : x + r' < x + r / 2 → 2 / 2 = 1
Tactic: linarith [r'mem.1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x + r / 2 ≤ x + r'
have linarith₁ : x + r' < x + r / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [r'mem.1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x + r / 2 ≤ x + r'
have linarith₂ : x + r' < x + r / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [r'mem.1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ x + r / 2 ≤ x + r'
have linarith₆ : x + r' < x + r / 2 → 2 * x + 2 * r' - (2 * x + 1 * r) + (1 * r - 2 * r') = 0
Tactic: linarith [r'mem.1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r
have A : x + r / 2 ≤ x + r'
Tactic: have A : x + r / 2 ≤ x + r' := by linarith [r'mem.1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
have this : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
Tactic: have := hx.hasDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
have 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‖
Tactic: simp_rw [hasDerivWithinAt_iff_isLittleO, isLittleO_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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‖
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
have 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 ε
Tactic: rcases mem_nhdsGE_iff_exists_Ico_subset.1 (this (half_pos hε)) with ⟨m, xm, hm⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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}
⊢ m - x > 0
have linarith : m - x ≤ 0 → m - x - 0 + (x - m) = 0
Tactic: linarith [show x < m from xm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
have refine : ∀ (r : ℝ) (hr : r ∈ Ioo 0 (m - x)), x ∈ A f (derivWithin f (Ici x) x) r ε
Tactic: refine ⟨m - x, by linarith [show x < m from xm], fun r hr => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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)
⊢ x ∈ A f (derivWithin f (Ici x) x) r ε
have this₁ : r ∈ Ioc (r / 2) r
Tactic: have : r ∈ Ioc (r / 2) r := ⟨half_lt_self hr.1, le_rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 ε
have 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
Tactic: refine ⟨r, this, fun y hy z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ ‖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)‖
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ 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)
have e_a : f z - f y - (z • derivWithin f (Ici x) x - y • derivWithin f (Ici x) x) =
  f z - f x - (z • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x) -
    (f y - f x - (y • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x))
Tactic: simp only [sub_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ x + r < m
have linarith : m ≤ x + r → m - (x + r) + (r - (m - x)) = 0
Tactic: linarith [hr.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ ≤ ε / 2 * r + ε / 2 * r
have h₁ : ‖z - x‖ ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
h₁ : ‖z - x‖ ≤ r
⊢ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ ≤ ε / 2 * r + ε / 2 * r
have h₂ : ‖y - x‖ ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ ‖z - x‖ ≤ r
have h₁ : z - x ≤ r
Tactic: rw [Real.norm_of_nonneg]