-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
@[simp] lemma add_right_inj (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] :
    μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
⊢ ν₁ = ν₂

Tactic:
rw [ext_iff_of_iUnion_eq_univ (iUnion_spanningSets μ)]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
⊢ ∀ (i : ℕ), ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
i : ℕ
s : Set α
hs : MeasurableSet s
h : ∀ (s : Set α), μ s + ν₁ s = μ s + ν₂ s
⊢ μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s =
    μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s

Tactic:
simp [hs, h]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
⊢ ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)

Tactic:
ext s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ (ν₁.restrict (spanningSets μ i)) s = (ν₂.restrict (spanningSets μ i)) s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
⊢ ∀ (i : ℕ), ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)

Tactic:
intro i

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
⊢ ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
⊢ ν₁ = ν₂

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : ν₁ = ν₂
⊢ μ + ν₁ = μ + ν₂

Tactic:
rw [h]

Result:
no goals

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s =
    μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s

Tactic:
simp only [ext_iff', coe_add, Pi.add_apply] at h

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
i : ℕ
s : Set α
hs : MeasurableSet s
h : ∀ (s : Set α), μ s + ν₁ s = μ s + ν₂ s
⊢ μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s =
    μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ (ν₁.restrict (spanningSets μ i)) s = (ν₂.restrict (spanningSets μ i)) s

Tactic:
rw [← ENNReal.add_right_inj (measure_mono s.inter_subset_right |>.trans_lt <|
  measure_spanningSets_lt_top μ i).ne]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s =
    μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s