awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : IsFiniteMeasure μ
nth_rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν
⊢ μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
nth_rw 1 [← singularPart_add_rnDeriv μ ν]

Premises used: MeasureTheory.Measure.singularPart_add_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : IsFiniteMeasure μ
⊢ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
Measure.add_sub_cancel

Premises used: MeasureTheory.Measure.add_sub_cancel
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : IsFiniteMeasure μ
⊢ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
exact Measure.add_sub_cancel

Premises used: MeasureTheory.Measure.add_sub_cancel
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
obtain :
  ∀ (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∞)),
    ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Tactic:
obtain ⟨⟨S, hS₁, hS₂, hS₃⟩, ⟨T, hT₁, hT₂, hT₃⟩⟩ := hs, hsing
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ = 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∞)
rw :
  ∀ (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∞)),
    ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [hadd'] at hadd
-- 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∞)
h :
  ∀ (A : Set α) (hA : MeasurableSet A),
    Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)

Tactic:
ext1 A hA
-- 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∞)
A : Set α
hA : MeasurableSet A
rw : LE.le (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- 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∞)
A : Set α
hA : MeasurableSet A
⊢ LE.le (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)

Premises used: Eq.rec, HasSubset.Subset.trans, Set.inter_subset_left, MeasureTheory.measure_mono, Set.inter_subset_right
-- 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∞)
A : Set α
hA : MeasurableSet A
⊢ LE.le (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
-- 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∞)
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hs : s (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)

Premises used: Eq.rec, HasSubset.Subset.trans, MeasureTheory.measure_mono, Set.inter_subset_right
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hsing : μ.singularPart ν (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)
-- 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∞)
⊢ (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)

Tactic:
have heq :
    (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) := by
    ext1 A hA
    have hs : s (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
    have hsing : μ.singularPart ν (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)
    rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ←
      add_apply, add_comm, ← hadd, add_apply, hsing, zero_add]
-- 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)
A : Set α
hA : MeasurableSet A
rw : LE.le (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- 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)
A : Set α
hA : MeasurableSet A
⊢ LE.le (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
withDensity_absolutelyContinuous ν f hνinter ▸ measure_mono inter_subset_right

Premises used: Eq.rec, MeasureTheory.measure_mono, MeasureTheory.withDensity_absolutelyContinuous, Set.inter_subset_right
-- 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)
A : Set α
hA : MeasurableSet A
⊢ LE.le (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact withDensity_absolutelyContinuous ν f hνinter ▸ measure_mono inter_subset_right
-- 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)
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hνfinter : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact withDensity_absolutelyContinuous ν f hνinter ▸ measure_mono inter_subset_right
-- 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)
A : Set α
hA : MeasurableSet A
hνfinter : Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
rw₁ :
  (ν.withDensity f : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ :
  (ν.withDensity f : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
      ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞)
rw₃ :
  (ν.withDensity f : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
      ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A \ (S ∩ T)) : ℝ≥0∞)
rw₄ rw₅ :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hνfinter, ← diff_eq,
      measure_inter_add_diff _ (hS₁.inter hT₁)]

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.Measure.restrict_apply, Set.diff_eq, Inter.inter, MeasureTheory.measure_inter_add_diff, add_zero, DFunLike.coe, MeasurableSet.inter
-- 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)
⊢ ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
have heq' :
    ∀ A : Set α, MeasurableSet A → ν.withDensity f A = (ν.withDensity f).restrict (S ∩ T) A := by
    intro A hA
    have hνfinter : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact withDensity_absolutelyContinuous ν f hνinter ▸ measure_mono inter_subset_right
    rw [restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hνfinter, ← diff_eq,
      measure_inter_add_diff _ (hS₁.inter hT₁)]