awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
have M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
Tactic: have M :
    ∀ e p q e' p' q',
      n e ≤ p →
        n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e := by
    intro e p q e' p' q' hp hq hp' hq' he'
    let r := max (n e) (n e')
    have I : ((1 : ℝ) / 2) ^ e' ≤ (1 / 2) ^ e :=
      pow_le_pow_of_le_one (by norm_num) (by norm_num) he'
    have J1 : ‖L e p q - L e p r‖ ≤ 4 * (1 / 2) ^ e := by
      have I1 : x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) := (hn e p q hp hq).2.1
      have I2 : x ∈ A f (L e p r) ((1 / 2) ^ p) ((1 / 2) ^ e) := (hn e p r hp (le_max_left _ _)).2.1
      exact norm_sub_le_of_mem_A P _ I1 I2
    have J2 : ‖L e p r - L e' p' r‖ ≤ 4 * (1 / 2) ^ e := by
      have I1 : x ∈ A f (L e p r) ((1 / 2) ^ r) ((1 / 2) ^ e) := (hn e p r hp (le_max_left _ _)).2.2
      have I2 : x ∈ A f (L e' p' r) ((1 / 2) ^ r) ((1 / 2) ^ e') :=
        (hn e' p' r hp' (le_max_right _ _)).2.2
      exact norm_sub_le_of_mem_A P _ I1 (A_mono _ _ I I2)
    have J3 : ‖L e' p' r - L e' p' q'‖ ≤ 4 * (1 / 2) ^ e := by
      have I1 : x ∈ A f (L e' p' r) ((1 / 2) ^ p') ((1 / 2) ^ e') :=
        (hn e' p' r hp' (le_max_right _ _)).2.1
      have I2 : x ∈ A f (L e' p' q') ((1 / 2) ^ p') ((1 / 2) ^ e') := (hn e' p' q' hp' hq').2.1
      exact norm_sub_le_of_mem_A P _ (A_mono _ _ I I1) (A_mono _ _ I I2)
    calc
      ‖L e p q - L e' p' q'‖ =
          ‖L e p q - L e p r + (L e p r - L e' p' r) + (L e' p' r - L e' p' q')‖ := by
        congr 1; abel
      _ ≤ ‖L e p q - L e p r‖ + ‖L e p r - L e' p' r‖ + ‖L e' p' r - L e' p' q'‖ := by
        grw [norm_add_le, norm_add_le]
      _ ≤ 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e := by gcongr
      _ = 12 * (1 / 2) ^ e := by ring
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
⊢ CauchySeq L0
have rw : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (L0 n) (L0 N) < ε
Tactic: rw [Metric.cauchySeq_iff']
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (L0 n) (L0 N) < ε
have obtain : ∀ (e : ℕ) (he : (1 / 2) ^ e < ε / 12), ∃ (N : ℕ), ∀ n ≥ N, dist (L0 n) (L0 N) < ε
Tactic: obtain ⟨e, he⟩ : ∃ e : ℕ, (1 / 2) ^ e < ε / 12 :=
      exists_pow_lt_of_lt_one (div_pos εpos (by norm_num)) (by norm_num)
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / 12
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (L0 n) (L0 N) < ε
have refine : ∀ (e' : ℕ) (he' : e' ≥ e), dist (L0 e') (L0 e) < ε
Tactic: refine ⟨e, fun e' he' => ?_⟩
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / 12
e' : ℕ
he' : e' ≥ e
⊢ dist (L0 e') (L0 e) < ε
have rw : ‖L0 e - L0 e'‖ < ε
Tactic: rw [dist_comm, dist_eq_norm]
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / 12
e' : ℕ
he' : e' ≥ e
⊢ ‖L0 e - L0 e'‖ < ε
have e₁ : 12 * (ε / 12) = ε
Tactic: calc
      ‖L0 e - L0 e'‖ ≤ 12 * (1 / 2) ^ e := M _ _ _ _ _ _ le_rfl le_rfl le_rfl le_rfl he'
      _ < 12 * (ε / 12) := mul_lt_mul' le_rfl he (le_of_lt P) (by norm_num)
      _ = ε := by ring
-- 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
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
have this : CauchySeq L0
Tactic: have : CauchySeq L0 := by
    rw [Metric.cauchySeq_iff']
    intro ε εpos
    obtain ⟨e, he⟩ : ∃ e : ℕ, (1 / 2) ^ e < ε / 12 :=
      exists_pow_lt_of_lt_one (div_pos εpos (by norm_num)) (by norm_num)
    refine ⟨e, fun e' he' => ?_⟩
    rw [dist_comm, dist_eq_norm]
    calc
      ‖L0 e - L0 e'‖ ≤ 12 * (1 / 2) ^ e := M _ _ _ _ _ _ le_rfl le_rfl le_rfl le_rfl he'
      _ < 12 * (ε / 12) := mul_lt_mul' le_rfl he (le_of_lt P) (by norm_num)
      _ = ε := by ring
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
have obtain : ∀ (f' : F) (f'K : f' ∈ K) (hf' : Tendsto L0 atTop (𝓝 f')),
  Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
Tactic: obtain ⟨f', f'K, hf'⟩ : ∃ f' ∈ K, Tendsto L0 atTop (𝓝 f') :=
    cauchySeq_tendsto_of_isComplete hK (fun e => (hn e (n e) (n e) le_rfl le_rfl).1) 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
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
hp : n e ≤ p
⊢ ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
have apply : ∀ᶠ (c : ℕ) in atTop, ‖L e (n e) p - L0 c‖ ≤ 12 * (1 / 2) ^ e
Tactic: apply le_of_tendsto (tendsto_const_nhds.sub hf').norm
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
hp : n e ≤ p
⊢ ∀ᶠ (c : ℕ) in atTop, ‖L e (n e) p - L0 c‖ ≤ 12 * (1 / 2) ^ e
have rw : ∃ (a : ℕ), ∀ b ≥ a, ‖L e (n e) p - L0 b‖ ≤ 12 * (1 / 2) ^ e
Tactic: rw [eventually_atTop]
-- 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
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
have Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
Tactic: have Lf' : ∀ e p, n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e := by
    intro e p hp
    apply le_of_tendsto (tendsto_const_nhds.sub hf').norm
    rw [eventually_atTop]
    exact ⟨e, fun e' he' => M _ _ _ _ _ _ le_rfl hp le_rfl le_rfl he'⟩
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
⊢ HasDerivWithinAt f f' (Ici x) x
have simp : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • f'‖ ≤ c * ‖x_1 - x‖
Tactic: simp only [hasDerivWithinAt_iff_isLittleO, isLittleO_iff]
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • f'‖ ≤ ε * ‖x_1 - x‖
have obtain : ∀ (e : ℕ) (he : (1 / 2) ^ e < ε / 16), ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • f'‖ ≤ ε * ‖x_1 - x‖
Tactic: obtain ⟨e, he⟩ : ∃ e : ℕ, (1 / 2) ^ e < ε / 16 :=
      exists_pow_lt_of_lt_one (div_pos εpos (by norm_num)) (by norm_num)
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • f'‖ ≤ ε * ‖x_1 - x‖
have h : ∀ (y : ℝ) (hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))), ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
Tactic: filter_upwards [Icc_mem_nhdsGE <| show x < x + (1 / 2) ^ (n e + 1) by simp] with y 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have h : ∀ (hy : x ∈ Icc x (x + (1 / 2) ^ (n e + 1))), ‖f x - f x - (x - x) • f'‖ ≤ ε * ‖x - x‖
Tactic: rcases eq_or_lt_of_le hy.1 with (rfl | xy)
Cleared hypotheses: y, 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
h : ∀ (hy : x ∈ Icc x (x + (1 / 2) ^ (n e + 1))), ‖f x - f x - (x - x) • f'‖ ≤ ε * ‖x - x‖
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have h₁ : ∀ (xy : x < y), ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
Tactic: rcases eq_or_lt_of_le hy.1 with (rfl | xy)
-- 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
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have yzero : 0 < y - x
Tactic: have yzero : 0 < y - x := sub_pos.2 xy
-- 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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
⊢ y - x ≤ (1 / 2) ^ (n e + 1)
have linarith : (1 / 2) ^ (n e + 1) < y - x → 16 / 16 = 1
Tactic: linarith [hy.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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
linarith : (1 / 2) ^ (n e + 1) < y - x → 16 / 16 = 1
⊢ y - x ≤ (1 / 2) ^ (n e + 1)
have linarith₁ : (1 / 2) ^ (n e + 1) < y - x → HMul.hMul (α := ℝ) 1 16 = 16
Tactic: linarith [hy.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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
linarith : (1 / 2) ^ (n e + 1) < y - x → 16 / 16 = 1
linarith₁ : (1 / 2) ^ (n e + 1) < y - x → HMul.hMul (α := ℝ) 1 16 = 16
⊢ y - x ≤ (1 / 2) ^ (n e + 1)
have linarith₂ : (1 / 2) ^ (n e + 1) < y - x → GT.gt (α := ℝ) 16 0
Tactic: linarith [hy.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
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
linarith : (1 / 2) ^ (n e + 1) < y - x → 16 / 16 = 1
linarith₁ : (1 / 2) ^ (n e + 1) < y - x → HMul.hMul (α := ℝ) 1 16 = 16
linarith₂ : (1 / 2) ^ (n e + 1) < y - x → GT.gt (α := ℝ) 16 0
⊢ y - x ≤ (1 / 2) ^ (n e + 1)
have linarith₃ : (1 / 2) ^ (n e + 1) < y - x →
  1 * (1 / 2) ^ (n e + 1) - (1 * y - 1 * x) + (1 * y - (1 * x + 1 * (1 / 2) ^ (n e + 1))) = 0
Tactic: linarith [hy.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
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have y_le : y - x ≤ (1 / 2) ^ (n e + 1)
Tactic: have y_le : y - x ≤ (1 / 2) ^ (n e + 1) := by linarith [hy.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
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have yone : y - x ≤ 1
Tactic: have yone : y - x ≤ 1 := le_trans y_le (pow_le_one₀ (by norm_num) (by norm_num))