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 α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
pos : r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + (↑r : ℝ≥0∞) • ν.withDensity (μ.rnDeriv ν)
pos₁ : r • μ = (↑r : ℝ≥0∞) • (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
pos₂ : r • μ = (↑r : ℝ≥0∞) • μ
⊢ r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • μ.rnDeriv ν)
have pos₃ : (↑r : ℝ≥0∞) • μ = (↑r : ℝ≥0∞) • μ
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
      ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have neg : ¬(r • μ).HaveLebesgueDecomposition ν
Tactic: rw [singularPart, singularPart, dif_neg hl, dif_neg, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬(r • μ).HaveLebesgueDecomposition ν
have neg : ∀ (hl' : (r • μ).HaveLebesgueDecomposition ν), μ.HaveLebesgueDecomposition ν
Tactic: refine fun hl' ↦ hl ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : (r • μ).HaveLebesgueDecomposition ν
⊢ μ.HaveLebesgueDecomposition ν
have neg : (r⁻¹ • r • μ).HaveLebesgueDecomposition ν
Tactic: rw [← inv_smul_smul₀ hr μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
⊢ μ.singularPart (r • ν) = μ.singularPart ν
have pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), μ.singularPart (r • ν) = μ.singularPart ν
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), μ.singularPart (r • ν) = μ.singularPart ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν
have neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), μ.singularPart (r • ν) = μ.singularPart ν
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν
have pos : μ.singularPart ν ⟂ₘ r • ν
Tactic: refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
pos : μ.singularPart ν ⟂ₘ r • ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν
have pos₁ : μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)
Tactic: refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)
have pos : μ = μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν)
Tactic: rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
pos : μ = μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν)
⊢ μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)
have pos₁ : Measurable (r⁻¹ • μ.rnDeriv ν)
Tactic: rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν)
have h : (↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν = μ.rnDeriv ν
Tactic: convert! haveLebesgueDecomposition_add μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ (↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν = μ.rnDeriv ν
have h : ∀ (x : α), ((↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν) x = μ.rnDeriv ν x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ (↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x
have h : r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x
Tactic: rw [← ENNReal.smul_def, smul_inv_smul₀ hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
h : r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x
⊢ (↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x
have h₁ : μ.rnDeriv ν x = μ.rnDeriv ν x
Tactic: rw [← ENNReal.smul_def, smul_inv_smul₀ hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν
have neg : ¬μ.HaveLebesgueDecomposition (r • ν)
Tactic: rw [singularPart, singularPart, dif_neg hl, dif_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬μ.HaveLebesgueDecomposition (r • ν)
have neg : ∀ (hl' : μ.HaveLebesgueDecomposition (r • ν)), μ.HaveLebesgueDecomposition ν
Tactic: refine fun hl' ↦ hl ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : μ.HaveLebesgueDecomposition (r • ν)
⊢ μ.HaveLebesgueDecomposition ν
have neg : μ.HaveLebesgueDecomposition (r⁻¹ • r • ν)
Tactic: rw [← inv_smul_smul₀ hr ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
⊢ (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν
have refine : μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity fun (a : α) ↦ μ₁.rnDeriv ν a + μ₂.rnDeriv ν a
Tactic: refine (eq_singularPart ((measurable_rnDeriv μ₁ ν).add (measurable_rnDeriv μ₂ ν))
    ((mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity fun (a : α) ↦ μ₁.rnDeriv ν a + μ₂.rnDeriv ν a
have rw : μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))
Tactic: rw [← Pi.add_def, withDensity_add_left (measurable_rnDeriv μ₁ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
| μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))
have rw : μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
Tactic: rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))
have conv_rhs : μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
Tactic: conv_rhs => rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
have rw : μ₁ + μ₂ = μ₁ + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
Tactic: rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)),
    ← haveLebesgueDecomposition_add μ₂ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
rw : μ₁ + μ₂ = μ₁ + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
have rw₁ : μ₁ + μ₂ = μ₁ + (ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν)
Tactic: rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)),
    ← haveLebesgueDecomposition_add μ₂ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
rw : μ₁ + μ₂ = μ₁ + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
rw₁ : μ₁ + μ₂ = μ₁ + (ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν)
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
have rw₂ : μ₁ + μ₂ = μ₁ + (μ₂.singularPart ν + ν.withDensity (μ₂.rnDeriv ν))
Tactic: rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)),
    ← haveLebesgueDecomposition_add μ₂ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
rw : μ₁ + μ₂ = μ₁ + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
rw₁ : μ₁ + μ₂ = μ₁ + (ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν)
rw₂ : μ₁ + μ₂ = μ₁ + (μ₂.singularPart ν + ν.withDensity (μ₂.rnDeriv ν))
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
have rw₃ : μ₁ + μ₂ = μ₁ + μ₂
Tactic: rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)),
    ← haveLebesgueDecomposition_add μ₂ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s
have refine_1 : Measurable (s.indicator (μ.rnDeriv ν))
Tactic: refine (Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
refine_1 : Measurable (s.indicator (μ.rnDeriv ν))
⊢ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s
have refine_2 : (μ.singularPart ν).restrict s ⟂ₘ ν
Tactic: refine (Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
refine_1 : Measurable (s.indicator (μ.rnDeriv ν))
refine_2 : (μ.singularPart ν).restrict s ⟂ₘ ν
⊢ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s
have refine_3 : μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))
Tactic: refine (Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))
have refine_3 : ∀ (t : Set α),
  MeasurableSet t →
    Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν)) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
