-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma eq_of_measure_of_tendsto_atBot (g : StieltjesFunction) {l : ℝ}
    (hfg : f.measure = g.measure) (hfl : Tendsto f atBot (𝓝 l)) (hgl : Tendsto g atBot (𝓝 l)) :
    f = g

Proof state:
case h.hq
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ l ≤ ↑f x

Tactic:
exact Monotone.le_of_tendsto f.mono hfl x

Result:
no goals

Proof state:
case h.hp
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ 0 ≤ ↑g x - l

Tactic:
rw [sub_nonneg]

Result:
case h.hp
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ l ≤ ↑g x

Proof state:
case h
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ↑f x - l = ↑g x - l
⊢ ↑f x = ↑g x

Tactic:
simpa using hf

Result:
no goals

Proof state:
case h.hp
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ l ≤ ↑g x

Tactic:
exact Monotone.le_of_tendsto g.mono hgl x

Result:
no goals

Proof state:
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
⊢ f = g

Tactic:
ext x

Result:
case h
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
⊢ ↑f x = ↑g x

Proof state:
case h
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : f.measure (Iic x) = ofReal (↑f x - l)
⊢ ↑f x = ↑g x

Tactic:
rw [hfg, measure_Iic g hgl x, ENNReal.ofReal_eq_ofReal_iff, eq_comm] at hf

Result:
case h
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ↑f x - l = ↑g x - l
⊢ ↑f x = ↑g x

case h.hp
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ 0 ≤ ↑g x - l

case h.hq
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ 0 ≤ ↑f x - l

Proof state:
case h
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
⊢ ↑f x = ↑g x

Tactic:
have hf := measure_Iic f hfl x

Result:
case h
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : f.measure (Iic x) = ofReal (↑f x - l)
⊢ ↑f x = ↑g x

Proof state:
case h.hq
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ 0 ≤ ↑f x - l

Tactic:
rw [sub_nonneg]

Result:
case h.hq
f g : StieltjesFunction
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ l ≤ ↑f x