-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem absolutelyContinuous_ennreal_iff (s : SignedMeasure α) (μ : VectorMeasure α ℝ≥0∞) :
    s ≪ᵥ μ ↔ s.totalVariation ≪ μ.ennrealToMeasure

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
⊢ s.totalVariation ≪ μ.ennrealToMeasure

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

Result:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ s.totalVariation S = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s ≪ᵥ μ ↔ s.totalVariation ≪ μ.ennrealToMeasure

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
⊢ s.totalVariation ≪ μ.ennrealToMeasure

case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
⊢ s ≪ᵥ μ

Proof state:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ ↑s S = 0

Tactic:
exact null_of_totalVariation_zero s (h hS₂)

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s_1 : Set α⦄, μ.ennrealToMeasure s_1 = 0 → ↑s s_1 = 0
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ ↑⟨↑s (i ∩ S), ⋯⟩ + ↑⟨-↑s (iᶜ ∩ S), ⋯⟩ = 0

Tactic:
simp [h (measure_mono_null (i.inter_subset_right) hS₂),
  h (measure_mono_null (iᶜ.inter_subset_right) hS₂)]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ s.totalVariation S = 0

Tactic:
rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hS₁,
  toMeasureOfLEZero_apply _ _ _ hS₁]

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ ↑⟨↑s (i ∩ S), ⋯⟩ + ↑⟨-↑s (iᶜ ∩ S), ⋯⟩ = 0

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ s.totalVariation S = 0

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ s.totalVariation S = 0

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ ↑⟨↑s (i ∩ S), ⋯⟩ + ↑⟨-↑s (iᶜ ∩ S), ⋯⟩ = 0

Tactic:
rw [← VectorMeasure.AbsolutelyContinuous.ennrealToMeasure] at h

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s_1 : Set α⦄, μ.ennrealToMeasure s_1 = 0 → ↑s s_1 = 0
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ ↑⟨↑s (i ∩ S), ⋯⟩ + ↑⟨-↑s (iᶜ ∩ S), ⋯⟩ = 0

Proof state:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
⊢ s ≪ᵥ μ

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

Result:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑μ S = 0
⊢ ↑s S = 0

Proof state:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑μ S = 0
⊢ ↑s S = 0

Tactic:
rw [← VectorMeasure.ennrealToMeasure_apply hS₁] at hS₂

Result:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ ↑s S = 0