-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_Ioo {a b : ℝ} : f.measure (Ioo a b) = ofReal (leftLim f b - f a)

Proof state:
f : StieltjesFunction
a b : ℝ
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
rcases le_or_lt b a with (hab | hab)

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
simp only [hab, measure_empty, Ioo_eq_empty, not_lt]

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - ↑f a)

Proof state:
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ Disjoint (Ioo a b) {b}

Tactic:
simp

Result:
no goals

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
symm

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - ↑f a) = 0

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
have D : f b - f a = f b - leftLim f b + (leftLim f b - f a) := by abel

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
have A : Disjoint (Ioo a b) {b} := by simp

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - ↑f a) = 0

Tactic:
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim_le hab]

Result:
no goals

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
rw [D, ENNReal.ofReal_add, add_comm] at this

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ofReal (↑f b - leftLim (↑f) b) + f.measure (Ioo a b) = ofReal (↑f b - leftLim (↑f) b) + ofReal (leftLim (↑f) b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

case inr.hp
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ ↑f b - leftLim (↑f) b

case inr.hq
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ leftLim (↑f) b - ↑f a

Proof state:
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)

Tactic:
abel

Result:
no goals

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ofReal (↑f b - leftLim (↑f) b) + f.measure (Ioo a b) = ofReal (↑f b - leftLim (↑f) b) + ofReal (leftLim (↑f) b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
simpa only [ENNReal.add_right_inj ENNReal.ofReal_ne_top]

Result:
no goals

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
have := f.measure_Ioc a b

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioc a b) = ofReal (↑f b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioc a b) = ofReal (↑f b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton,
  measure_union A (measurableSet_singleton b), Icc_self] at this

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Proof state:
case inr.hp
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ ↑f b - leftLim (↑f) b

Tactic:
simp only [f.mono.leftLim_le le_rfl, sub_nonneg]

Result:
no goals

Proof state:
case inr.hq
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ leftLim (↑f) b - ↑f a

Tactic:
simp only [f.mono.le_leftLim hab, sub_nonneg]

Result:
no goals