-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toSignedMeasure_injective : Injective <| @JordanDecomposition.toSignedMeasure α _

Proof state:
case hd
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ Disjoint (i ∩ S) (i ∩ Sᶜ)

Tactic:
refine
  Set.disjoint_of_subset_left Set.inter_subset_right
    (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ MeasurableSet (i ∩ Sᶜ)

Tactic:
exact hi.inter hS₁.compl

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
⊢ j₁ = j₂

Tactic:
obtain ⟨T, hT₁, hT₂, hT₃, hT₄, hT₅⟩ := j₂.exists_compl_positive_negative

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₂.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₂.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
⊢ j₁ = j₂

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : (j₁.posPart i).toReal = ↑j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ (j₂.posPart i).toReal = ↑j₂.toSignedMeasure (i ∩ Tᶜ)

Tactic:
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]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : (j₁.posPart i).toReal = ↑j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ (j₂.posPart i).toReal = (j₂.posPart (i ∩ Tᶜ)).toReal

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : (j₁.posPart i).toReal = ↑j₁.toSignedMeasure (i ∩ Sᶜ)
hμ₂ : (j₂.posPart i).toReal = ↑j₂.toSignedMeasure (i ∩ Tᶜ)
⊢ j₁.posPart i = j₂.posPart i

Tactic:
rw [← ENNReal.toReal_eq_toReal (measure_ne_top _ _) (measure_ne_top _ _), hμ₁, hμ₂, ← hj]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : (j₁.posPart i).toReal = ↑j₁.toSignedMeasure (i ∩ Sᶜ)
hμ₂ : (j₂.posPart i).toReal = ↑j₂.toSignedMeasure (i ∩ Tᶜ)
⊢ ↑j₁.toSignedMeasure (i ∩ Sᶜ) = ↑j₁.toSignedMeasure (i ∩ Tᶜ)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁ = j₂

Tactic:
obtain ⟨S, hS₁, hS₂, hS₃, hS₄, hS₅⟩ := j₁.exists_compl_positive_negative

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
⊢ j₁ = j₂

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ Injective toSignedMeasure

Tactic:
intro j₁ j₂ hj

Result:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁ = j₂