awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
s : Set α
hs : MeasurableSet s
rw : μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))
rw₁ : μ.restrict s = (μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν)
rw₂ : μ.restrict s = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
⊢ μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))
have rw₃ : μ.restrict s = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
Tactic: rw [singularPart_restrict _ _ hs, withDensity_indicator hs, ← restrict_withDensity hs,
    ← Measure.restrict_add, ← μ.haveLebesgueDecomposition_add ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
s : Set α
hs : MeasurableSet s
rw : μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))
rw₁ : μ.restrict s = (μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν)
rw₂ : μ.restrict s = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
rw₃ : μ.restrict s = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
⊢ μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))
have rw₄ : μ.restrict s = μ.restrict s
Tactic: rw [singularPart_restrict _ _ hs, withDensity_indicator hs, ← restrict_withDensity hs,
    ← Measure.restrict_add, ← μ.haveLebesgueDecomposition_add ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator 1
have rw : (ν.withDensity (s.indicator 1)).rnDeriv ν =ᶠ[ae ν] s.indicator 1
Tactic: rw [← withDensity_indicator_one hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have hf : AEMeasurable ((r • ν).rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
hf : AEMeasurable ((r • ν).rnDeriv μ) μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have hg : AEMeasurable (r • ν.rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
hf : AEMeasurable ((r • ν).rnDeriv μ) μ
hg : AEMeasurable (r • ν.rnDeriv μ) μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have hfi : ∫⁻ (x : α), (r • ν).rnDeriv μ x ∂μ ≠ ∞
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = μ.withDensity ((↑r : ℝ≥0∞) • ν.rnDeriv μ)
have rw : μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
this :
  (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
have rwa : ∀ (this : μ.withDensity ((r • ν).rnDeriv μ) = r • μ.withDensity (ν.rnDeriv μ)),
  μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
Tactic: rwa [Measure.add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
have suffices : (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
Tactic: suffices (r • ν).singularPart μ + withDensity μ (rnDeriv (r • ν) μ)
        = (r • ν).singularPart μ + r • withDensity μ (rnDeriv ν μ) by
      rwa [Measure.add_right_inj] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw₁ : r • ν = r • ν.singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₁ : r • ν = r • ν.singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw₂ : r • ν = r • (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ))
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₁ : r • ν = r • ν.singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₂ : r • ν = r • (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ))
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw₃ : r • ν = r • ν
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ
Tactic: have h : (r.toNNReal • ν).rnDeriv μ =ᵐ[μ] r.toNNReal • ν.rnDeriv μ :=
    rnDeriv_smul_left ν μ r.toNNReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have refine : ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
Tactic: refine (absolutelyContinuous_smul <| ENNReal.coe_ne_zero.2 hr).ae_le
    (?_ : ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
have rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
have hf : AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
hf : AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
have hg : AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
hf : AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
hg : AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
have hfi : ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ∞
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    ((↑r : ℝ≥0∞) • μ).withDensity ((↑r⁻¹ : ℝ≥0∞) • ν.rnDeriv μ)
have rw : ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
  (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ)
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
have rwa : ∀ (this : (r • μ).withDensity (ν.rnDeriv (r • μ)) = r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)),
  ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
Tactic: rwa [add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
have suffices : ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
  ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
Tactic: suffices ν.singularPart (r • μ) + withDensity (r • μ) (rnDeriv ν (r • μ))
        = ν.singularPart (r • μ) + r⁻¹ • withDensity (r • μ) (rnDeriv ν μ) by
      rwa [add_right_inj] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
have rw : ν = ν.singularPart μ + μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ
have refine : r.toNNReal ≠ 0
Tactic: refine rnDeriv_smul_right ν μ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ r.toNNReal ≠ 0
have rw : ¬(r = 0 ∨ r = ∞)
Tactic: rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have h : ν.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ
have h₁ : ∀ (x : α), (r.toNNReal⁻¹ • ν.rnDeriv μ) x = (r⁻¹ • ν.rnDeriv μ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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.toNNReal⁻¹ : ℝ≥0∞) * ν.rnDeriv μ x = r⁻¹ * ν.rnDeriv μ x
have h₁ : r.toNNReal ≠ 0
Tactic: rw [ENNReal.coe_inv, ENNReal.coe_toNNReal hr_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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.toNNReal ≠ 0
have h₁ : ¬(r = 0 ∨ r = ∞)
Tactic: rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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 μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have this : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • ν).rnDeriv (r • μ) =ᶠ[ae μ] ν.rnDeriv μ
have h : ∀ (x : α) (hx1 : (r • ν).rnDeriv μ x = (r • ν.rnDeriv μ) x)
  (hx2 : (r • ν).rnDeriv (r • μ) x = (r⁻¹ • (r • ν).rnDeriv μ) x), (r • ν).rnDeriv (r • μ) x = ν.rnDeriv μ x
Tactic: filter_upwards [rnDeriv_smul_left ν μ r, rnDeriv_smul_right (r • ν) μ hr] with x hx1 hx2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
have rw : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ)
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
have hf : AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ) μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
have hg : AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ) μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
have hfi : ∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ∞
Tactic: rw [← withDensity_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rwa : ∀ (this : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)),
  μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: rwa [add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have suffices : (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
  (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: suffices (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ)
        = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ) by
      rwa [add_right_inj] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : IsFiniteMeasure ν₁
inst_1 : IsFiniteMeasure ν₂
inst_2 : ν₁.HaveLebesgueDecomposition μ
inst_3 : ν₂.HaveLebesgueDecomposition μ
inst_4 : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw : ν₁ + ν₂ = (ν₁ + ν₂).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 μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ)
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.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 μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 μ)
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.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 μ]