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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
refine_1 : ∀ (h : ν.withDensity (μ.rnDeriv ν) = 0), μ ⟂ₘ ν
refine_2 : ∀ (h : μ ⟂ₘ ν), ν.withDensity (μ.rnDeriv ν) = 0
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ = μ.singularPart ν

Tactic:
rw [h, add_zero] at h_dec

Premises used: add_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : ν.withDensity (μ.rnDeriv ν) = 0
h_dec₁ : μ = μ.singularPart ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
rw [h, add_zero] at h_dec

Premises used: add_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
refine_1 : μ.singularPart ν ⟂ₘ ν
⊢ μ ⟂ₘ ν

Tactic:
rw [h_dec]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart μ ν

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
refine_2 : ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
rw [← MutuallySingular.self_iff]

Premises used: MeasureTheory.Measure.MutuallySingular.self_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν

Tactic:
rw [h_dec, MutuallySingular.add_left_iff] at h

Premises used: MeasureTheory.Measure.MutuallySingular.add_left_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)

Tactic:
MutuallySingular.mono_ac h.2 AbsolutelyContinuous.rfl ?_

Premises used: And.right, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
refine_2 : ν.withDensity (μ.rnDeriv ν) ≪ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)

Tactic:
refine MutuallySingular.mono_ac h.2 AbsolutelyContinuous.rfl ?_

Premises used: And.right, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
exact withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
rw : μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ ν.withDensity (μ.rnDeriv ν) = 0
rw₁ rw₂ : μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ.rnDeriv ν =ᶠ[ae ν] 0
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ ⟂ₘ ν

Tactic:
rw [← withDensity_rnDeriv_eq_zero, withDensity_eq_zero_iff (measurable_rnDeriv _ _).aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.withDensity_eq_zero_iff, MeasureTheory.Measure.withDensity_rnDeriv_eq_zero, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
rw : 0 ⟂ₘ ν
⊢ rnDeriv 0 ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
⊢ 0 ⟂ₘ ν

Tactic:
MutuallySingular.zero_left

Premises used: MeasureTheory.Measure.MutuallySingular.zero_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
⊢ 0 ⟂ₘ ν

Tactic:
exact MutuallySingular.zero_left

Premises used: MeasureTheory.Measure.MutuallySingular.zero_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
pos : ∀ (h : μ.HaveLebesgueDecomposition ν), μ.rnDeriv ν =ᶠ[ae ν] 0
neg : ∀ (h : ¬μ.HaveLebesgueDecomposition ν), μ.rnDeriv ν =ᶠ[ae ν] 0
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0

Tactic:
by_cases h : μ.HaveLebesgueDecomposition ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : μ.HaveLebesgueDecomposition ν
pos : μ ⟂ₘ ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : μ.HaveLebesgueDecomposition ν
⊢ μ ⟂ₘ ν

Tactic:
hμν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : μ.HaveLebesgueDecomposition ν
⊢ μ ⟂ₘ ν

Tactic:
exact hμν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : ¬μ.HaveLebesgueDecomposition ν
neg neg₁ : (ae ν).EventuallyEq (β := ℝ≥0∞) 0 0
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_of_not_haveLebesgueDecomposition h]

Premises used: MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
f : α → ℝ≥0∞
⊢ (ν.withDensity f).singularPart ν = 0

Tactic:
singularPart_eq_zero_of_ac (withDensity_absolutelyContinuous _ _)

Premises used: MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.singularPart_eq_zero_of_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
rw : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
mutuallySingular_singularPart μ ν

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart μ ν

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ.singularPart μ = 0

Tactic:
singularPart_eq_zero_of_ac Measure.AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.singularPart_eq_zero_of_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ μ.withDensity (μ.rnDeriv μ) + μ.singularPart μ = μ

Tactic:
have h := rnDeriv_add_singularPart μ μ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) + μ.singularPart μ = μ
⊢ μ.withDensity (μ.rnDeriv μ) = μ

Tactic:
rw [singularPart_self, add_zero] at h

Premises used: MeasureTheory.Measure.singularPart_self, add_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
⊢ μ = μ.withDensity 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
⊢ μ = μ.withDensity 1

Tactic:
have h_one : μ = μ.withDensity 1 := by simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
rw : μ.withDensity 1
| μ

Tactic:
rw [h_one]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
⊢ μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1

Tactic:
conv_rhs at h => rw [h_one]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
h₁ : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
⊢ μ = μ.withDensity 1

Tactic:
conv_rhs at h => rw [h_one]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
rwa : AEMeasurable (β := ℝ≥0∞) 1 μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ 1

Tactic:
rwa [withDensity_eq_iff_of_sigmaFinite (measurable_rnDeriv _ _).aemeasurable] at h

Premises used: Measurable.aemeasurable, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
⊢ AEMeasurable (β := ℝ≥0∞) 1 μ

Tactic:
aemeasurable_const

Premises used: ENNReal.ofNNReal, WithTop.some, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
⊢ AEMeasurable (β := ℝ≥0∞) 1 μ

Tactic:
exact aemeasurable_const

Premises used: aemeasurable_const
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν = μ ↔ μ ⟂ₘ ν

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
refine_1 : ∀ (h : μ.singularPart ν = μ), μ ⟂ₘ ν
refine_2 : ∀ (h : μ ⟂ₘ ν), μ.singularPart ν = μ
⊢ μ.singularPart ν = μ ↔ μ ⟂ₘ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.singularPart ν = μ
refine_1 : μ.singularPart ν ⟂ₘ ν
⊢ μ ⟂ₘ ν

Tactic:
rw [← h]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.singularPart ν = μ
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
mutuallySingular_singularPart _ _

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.singularPart ν = μ
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart _ _

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
have := h.haveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
| μ

Tactic:
rw [← singularPart_add_rnDeriv μ ν]

Premises used: MeasureTheory.Measure.singularPart_add_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
refine_2 : μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = μ

Tactic:
conv_rhs => rw [← singularPart_add_rnDeriv μ ν]

Premises used: MeasureTheory.Measure.singularPart_add_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
refine_2 : μ.singularPart ν = μ.singularPart ν + 0
refine_2₁ refine_2₂ : μ.singularPart ν = μ.singularPart ν
⊢ μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [(withDensity_rnDeriv_eq_zero _ _).mpr h, add_zero]

Premises used: Iff.mpr, MeasureTheory.Measure.withDensity_rnDeriv_eq_zero, add_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
rw : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν).singularPart ν = μ.singularPart ν

Tactic:
rw [Measure.singularPart_eq_self]

Premises used: MeasureTheory.Measure.singularPart_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
Measure.mutuallySingular_singularPart _ _

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact Measure.mutuallySingular_singularPart _ _

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
⊢ IsFiniteMeasure (μ.singularPart ν)

Tactic:
isFiniteMeasure_of_le μ <| singularPart_le μ ν

Premises used: MeasureTheory.isFiniteMeasure_of_le, MeasureTheory.Measure.singularPart_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
⊢ SigmaFinite (μ.singularPart ν)

Tactic:
sigmaFinite_of_le μ <| singularPart_le μ ν

Premises used: MeasureTheory.Measure.sigmaFinite_of_le, MeasureTheory.Measure.singularPart_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace α
inst_1 : IsLocallyFiniteMeasure μ
⊢ IsLocallyFiniteMeasure (μ.singularPart ν)

Tactic:
isLocallyFiniteMeasure_of_le <| singularPart_le μ ν

Premises used: MeasureTheory.Measure.isLocallyFiniteMeasure_of_le, MeasureTheory.Measure.singularPart_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
⊢ IsFiniteMeasure (ν.withDensity (μ.rnDeriv ν))

Tactic:
isFiniteMeasure_of_le μ <| withDensity_rnDeriv_le μ ν

Premises used: MeasureTheory.isFiniteMeasure_of_le, MeasureTheory.Measure.withDensity_rnDeriv_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
⊢ SigmaFinite (ν.withDensity (μ.rnDeriv ν))

Tactic:
sigmaFinite_of_le μ <| withDensity_rnDeriv_le μ ν

Premises used: MeasureTheory.Measure.sigmaFinite_of_le, MeasureTheory.Measure.withDensity_rnDeriv_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace α
inst_1 : IsLocallyFiniteMeasure μ
⊢ IsLocallyFiniteMeasure (ν.withDensity (μ.rnDeriv ν))

Tactic:
isLocallyFiniteMeasure_of_le <| withDensity_rnDeriv_le μ ν

Premises used: MeasureTheory.Measure.isLocallyFiniteMeasure_of_le, MeasureTheory.Measure.withDensity_rnDeriv_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
pos : ∫⁻ (x : α) in toMeasurable μ s, μ.rnDeriv ν x ∂ν < ∞
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞

Tactic:
suffices (∫⁻ x in toMeasurable μ s, μ.rnDeriv ν x ∂ν) < ∞ from
      lt_of_le_of_lt (lintegral_mono_set (subset_toMeasurable _ _)) this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
pos : LT.lt (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in toMeasurable μ s, μ.rnDeriv ν x ∂ν < ∞

Tactic:
rw [← withDensity_apply _ (measurableSet_toMeasurable _ _)]

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
⊢ (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)

Tactic:
le_add_self

Premises used: le_add_self
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
rw :
  Eq (α := ℝ≥0∞) ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.Measure.add_apply, MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hs.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
_ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s
⊢ LT.lt (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
calc
      _ ≤ (singularPart μ ν) (toMeasurable μ s) + _ := le_add_self
      _ = μ s := by rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]
      _ < ⊤ := hs.lt_top

Premises used: MeasureTheory.Measure.singularPart, Ne.lt_top, MeasureTheory.toMeasurable, DFunLike.coe, le_add_self
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞

Tactic:
simp only [Measure.rnDeriv, dif_neg hl, Pi.zero_apply, lintegral_zero, ENNReal.zero_lt_top]

Premises used: ENNReal.zero_lt_top, MeasureTheory.Measure.rnDeriv, Pi.zero_apply, MeasureTheory.lintegral_zero, dif_neg
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
rw : ∫⁻ (x : α) in univ, μ.rnDeriv ν x ∂ν < ∞
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ∞

Tactic:
rw [← setLIntegral_univ]

Premises used: MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
⊢ ∫⁻ (x : α) in univ, μ.rnDeriv ν x ∂ν < ∞

Tactic:
lintegral_rnDeriv_lt_top_of_measure_ne_top _ (measure_lt_top _ _).ne

Premises used: MeasureTheory.measure_lt_top, MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
⊢ ∫⁻ (x : α) in univ, μ.rnDeriv ν x ∂ν < ∞

Tactic:
exact lintegral_rnDeriv_lt_top_of_measure_ne_top _ (measure_lt_top _ _).ne

Premises used: MeasureTheory.measure_lt_top, MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ∞
a : α
hx : ∀ (i : ℕ), a ∈ spanningSets μ i → μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a < ∞

Tactic:
hx _ (mem_spanningSetsIndex _ _)

Premises used: MeasureTheory.mem_spanningSetsIndex