-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem totalVariation_absolutelyContinuous_iff (s : SignedMeasure α) (μ : Measure α) :
    s.totalVariation ≪ μ ↔
      s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ

Proof state:
case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.posPart S = 0

case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Tactic:
exacts [this.1, this.2]

Result:
no goals

Proof state:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.totalVariation S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Tactic:
rw [totalVariation, Measure.add_apply, add_eq_zero] at this

Result:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Proof state:
case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ

case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.negPart ≪ μ

Tactic:
all_goals
  refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
  have := h hS₂
  rw [totalVariation, Measure.add_apply, add_eq_zero] at this

Result:
case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.posPart S = 0

case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Proof state:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.negPart ≪ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Result:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Proof state:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Tactic:
have := h hS₂

Result:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.totalVariation S = 0
⊢ s.toJordanDecomposition.negPart S = 0

Proof state:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
⊢ s.totalVariation S = 0

Tactic:
rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ

Tactic:
constructor

Result:
case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ

case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.negPart ≪ μ

Proof state:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ s.totalVariation ≪ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Result:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
⊢ s.totalVariation S = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.totalVariation ≪ μ ↔ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ

case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ s.totalVariation ≪ μ