-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hνrn : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (0 : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A
h₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A
h₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A
h₅ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A \ (S ∩ T)) : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A
h₆ h₇ :
  Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [heq' A hA, heq, ← add_zero ((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) A), ← hνrn,
    restrict_apply hA, ← diff_eq, measure_inter_add_diff _ (hS₁.inter hT₁)]

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.restrict, Set.diff_eq, Inter.inter, MeasureTheory.measure_inter_add_diff, add_zero, DFunLike.coe, MeasurableSet.inter