-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem abs_toReal_measure_sub_le_measure_symmDiff'
    (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (hs' : μ s ≠ ∞) (ht' : μ t ≠ ∞) :
    |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
⊢ (μ s).toReal - (μ t).toReal = (μ (s ∪ t)).toReal - (μ t).toReal - ((μ (s ∪ t)).toReal - (μ s).toReal)

Tactic:
abel

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Tactic:
suffices (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal by
  rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]
  convert abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal <;> simp

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
⊢ (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Tactic:
have hst : μ (s \ t) ≠ ∞ := (measure_lt_top_of_subset diff_subset hs').ne

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
⊢ (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal

Tactic:
rw [measure_diff' s ht ht', measure_diff' t hs hs',
  ENNReal.toReal_sub_of_le measure_le_measure_union_right (measure_union_ne_top hs' ht'),
  ENNReal.toReal_sub_of_le measure_le_measure_union_right (measure_union_ne_top ht' hs'),
  union_comm t s]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
⊢ (μ s).toReal - (μ t).toReal = (μ (s ∪ t)).toReal - (μ t).toReal - ((μ (s ∪ t)).toReal - (μ s).toReal)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Tactic:
rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ |(μ (s \ t)).toReal - (μ (t \ s)).toReal| ≤ (μ (s \ t)).toReal + (μ (t \ s)).toReal

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ |(μ (s \ t)).toReal - (μ (t \ s)).toReal| ≤ (μ (s \ t)).toReal + (μ (t \ s)).toReal

Tactic:
convert abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal <;> simp

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Tactic:
have hts : μ (t \ s) ≠ ∞ := (measure_lt_top_of_subset diff_subset ht').ne

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ⊤
ht' : μ t ≠ ⊤
hst : μ (s \ t) ≠ ⊤
hts : μ (t \ s) ≠ ⊤
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal