-- 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_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

Tactic:
simp [hu₁ _ Set.inter_subset_right]

Result:
no goals

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

Tactic:
constructor

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

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

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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 ⟂ₘ t.totalVariation

Tactic:
refine ⟨u, 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.totalVariation u = 0

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

Proof state:
case mp.intro.intro.intro.intro.intro.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
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₃
⊢ s.totalVariation ⟂ₘ t.totalVariation

Tactic:
obtain ⟨j, hj₁, hj₂, hj₃, hjpos, hjneg⟩ := t.toJordanDecomposition_spec

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
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 ⟂ₘ 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 (j ∩ uᶜ), ⋯⟩ + ↑⟨-↑t (jᶜ ∩ uᶜ), ⋯⟩ = 0

Tactic:
simp [hu₂ _ Set.inter_subset_right]

Result:
no goals

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : s.totalVariation u = 0
hu₂ : t.totalVariation uᶜ = 0
⊢ s ⟂ᵥ t

Tactic:
exact
  ⟨u, hmeas, fun t htu => null_of_totalVariation_zero _ (measure_mono_null htu hu₁),
    fun t htv => null_of_totalVariation_zero _ (measure_mono_null htv hu₂)⟩

Result:
no goals

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

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

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : s.totalVariation u = 0
hu₂ : t.totalVariation uᶜ = 0
⊢ s ⟂ᵥ t

Proof state:
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

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hipos, hineg⟩ := s.toJordanDecomposition_spec

Result:
case mp.intro.intro.intro.intro.intro.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
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₃
⊢ s.totalVariation ⟂ₘ t.totalVariation