-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_mutuallySingular (s : SignedMeasure α) (μ : Measure α) :
    s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ
      s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case neg.inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hn : ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
⊢ (if h : s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ then (Classical.choose ⋯).1 else 0) ⟂ₘ 0

Tactic:
exact MutuallySingular.zero_right

Result:
no goals

Proof state:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos :
  (s.toJordanDecomposition.posPart.singularPart μ) i = 0 ∧
    (μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)) i = 0
hneg :
  (s.toJordanDecomposition.negPart.singularPart μ) iᶜ = 0 ∧
    (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)) iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
exact ⟨i, hi, hpos.1, hneg.1⟩

Result:
no goals

Proof state:
case neg.inl
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hp : ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
⊢ 0 ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
exact MutuallySingular.zero_left

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
by_cases hl : s.HaveLebesgueDecomposition μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

case neg
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : ¬s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case neg.inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hn : ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [Measure.singularPart, Measure.singularPart, dif_neg hn]

Result:
case neg.inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hn : ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
⊢ (if h : s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ then (Classical.choose ⋯).1 else 0) ⟂ₘ 0

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
obtain ⟨i, hi, hpos, hneg⟩ := s.toJordanDecomposition.mutuallySingular

Result:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos : s.toJordanDecomposition.posPart i = 0
hneg : s.toJordanDecomposition.negPart iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case neg.inl
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hp : ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [Measure.singularPart, dif_neg hp]

Result:
case neg.inl
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hp : ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
⊢ 0 ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos :
  (s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)) i = 0
hneg :
  (s.toJordanDecomposition.negPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)) iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [add_apply, add_eq_zero] at hpos hneg

Result:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos :
  (s.toJordanDecomposition.posPart.singularPart μ) i = 0 ∧
    (μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)) i = 0
hneg :
  (s.toJordanDecomposition.negPart.singularPart μ) iᶜ = 0 ∧
    (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)) iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos :
  (s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)) i = 0
hneg : s.toJordanDecomposition.negPart iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ] at hneg

Result:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos :
  (s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)) i = 0
hneg :
  (s.toJordanDecomposition.negPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)) iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : ¬s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [not_haveLebesgueDecomposition_iff] at hl

Result:
case neg
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl :
  ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨
    ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos : s.toJordanDecomposition.posPart i = 0
hneg : s.toJordanDecomposition.negPart iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ] at hpos

Result:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl : s.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
hpos :
  (s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)) i = 0
hneg : s.toJordanDecomposition.negPart iᶜ = 0
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