awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
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 ∈ Iio x
⊢ y - x < 0

Tactic:
rw [mem_Iio, ← sub_neg] at hy

Premises used: sub_neg, Set.mem_Iio
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
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 - x < 0
h : f y - f x ≤ (↑hf.stieltjesFunction : ℝ → ℝ) y - f x
⊢ ((↑hf.stieltjesFunction : ℝ → ℝ) y - f x) / (y - x) ≤ (f y - f x) / (y - x)

Tactic:
apply div_le_div_of_nonpos_of_le hy.le

Premises used: div_le_div_of_nonpos_of_le, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
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 - x < 0
⊢ f y - f x ≤ (↑hf.stieltjesFunction : ℝ → ℝ) y - f x

Tactic:
(sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))

Premises used: Iff.mpr, le_refl, sub_le_sub_iff_right, Monotone.le_rightLim
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
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 - x < 0
⊢ f y - f x ≤ (↑hf.stieltjesFunction : ℝ → ℝ) y - f x

Tactic:
exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))

Premises used: Iff.mpr, le_refl, sub_le_sub_iff_right, Monotone.le_rightLim
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
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)
h :
  ∀ a ∈ Iio x,
    (f a - f x) / (a - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) (a + -1 * HPow.hPow (β := ℕ) (a - x) 2) - f x) / (a - x)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x,
    (f b - f x) / (b - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) (b + -1 * HPow.hPow (β := ℕ) (b - x) 2) - f x) / (b - x)

Tactic:
filter_upwards [self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
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 - x < 0
⊢ 0 < HPow.hPow (β := ℕ) (y - x) 2

Tactic:
have : 0 < (y - x) ^ 2 := sq_pos_of_neg hy
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
this_1 :
  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 - x < 0
this : 0 < HPow.hPow (β := ℕ) (y - x) 2
h : (↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x ≤ f y - f x
⊢ (f y - f x) / (y - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x)

Tactic:
apply div_le_div_of_nonpos_of_le hy.le

Premises used: div_le_div_of_nonpos_of_le, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
this_1 :
  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 - x < 0
this : 0 < HPow.hPow (β := ℕ) (y - x) 2
linarith :
  y ≤ y + -1 * HPow.hPow (β := ℕ) (y - x) 2 →
    0 - HPow.hPow (β := ℕ) (y - x) 2 + (y - (y + -1 * HPow.hPow (β := ℕ) (y - x) 2)) = 0
⊢ y + -1 * HPow.hPow (β := ℕ) (y - x) 2 < y

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
this_1 :
  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 - x < 0
this : 0 < HPow.hPow (β := ℕ) (y - x) 2
⊢ (↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x ≤ f y - f x

Tactic:
exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by linarith))

Premises used: Iff.mpr, sub_le_sub_iff_right, Monotone.rightLim_le
-- Module: Mathlib.Analysis.Calculus.Monotone
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)

