-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem null_of_totalVariation_zero (s : SignedMeasure α) {i : Set α}
    (hs : s.totalVariation i = 0) : s i = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
⊢ ↑s i = 0

Tactic:
rw [← toSignedMeasure_toJordanDecomposition s, toSignedMeasure, VectorMeasure.coe_sub,
  Pi.sub_apply, Measure.toSignedMeasure_apply, Measure.toSignedMeasure_apply]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
⊢ ((if MeasurableSet i then (s.toJordanDecomposition.posPart i).toReal else 0) -
      if MeasurableSet i then (s.toJordanDecomposition.negPart i).toReal else 0) =
    0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.totalVariation i = 0
⊢ ↑s i = 0

Tactic:
rw [totalVariation, Measure.coe_add, Pi.add_apply, add_eq_zero] at hs

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
⊢ ↑s i = 0

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
hi : ¬MeasurableSet i
⊢ ((if MeasurableSet i then (s.toJordanDecomposition.posPart i).toReal else 0) -
      if MeasurableSet i then (s.toJordanDecomposition.negPart i).toReal else 0) =
    0

Tactic:
simp [if_neg hi]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
hi : MeasurableSet i
⊢ (s.toJordanDecomposition.posPart i).toReal - (s.toJordanDecomposition.negPart i).toReal = 0

Tactic:
simp [hs.1, hs.2]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
⊢ ((if MeasurableSet i then (s.toJordanDecomposition.posPart i).toReal else 0) -
      if MeasurableSet i then (s.toJordanDecomposition.negPart i).toReal else 0) =
    0

Tactic:
by_cases hi : MeasurableSet i

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
hi : MeasurableSet i
⊢ ((if MeasurableSet i then (s.toJordanDecomposition.posPart i).toReal else 0) -
      if MeasurableSet i then (s.toJordanDecomposition.negPart i).toReal else 0) =
    0

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
hi : ¬MeasurableSet i
⊢ ((if MeasurableSet i then (s.toJordanDecomposition.posPart i).toReal else 0) -
      if MeasurableSet i then (s.toJordanDecomposition.negPart i).toReal else 0) =
    0

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
hi : MeasurableSet i
⊢ ((if MeasurableSet i then (s.toJordanDecomposition.posPart i).toReal else 0) -
      if MeasurableSet i then (s.toJordanDecomposition.negPart i).toReal else 0) =
    0

Tactic:
rw [if_pos hi, if_pos hi]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0
hi : MeasurableSet i
⊢ (s.toJordanDecomposition.posPart i).toReal - (s.toJordanDecomposition.negPart i).toReal = 0