awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (r • μ).withDensity (ν.rnDeriv (r • μ)) = r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)),
    ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
      (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

Premises used: MeasureTheory.Measure.add_right_inj
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
suffices :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)

Tactic:
suffices ν.singularPart (r • μ) + withDensity (r • μ) (rnDeriv ν (r • μ))
        = ν.singularPart (r • μ) + r⁻¹ • withDensity (r • μ) (rnDeriv ν μ) by
      rwa [add_right_inj] at this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
rw : ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
⊢ ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)

Tactic:
rw [← ν.haveLebesgueDecomposition_add (r • μ), singularPart_smul_right _ _ _ hr,
      ENNReal.smul_def r, withDensity_smul_measure, ← ENNReal.smul_def, ← smul_assoc,
      smul_eq_mul, inv_mul_cancel₀ hr, one_smul]

Premises used: ENNReal.smul_def, smul_assoc, MeasureTheory.Measure.haveLebesgueDecomposition_add, one_smul, HSMul.hSMul, MeasureTheory.withDensity_smul_measure, smul_eq_mul, MeasureTheory.Measure.singularPart_smul_right, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)

Tactic:
ν.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)

Tactic:
exact ν.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ

Tactic:
rnDeriv_smul_right ν μ ?_

Premises used: MeasureTheory.Measure.rnDeriv_smul_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
refine : r.toNNReal ≠ 0
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ

Tactic:
refine rnDeriv_smul_right ν μ ?_

Premises used: MeasureTheory.Measure.rnDeriv_smul_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
rw : ¬(r = 0 ∨ r = ∞)
⊢ r.toNNReal ≠ 0

Tactic:
rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]

Premises used: ENNReal.toNNReal_eq_zero_iff, ne_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ¬(r = 0 ∨ r = ∞)

Tactic:
simp [hr, hr_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ

Tactic:
have h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ := by
    refine rnDeriv_smul_right ν μ ?_
    rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
    simp [hr, hr_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
h₁ : ∀ (x : α), (r.toNNReal⁻¹ • ν.rnDeriv μ) x = (r⁻¹ • ν.rnDeriv μ) x
⊢ r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
x : α
h₁ : r.toNNReal ≠ 0
⊢ (↑r.toNNReal⁻¹ : ℝ≥0∞) * ν.rnDeriv μ x = r⁻¹ * ν.rnDeriv μ x

Tactic:
rw [ENNReal.coe_inv, ENNReal.coe_toNNReal hr_ne_top]

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_inv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
x : α
h₁ : ¬(r = 0 ∨ r = ∞)
⊢ r.toNNReal ≠ 0

Tactic:
rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]

Premises used: ENNReal.toNNReal_eq_zero_iff, ne_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
x : α
⊢ ¬(r = 0 ∨ r = ∞)

Tactic:
simp [hr, hr_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
⊢ r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ

Tactic:
have : (r.toNNReal)⁻¹ • rnDeriv ν μ = r⁻¹ • rnDeriv ν μ := by
    ext x
    simp only [Pi.smul_apply, ENNReal.smul_def, smul_eq_mul]
    rw [ENNReal.coe_inv, ENNReal.coe_toNNReal hr_ne_top]
    rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
    simp [hr, hr_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
this : r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
simp_rw [this, ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top] at h

Premises used: ENNReal.coe_toNNReal, ENNReal.smul_def
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
this : r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ
h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
this : r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ
h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
h :
  ∀ (x : α) (hx1 : (r • ν).rnDeriv μ x = (r • ν.rnDeriv μ) x)
    (hx2 : (r • ν).rnDeriv (r • μ) x = (r⁻¹ • (r • ν).rnDeriv μ) x), (r • ν).rnDeriv (r • μ) x = ν.rnDeriv μ x
⊢ (r • ν).rnDeriv (r • μ) =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
filter_upwards [rnDeriv_smul_left ν μ r, rnDeriv_smul_right (r • ν) μ hr] with x hx1 hx2

Premises used: MeasureTheory.Measure.rnDeriv_smul_right, MeasureTheory.Measure.rnDeriv_smul_left, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
x : α
hx1 : (r • ν).rnDeriv μ x = (r • ν.rnDeriv μ) x
hx2 : (r • ν).rnDeriv (r • μ) x = (r⁻¹ • (r • ν).rnDeriv μ) x
⊢ (r • ν).rnDeriv (r • μ) x = ν.rnDeriv μ x

Tactic:
simp [hx1, hx2, hr]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
rw : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
hf : AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ
hg : AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ
hfi : ∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ∞
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff]

Premises used: MeasureTheory.withDensity_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)),
    μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

Premises used: MeasureTheory.Measure.add_right_inj
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
suffices :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
suffices (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ)
        = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ) by
      rwa [add_right_inj] at this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
rw₅ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ))
rw₆ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (ν₂.singularPart μ + μ.withDensity (ν₂.rnDeriv μ)))
rw₇ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + ν₂)
rw₈ : ν₁ + ν₂ = ν₁.singularPart μ + μ.withDensity (ν₁.rnDeriv μ) + ν₂
rw₉ rw₁₀ : ν₁ + ν₂ = ν₁ + ν₂
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_assoc, MeasureTheory.withDensity_add_left, add_comm, MeasureTheory.Measure.singularPart, HAdd.hAdd, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.singularPart_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ

Tactic:
(measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ

Tactic:
((measurable_rnDeriv _ _).add (measurable_rnDeriv _ _)).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.add, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ

Tactic:
exact ((measurable_rnDeriv _ _).add (measurable_rnDeriv _ _)).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.add, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ∞

Tactic:
(lintegral_rnDeriv_lt_top (ν₁ + ν₂) μ).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, HAdd.hAdd, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ∞

Tactic:
exact (lintegral_rnDeriv_lt_top (ν₁ + ν₂) μ).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, HAdd.hAdd, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
obtain :
  ∀ (s : Set α) (hs : MeasurableSet s)
    (hs_le :
      ∀ (t : Set α),
        MeasurableSet t →
          t ⊆ s →
            LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
    (hs_ge :
      ∀ (t : Set α),
        MeasurableSet t →
          t ⊆ sᶜ →
            LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
              (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)),
    ∃ (s : Set α),
      MeasurableSet s ∧
        (∀ (t : Set α),
            MeasurableSet t →
              LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
                ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)) ∧
          ∀ (t : Set α),
            MeasurableSet t →
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
                (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
              (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)

Tactic:
obtain ⟨s, hs, hs_le, hs_ge⟩ := hahn_decomposition μ ((1 / (n + 1) : ℝ≥0) • ν)

Premises used: MeasureTheory.hahn_decomposition, HDiv.hDiv, Nat.cast, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ s →
        LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
hs_ge :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ sᶜ →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
              (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)

Tactic:
⟨s, hs, fun t ht ↦ ?_, fun t ht ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ s →
        LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
hs_ge :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ sᶜ →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_1 :
  ∀ (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
refine_2 :
  ∀ (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
              (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)

Tactic:
refine ⟨s, hs, fun t ht ↦ ?_, fun t ht ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ s →
        LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
hs_ge :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ sᶜ →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
hs_le (t ∩ s) (ht.inter hs) inter_subset_right

Premises used: Inter.inter, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ s →
        LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
hs_ge :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ sᶜ →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
exact hs_le (t ∩ s) (ht.inter hs) inter_subset_right

Premises used: Inter.inter, Set.inter_subset_right, MeasurableSet.inter