awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
⊢ μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν
have h_ac : ν ≪ ν + ν'
Tactic: have h_ac : ν ≪ ν + ν' := Measure.AbsolutelyContinuous.rfl.add_right _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν
have rw : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Tactic: rw [haveLebesgueDecomposition_add μ ν']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have h₁ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
  (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
Tactic: have h₁ := rnDeriv_add' (μ.singularPart ν') (ν'.withDensity (μ.rnDeriv ν')) (ν + ν')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have h₂ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
  (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Tactic: have h₂ := rnDeriv_add' (μ.singularPart ν') (ν'.withDensity (μ.rnDeriv ν')) ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have refine : (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
  (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Tactic: refine (Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have refine_2 : ∀ (h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν),
  (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Tactic: have h₃ := rnDeriv_add_right_of_mutuallySingular' (?_ : μ.singularPart ν' ⟂ₘ ν') hνν'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
refine_2 :
  ∀ (h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν),
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
      (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have refine_1 : μ.singularPart ν' ⟂ₘ ν'
Tactic: have h₃ := rnDeriv_add_right_of_mutuallySingular' (?_ : μ.singularPart ν' ⟂ₘ ν') hνν'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
have refine : ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν
Tactic: refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
Tactic: have h₄ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv (ν + ν') =ᵐ[ν] 0 := by
      refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac
      exact hνν'.symm.withDensity
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
have rw : ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν
Tactic: rw [rnDeriv_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
Tactic: have h₅ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv ν =ᵐ[ν] 0 := by
      rw [rnDeriv_eq_zero]
      exact hνν'.symm.withDensity
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
have h : ∀ (x : α) (hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x)
  (hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x)
  (hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x),
  ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
Tactic: filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
have h : (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
  ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
Tactic: rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
h :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
have h₆ : (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
  (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
Tactic: rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
h :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
h₆ :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
have h₇ : (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
  (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
Tactic: rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
h :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
h₆ :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
h₇ :
  (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
have h₈ : (μ.singularPart ν').rnDeriv ν x + 0 x = (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
Tactic: rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
h :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
h₆ :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
h₇ :
  (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
h₈ :
  (μ.singularPart ν').rnDeriv ν x + 0 x = (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
have h₉ : (μ.singularPart ν').rnDeriv ν x + 0 x = (μ.singularPart ν').rnDeriv ν x + 0 x
Tactic: rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
| μ.rnDeriv ν
have rw : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
Tactic: rw [ν.haveLebesgueDecomposition_add μ, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv ν
have conv_rhs : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
Tactic: conv_rhs => rw [ν.haveLebesgueDecomposition_add μ, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
have refine : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae (μ.withDensity (ν.rnDeriv μ))]
  μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
Tactic: refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
this : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
⊢ (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
have rw : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
this : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ
have calc : (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
Tactic: calc (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
          (rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
    _ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
    _ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ
have suffices : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
Tactic: suffices μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ) by
    calc (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
          (rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
    _ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
    _ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
have rw : (ν.withDensity (μ.rnDeriv ν)).withDensity ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ = ν
Tactic: rw [withDensity_rnDeriv_eq _ _ hνμ, ← withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
| ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹
have rw : (μ.rnDeriv ν)⁻¹
Tactic: rw [withDensity_rnDeriv_eq _ _ hμν]