Tactic:
have L2 : 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 (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
    -- apply the sandwiching argument, with `g` and the helper function
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this
    · filter_upwards [self_mem_nhdsWithin]
      rintro y hy
      rw [mem_Iio, ← sub_neg] at hy
      apply div_le_div_of_nonpos_of_le hy.le
      exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))
    · filter_upwards [self_mem_nhdsWithin]
      rintro y hy
      rw [mem_Iio, ← sub_neg] at hy
      have : 0 < (y - x) ^ 2 := sq_pos_of_neg hy
      apply div_le_div_of_nonpos_of_le hy.le
      exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by linarith))
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
L2 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h :
  Tendsto (fun (b : ℝ) ↦ (f b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ (f b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ HasDerivAt f (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x

Tactic:
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, ← nhdsLT_sup_nhdsGT, tendsto_sup]

Premises used: Filter.tendsto_sup, slope_fun_def_field, hasDerivAt_iff_tendsto_slope, nhdsLT_sup_nhdsGT
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
L2 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (b : ℝ) ↦ (f b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ (f b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)

Tactic:
⟨L2, L1⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
L2 :
  Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
⊢ Tendsto (fun (b : ℝ) ↦ (f b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ (f b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)

Tactic:
exact ⟨L2, L1⟩
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt f (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
⊢ DifferentiableAt ℝ f x

Tactic:
hx.differentiableAt

Premises used: HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
hf : Monotone f
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  HasDerivAt f
                    (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume
                        x).toReal
                    x)
                x}
            x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ DifferentiableAt ℝ f x) x} x}
      a
h₁ h₂ :
  ∀ (x : ℝ)
    (hx :
      HasDerivAt f
        (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x),
    DifferentiableAt ℝ f x
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

Tactic:
filter_upwards [hf.ae_hasDerivAt] with x hx using hx.differentiableAt

Premises used: Monotone.ae_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
apply ae_of_mem_of_ae_of_mem_inter_Ioo

Premises used: ae_of_mem_of_ae_of_mem_inter_Ioo
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h : a < b → ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
⊢ a < b → ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h : a < b
⊢ ∃ (g : ℝ → ℝ), Monotone g ∧ EqOn f g (s ∩ Icc a b)

Tactic:
(hf.mono inter_subset_left).exists_monotone_extension
      (hf.map_bddBelow inter_subset_left ⟨a, fun x hx => hx.2.1, as⟩)
      (hf.map_bddAbove inter_subset_left ⟨b, fun x hx => hx.2.2, bs⟩)

Premises used: MonotoneOn.map_bddAbove, Set.inter_subset_left, And.right, And.left, And.intro, MonotoneOn.map_bddBelow, Exists.intro, MonotoneOn.exists_monotone_extension, MonotoneOn.mono
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h_1 : a < b
h :
  ∀ (g : ℝ → ℝ) (hg : Monotone g) (gf : EqOn f g (s ∩ Icc a b)),
    ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x

Tactic:
obtain ⟨g, hg, gf⟩ : ∃ g : ℝ → ℝ, Monotone g ∧ EqOn f g (s ∩ Icc a b) :=
    (hf.mono inter_subset_left).exists_monotone_extension
      (hf.map_bddBelow inter_subset_left ⟨a, fun x hx => hx.2.1, as⟩)
      (hf.map_bddAbove inter_subset_left ⟨b, fun x hx => hx.2.2, bs⟩)

Premises used: MonotoneOn.map_bddAbove, Set.inter_subset_left, And.intro, MonotoneOn.map_bddBelow, Exists.intro, MonotoneOn.exists_monotone_extension, MonotoneOn.mono
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h_1 : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
h : ∀ (x : ℝ) (hx : DifferentiableAt ℝ g x), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [hg.ae_differentiableAt] with x hx

Premises used: Monotone.ae_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
apply : f =ᶠ[𝓝[s] x] g
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
apply hx.differentiableWithinAt.congr_of_eventuallyEq _ (gf ⟨h'x.1, h'x.2.1.le, h'x.2.2.le⟩)

Premises used: DifferentiableAt.differentiableWithinAt, LT.lt.le, DifferentiableWithinAt.congr_of_eventuallyEq, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
⊢ Ioo a b ∈ 𝓝[s] x

Tactic:
have : Ioo a b ∈ 𝓝[s] x := nhdsWithin_le_nhds (Ioo_mem_nhds h'x.2.1 h'x.2.2)
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h_1 : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
this : Ioo a b ∈ 𝓝[s] x
h : ∀ (y : ℝ) (hy : y ∈ s) (h'y : y ∈ Ioo a b), f y = g y
⊢ f =ᶠ[𝓝[s] x] g

Tactic:
filter_upwards [self_mem_nhdsWithin, this] with y hy h'y

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
this : Ioo a b ∈ 𝓝[s] x
y : ℝ
hy : y ∈ s
h'y : y ∈ Ioo a b
⊢ f y = g y

Tactic:
gf ⟨hy, h'y.1.le, h'y.2.le⟩

Premises used: LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
h : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
this : Ioo a b ∈ 𝓝[s] x
y : ℝ
hy : y ∈ s
h'y : y ∈ Ioo a b
⊢ f y = g y

Tactic:
exact gf ⟨hy, h'y.1.le, h'y.2.le⟩

Premises used: LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
rw : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume s, DifferentiableWithinAt ℝ f s x

Tactic:
rw [ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
hf.ae_differentiableWithinAt_of_mem

Premises used: MonotoneOn.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
exact hf.ae_differentiableWithinAt_of_mem

Premises used: MonotoneOn.ae_differentiableWithinAt_of_mem