-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_Ici {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : ℝ) :
    f.measure (Ici x) = ofReal (l - leftLim f x)

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a - 1

Tactic:
exact fun y => ⟨y + 1, fun z hyz => by rwa [le_sub_iff_add_le]⟩

Result:
no goals

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (leftLim ↑f) atTop (𝓝 l)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le (hf.comp ?_) hf h_le1 h_le2

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun i => i - 1) atTop atTop

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => f.measure (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))

Tactic:
simp_rw [measure_Ico]

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (leftLim (↑f) x_1 - leftLim (↑f) x)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ f.measure (Ici x) = ofReal (l - leftLim (↑f) x)

Tactic:
refine tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) ?_

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => f.measure (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
y z : ℝ
hyz : y + 1 ≤ z
⊢ y ≤ z - 1

Tactic:
rwa [le_sub_iff_add_le]

Result:
no goals

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
⊢ Tendsto (leftLim ↑f) atTop (𝓝 l)

Tactic:
have h_le2 : ∀ x, leftLim f x ≤ f x := fun x => Monotone.leftLim_le f.mono le_rfl

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (leftLim ↑f) atTop (𝓝 l)

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (leftLim ↑f) atTop (𝓝 l)

Tactic:
have h_le1 : ∀ x, f (x - 1) ≤ leftLim f x := fun x => Monotone.le_leftLim f.mono (sub_one_lt x)

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
⊢ Tendsto (leftLim ↑f) atTop (𝓝 l)

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (leftLim (↑f) x_1 - leftLim (↑f) x)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))

Tactic:
refine ENNReal.tendsto_ofReal (Tendsto.sub_const ?_ _)

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (leftLim ↑f) atTop (𝓝 l)

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun i => i - 1) atTop atTop

Tactic:
rw [tendsto_atTop_atTop]

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a - 1