-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma eq_of_measure_of_eq (g : StieltjesFunction) {y : ℝ}
    (hfg : f.measure = g.measure) (hy : f y = g y) :
    f = g

Proof state:
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
⊢ ↑f x = ↑g x

Tactic:
have hf := measure_Ioc f y x

Result:
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : f.measure (Ioc y x) = ofReal (↑f x - ↑f y)
⊢ ↑f x = ↑g x

Proof state:
case h.inl.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ ↑f x ≤ ↑f y

Tactic:
exact f.mono hxy

Result:
no goals

Proof state:
case h.inr.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ 0 ≤ ↑f x - ↑f y

Tactic:
rw [sub_nonneg]

Result:
case h.inr.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ ↑f y ≤ ↑f x

Proof state:
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : f.measure (Ioc x y) = ofReal (↑f y - ↑f x)
⊢ ↑f x = ↑g x

Tactic:
rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf

Result:
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ↑g y - ↑f x = ↑g y - ↑g x
⊢ ↑f x = ↑g x

case h.inl.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ 0 ≤ ↑g y - ↑g x

case h.inl.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ 0 ≤ ↑f y - ↑f x

Proof state:
case h.inr.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ ↑f y ≤ ↑f x

Tactic:
exact f.mono hxy

Result:
no goals

Proof state:
case h.inl.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ ↑g x ≤ ↑g y

Tactic:
exact g.mono hxy

Result:
no goals

Proof state:
case h.inr.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ ↑g y ≤ ↑g x

Tactic:
exact g.mono hxy

Result:
no goals

Proof state:
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ↑g y - ↑f x = ↑g y - ↑g x
⊢ ↑f x = ↑g x

Tactic:
simpa using hf

Result:
no goals

Proof state:
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
⊢ f = g

Tactic:
ext x

Result:
case h
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
⊢ ↑f x = ↑g x

Proof state:
case h.inr.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ 0 ≤ ↑g x - ↑g y

Tactic:
rw [sub_nonneg]

Result:
case h.inr.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ ↑g y ≤ ↑g x

Proof state:
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : f.measure (Ioc y x) = ofReal (↑f x - ↑f y)
⊢ ↑f x = ↑g x

Tactic:
rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf

Result:
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ↑f x - ↑g y = ↑g x - ↑g y
⊢ ↑f x = ↑g x

case h.inr.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ 0 ≤ ↑g x - ↑g y

case h.inr.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ 0 ≤ ↑f x - ↑f y

Proof state:
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
⊢ ↑f x = ↑g x

Tactic:
have hf := measure_Ioc f x y

Result:
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : f.measure (Ioc x y) = ofReal (↑f y - ↑f x)
⊢ ↑f x = ↑g x

Proof state:
case h.inl.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ 0 ≤ ↑g y - ↑g x

Tactic:
rw [sub_nonneg]

Result:
case h.inl.hp
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ ↑g x ≤ ↑g y

Proof state:
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ↑f x - ↑g y = ↑g x - ↑g y
⊢ ↑f x = ↑g x

Tactic:
simpa using hf

Result:
no goals

Proof state:
case h.inl.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ 0 ≤ ↑f y - ↑f x

Tactic:
rw [sub_nonneg]

Result:
case h.inl.hq
f g : StieltjesFunction
y : ℝ
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ ↑f x ≤ ↑f y