α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ j₁ = j₂
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
⊢ Injective toSignedMeasure
intro j₁ j₂ hj
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
⊢ j₁ = j₂
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ j₁ = j₂
obtain ⟨S, hS₁, hS₂, hS₃, hS₄, hS₅⟩ := j₁.exists_compl_positive_negative
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₂) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₂) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
⊢ j₁ = j₂
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
⊢ j₁ = j₂
obtain ⟨T, hT₁, hT₂, hT₃, hT₄, hT₅⟩ := j₂.exists_compl_positive_negative
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
⊢ j₁ = j₂
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₂) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₂) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
⊢ j₁ = j₂
rw [← hj] at hT₂ hT₃
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
⊢ j₁ = j₂
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
⊢ j₁ = j₂
obtain ⟨hST₁, -⟩ :=
  of_symmDiff_compl_positive_negative hS₁.compl hT₁.compl ⟨hS₃, (compl_compl S).symm ▸ hS₂⟩
    ⟨hT₃, (compl_compl T).symm ▸ hT₂⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
⊢ j₁.posPart = j₂.posPart
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
⊢ j₁ = j₂
refine' eq_of_posPart_eq_posPart _ hj
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ ↑↑j₁.posPart i = ↑↑j₂.posPart i
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
⊢ j₁.posPart = j₂.posPart
ext1 i hi
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
hμ₂ : ENNReal.toReal (↑↑j₂.posPart i) = ↑(toSignedMeasure j₂) (i ∩ Tᶜ)
⊢ ↑(toSignedMeasure j₁) (i ∩ Sᶜ) = ↑(toSignedMeasure j₁) (i ∩ Tᶜ)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
hμ₂ : ENNReal.toReal (↑↑j₂.posPart i) = ↑(toSignedMeasure j₂) (i ∩ Tᶜ)
⊢ ↑↑j₁.posPart i = ↑↑j₂.posPart i
rw [← ENNReal.toReal_eq_toReal (measure_ne_top _ _) (measure_ne_top _ _), hμ₁, hμ₂, ← hj]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
hμ₂ : ENNReal.toReal (↑↑j₂.posPart i) = ↑(toSignedMeasure j₂) (i ∩ Tᶜ)
⊢ ↑(toSignedMeasure j₁) (i ∩ Sᶜ) = ↑(toSignedMeasure j₁) (i ∩ Tᶜ)
exact of_inter_eq_of_symmDiff_eq_zero_positive hS₁.compl hT₁.compl hi hS₃ hT₃ hST₁
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑j₁.posPart i) = ENNReal.toReal (↑↑j₁.posPart (i ∩ Sᶜ))
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hS₁.compl),
  show j₁.negPart (i ∩ Sᶜ) = 0 from
    nonpos_iff_eq_zero.1 (hS₅ ▸ measure_mono (Set.inter_subset_right _ _)),
  ENNReal.zero_toReal, sub_zero]
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑j₁.posPart (i ∩ S ∪ i ∩ Sᶜ)) = ENNReal.toReal (↑↑j₁.posPart (i ∩ Sᶜ))
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑j₁.posPart i) = ENNReal.toReal (↑↑j₁.posPart (i ∩ Sᶜ))
conv_lhs => rw [← Set.inter_union_compl i S]
case hd
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ Disjoint (i ∩ S) (i ∩ Sᶜ)

case h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ MeasurableSet (i ∩ Sᶜ)
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑j₁.posPart (i ∩ S ∪ i ∩ Sᶜ)) = ENNReal.toReal (↑↑j₁.posPart (i ∩ Sᶜ))
rw [measure_union,
  show j₁.posPart (i ∩ S) = 0 from
    nonpos_iff_eq_zero.1 (hS₄ ▸ measure_mono (Set.inter_subset_right _ _)),
  zero_add]
no goals
case hd
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ Disjoint (i ∩ S) (i ∩ Sᶜ)
refine'
  Set.disjoint_of_subset_left (Set.inter_subset_right _ _)
    (Set.disjoint_of_subset_right (Set.inter_subset_right _ _) disjoint_compl_right)
no goals
case h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ MeasurableSet (i ∩ Sᶜ)
exact hi.inter hS₁.compl
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ ENNReal.toReal (↑↑j₂.posPart i) = ENNReal.toReal (↑↑j₂.posPart (i ∩ Tᶜ))
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ ENNReal.toReal (↑↑j₂.posPart i) = ↑(toSignedMeasure j₂) (i ∩ Tᶜ)
rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hT₁.compl),
  show j₂.negPart (i ∩ Tᶜ) = 0 from
    nonpos_iff_eq_zero.1 (hT₅ ▸ measure_mono (Set.inter_subset_right _ _)),
  ENNReal.zero_toReal, sub_zero]
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ ENNReal.toReal (↑↑j₂.posPart (i ∩ T ∪ i ∩ Tᶜ)) = ENNReal.toReal (↑↑j₂.posPart (i ∩ Tᶜ))
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ ENNReal.toReal (↑↑j₂.posPart i) = ENNReal.toReal (↑↑j₂.posPart (i ∩ Tᶜ))
conv_lhs => rw [← Set.inter_union_compl i T]
case hd
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ Disjoint (i ∩ T) (i ∩ Tᶜ)

case h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ MeasurableSet (i ∩ Tᶜ)
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ ENNReal.toReal (↑↑j₂.posPart (i ∩ T ∪ i ∩ Tᶜ)) = ENNReal.toReal (↑↑j₂.posPart (i ∩ Tᶜ))
rw [measure_union,
  show j₂.posPart (i ∩ T) = 0 from
    nonpos_iff_eq_zero.1 (hT₄ ▸ measure_mono (Set.inter_subset_right _ _)),
  zero_add]
no goals
case hd
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ Disjoint (i ∩ T) (i ∩ Tᶜ)
exact
  Set.disjoint_of_subset_left (Set.inter_subset_right _ _)
    (Set.disjoint_of_subset_right (Set.inter_subset_right _ _) disjoint_compl_right)
no goals
case h
α : Type u_1
β : Type ?u.70440
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : toSignedMeasure j₁ = toSignedMeasure j₂
S : Set α
hS₁ : MeasurableSet S
hS₂ : VectorMeasure.restrict (toSignedMeasure j₁) S ≤ VectorMeasure.restrict 0 S
hS₃ : VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Sᶜ)
hS₄ : ↑↑j₁.posPart S = 0
hS₅ : ↑↑j₁.negPart (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : VectorMeasure.restrict (toSignedMeasure j₁) T ≤ VectorMeasure.restrict 0 T
hT₃ : VectorMeasure.restrict 0 (Tᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j₁) (Tᶜ)
hT₄ : ↑↑j₂.posPart T = 0
hT₅ : ↑↑j₂.negPart (Tᶜ) = 0
hST₁ : ↑(toSignedMeasure j₁) (Sᶜ ∆ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : ENNReal.toReal (↑↑j₁.posPart i) = ↑(toSignedMeasure j₁) (i ∩ Sᶜ)
⊢ MeasurableSet (i ∩ Tᶜ)
exact hi.inter hT₁.compl