-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem mutuallySingular_iff (s t : SignedMeasure α) :
    s ⟂ᵥ t ↔ s.totalVariation ⟂ₘ t.totalVariation

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, ↑t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ t.totalVariation uᶜ = 0

Tactic:
rw [totalVariation, Measure.add_apply, hjpos, hjneg,
  toMeasureOfZeroLE_apply _ _ _ hmeas.compl,
  toMeasureOfLEZero_apply _ _ _ hmeas.compl]

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, ↑t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ ↑⟨↑t (j ∩ uᶜ), ⋯⟩ + ↑⟨-↑t (jᶜ ∩ uᶜ), ⋯⟩ = 0

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
⊢ s ⟂ᵥ t → s.totalVariation ⟂ₘ t.totalVariation

Tactic:
rintro ⟨u, hmeas, hu₁, hu₂⟩

Result:
case mp.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, ↑t t_1 = 0
⊢ s.totalVariation ⟂ₘ t.totalVariation

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, ↑t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ s.totalVariation u = 0

Tactic:
rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
  toMeasureOfLEZero_apply _ _ _ hmeas]

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, ↑t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ ↑⟨↑s (i ∩ u), ⋯⟩ + ↑⟨-↑s (iᶜ ∩ u), ⋯⟩ = 0