awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
have this : Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
  (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
Tactic: have : Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
        (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
      apply tendsto_apply_add_mul_sq_div_sub (nhdsGT_le_nhdsNE x) hx.2
      apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
      · apply Tendsto.mono_left _ nhdsWithin_le_nhds
        have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
          tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
        simpa using this
      · filter_upwards [Ioo_mem_nhdsGT <| show x < x + 1 by simp]
        rintro y ⟨hy : x < y, h'y : y < x + 1⟩
        rw [mem_Ioi]
        nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
have hgf : ∀ᶠ (b : ℝ) in 𝓝[>] x,
  ((↑hf.stieltjesFunction : ℝ → ℝ) (b + -1 * HPow.hPow (β := ℕ) (b - x) 2) - f x) / (b - x) ≤ (f b - f x) / (b - x)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
hgf :
  ∀ᶠ (b : ℝ) in 𝓝[>] x,
    ((↑hf.stieltjesFunction : ℝ → ℝ) (b + -1 * HPow.hPow (β := ℕ) (b - x) 2) - f x) / (b - x) ≤ (f b - f x) / (b - x)
⊢ Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
have hfh : ∀ᶠ (b : ℝ) in 𝓝[>] x, (f b - f x) / (b - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] x,
    ((↑hf.stieltjesFunction : ℝ → ℝ) (b + -1 * HPow.hPow (β := ℕ) (b - x) 2) - f x) / (b - x) ≤ (f b - f x) / (b - x)
have h : ∀ (y : ℝ) (hy : y ∈ Ioi x),
  ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
y : ℝ
hy : y ∈ Ioi x
⊢ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
have hy₁ : 0 < y - x
Tactic: rw [mem_Ioi, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
y : ℝ
hy : 0 < y - x
⊢ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
have h : (↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) ≤ f y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
y : ℝ
hy : 0 < y - x
⊢ y + -1 * HPow.hPow (β := ℕ) (y - x) 2 < y
have nlinarith : y ≤ y + -1 * HPow.hPow (β := ℕ) (y - x) 2 →
  y - (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) + (0 - (0 - (y - x)) * (0 - (y - x))) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] x, (f b - f x) / (b - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)
have h : ∀ (y : ℝ) (hy : y ∈ Ioi x), (f y - f x) / (y - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) y - f x) / (y - x)
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
y : ℝ
hy : y ∈ Ioi x
⊢ (f y - f x) / (y - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) y - f x) / (y - x)
have hy₁ : 0 < y - x
Tactic: rw [mem_Ioi, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
this :
  Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
y : ℝ
hy : 0 < y - x
⊢ (f y - f x) / (y - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) y - f x) / (y - x)
have h : f y ≤ (↑hf.stieltjesFunction : ℝ → ℝ) y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ HasDerivAt f (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
have L1 : Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
  (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
Tactic: have L1 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x)
      (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
    -- limit of a helper function, with a small shift compared to `g`
    have : Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
        (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
      apply tendsto_apply_add_mul_sq_div_sub (nhdsGT_le_nhdsNE x) hx.2
      apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
      · apply Tendsto.mono_left _ nhdsWithin_le_nhds
        have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
          tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
        simpa using this
      · filter_upwards [Ioo_mem_nhdsGT <| show x < x + 1 by simp]
        rintro y ⟨hy : x < y, h'y : y < x + 1⟩
        rw [mem_Ioi]
        nlinarith
    -- apply the sandwiching argument, with the helper function and `g`
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
    · filter_upwards [self_mem_nhdsWithin] with y hy
      rw [mem_Ioi, ← sub_pos] at hy
      gcongr
      exact hf.rightLim_le (by nlinarith)
    · filter_upwards [self_mem_nhdsWithin] with y hy
      rw [mem_Ioi, ← sub_pos] at hy
      gcongr
      exact hf.le_rightLim le_rfl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[<] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
have apply : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝[<] x)
Tactic: apply tendsto_apply_add_mul_sq_div_sub (nhdsLT_le_nhdsNE x) hx.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝[<] x)
have h1 : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝 x)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h1 : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝 x)
⊢ Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝[<] x)
have h2 : ∀ᶠ (x_1 : ℝ) in 𝓝[<] x, x_1 + -1 * HPow.hPow (β := ℕ) (x_1 - x) 2 ∈ Iio x
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝 x)
have apply : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 x)
Tactic: apply Tendsto.mono_left _ nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 x)
have this : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 (x + -1 * HPow.hPow (β := ℕ) (x - x) 2))
Tactic: have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
          tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] x, x_1 + -1 * HPow.hPow (β := ℕ) (x_1 - x) 2 ∈ Iio x
have h : ∀ a ∈ Ioo (x - 1) x, a + -1 * HPow.hPow (β := ℕ) (a - x) 2 ∈ Iio x
Tactic: filter_upwards [Ioo_mem_nhdsLT <| show x - 1 < x by simp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
y : ℝ
hy : y ∈ Ioo (x - 1) x
⊢ y + -1 * HPow.hPow (β := ℕ) (y - x) 2 ∈ Iio x
have hy₁ : x - 1 < y ∧ y < x
Tactic: rw [mem_Ioo] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
y : ℝ
hy : x - 1 < y ∧ y < x
⊢ y + -1 * HPow.hPow (β := ℕ) (y - x) 2 < x
have nlinarith : x ≤ y + -1 * HPow.hPow (β := ℕ) (y - x) 2 →
  0 - HPow.hPow (β := ℕ) (y - x) 2 + (y - x) + (x - (y + -1 * HPow.hPow (β := ℕ) (y - x) 2)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
L1 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
have this : Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
  (𝓝[<] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
Tactic: have : Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
        (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
      apply tendsto_apply_add_mul_sq_div_sub (nhdsLT_le_nhdsNE x) hx.1
      apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
      · apply Tendsto.mono_left _ nhdsWithin_le_nhds
        have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
          tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
        simpa using this
      · filter_upwards [Ioo_mem_nhdsLT <| show x - 1 < x by simp]
        rintro y hy
        rw [mem_Ioo] at hy
        rw [mem_Iio]
        nlinarith