Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
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) + ofReal (leftLim (↑f) b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

pp: case inr.hp
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
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

pp: case inr.hq
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
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:
add_comm

Goal state after:
case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
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
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
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
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
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