t : Set α
h : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν)) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine_3 : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  (((μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [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 ν
s : Set α
hs : MeasurableSet s
t : Set α
h : MeasurableSet t
refine_3 :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν)) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine_3₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  (((μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [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 ν
s : Set α
hs : MeasurableSet s
t : Set α
h : MeasurableSet t
refine_3 :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_3₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν)) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine_3₂ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  (((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [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 ν
s : Set α
hs : MeasurableSet s
t : Set α
h : MeasurableSet t
refine_3 :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_3₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_3₂ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν)) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine_3₃ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [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 α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
| μ.restrict s
have rw : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
Tactic: rw [← singularPart_add_rnDeriv μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.singularPart ν = μ.restrict s
have conv_rhs : μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
Tactic: conv_rhs => rw [← singularPart_add_rnDeriv μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
have rwa : μ.singularPart ν = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
Tactic: rwa [restrict_add, restrict_eq_self_of_ae_mem, restrict_eq_zero.2 hνs, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : μ.singularPart ν = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
⊢ μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
have rwa₁ : μ.singularPart ν = μ.singularPart ν + (ν.withDensity (μ.rnDeriv ν)).restrict s
Tactic: rwa [restrict_add, restrict_eq_self_of_ae_mem, restrict_eq_zero.2 hνs, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : μ.singularPart ν = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
rwa₁ : μ.singularPart ν = μ.singularPart ν + (ν.withDensity (μ.rnDeriv ν)).restrict s
⊢ μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
have hs : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
Tactic: rwa [restrict_add, restrict_eq_self_of_ae_mem, restrict_eq_zero.2 hνs, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : μ.singularPart ν = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
rwa₁ : μ.singularPart ν = μ.singularPart ν + (ν.withDensity (μ.rnDeriv ν)).restrict s
hs : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
⊢ μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
have rwa₂ : μ.singularPart ν = μ.singularPart ν + 0
Tactic: rwa [restrict_add, restrict_eq_self_of_ae_mem, restrict_eq_zero.2 hνs, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : μ.singularPart ν = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
rwa₁ : μ.singularPart ν = μ.singularPart ν + (ν.withDensity (μ.rnDeriv ν)).restrict s
hs : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
rwa₂ : μ.singularPart ν = μ.singularPart ν + 0
hs₁ : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
⊢ μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
have rwa₃ : μ.singularPart ν = μ.singularPart ν
Tactic: rwa [restrict_add, restrict_eq_self_of_ae_mem, restrict_eq_zero.2 hνs, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : IsFiniteMeasure μ
⊢ μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)
have nth_rw : ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)
Tactic: nth_rw 1 [← rnDeriv_add_singularPart μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : IsFiniteMeasure μ
⊢ μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν
have nth_rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν
Tactic: nth_rw 1 [← singularPart_add_rnDeriv μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
have this : μ.HaveLebesgueDecomposition ν
Tactic: have : HaveLebesgueDecomposition μ ν := ⟨⟨⟨s, f⟩, hf, hs, hadd⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
have hmeas : Measurable (μ.rnDeriv ν)
Tactic: obtain ⟨hmeas, hsing, hadd'⟩ := haveLebesgueDecomposition_spec μ ν