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μ : μ ≪ ξ
hν : ν ≪ ξ
⊢ μ.rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x
have hν_ac : ν ≪ μ + ν
Tactic: have hν_ac : ν ≪ μ + ν := rfl.absolutelyContinuous.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ν : ν ≪ ξ
hν_ac : ν ≪ μ + ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = (fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α)
                {x : α |
                  (fun (x : α) ↦
                      Eq (α := ℝ≥0∞) ((fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) x)
                        ((fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) x))
                    x}
                x →
              Membership.mem (γ := Set α)
                {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) x) x} x}
          x}
    a
Tactic: filter_upwards [μ.rnDeriv_eq_div_rnDeriv_add ν,
    hν_ac (rnDeriv_div_rnDeriv_eq_div_rnDeriv_add hμ hν)] with a h1 h2 using h1.trans h2.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ν : ν ≪ ξ
hν_ac : ν ≪ μ + ν
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = (fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq (α := ℝ≥0∞) ((fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) x)
                          ((fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) x))
                      x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) x) x} x}
            x}
      a
⊢ μ.rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x
have h₁ : ∀ (a : α),
  μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a →
    μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a →
      μ.rnDeriv ν a = μ.rnDeriv ξ a / ν.rnDeriv ξ a
Tactic: filter_upwards [μ.rnDeriv_eq_div_rnDeriv_add ν,
    hν_ac (rnDeriv_div_rnDeriv_eq_div_rnDeriv_add hμ hν)] with a h1 h2 using h1.trans h2.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν
have refine_1 : Measurable (β := ℝ≥0∞) fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
refine_1 : Measurable (β := ℝ≥0∞) fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
⊢ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν
have refine_2 : Measurable (μ.rnDeriv ν)
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
refine_1 : Measurable (β := ℝ≥0∞) fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
refine_2 : Measurable (μ.rnDeriv ν)
⊢ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν
have refine_3 : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α) in s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν
have refine_3 : ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
Tactic: rw [← hf.lintegral_map, Measure.setLIntegral_rnDeriv hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s = f ⁻¹' f '' s
have rw : s = s
Tactic: rw [hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
have hs_eq : s = f ⁻¹' f '' s
Tactic: have hs_eq : s = f ⁻¹' f '' s := by rw [hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_eq : s = f ⁻¹' f '' s
⊢ ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
have this : SigmaFinite (m0 := mβ) (map f ν)
Tactic: have : SigmaFinite (ν.map f) := hf.sigmaFinite_map
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (m0 := mβ) (map f ν)
⊢ ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
have refine_3 : ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict (f ⁻¹' f '' s)) =
  (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
Tactic: rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
    hf.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (m0 := mβ) (map f ν)
refine_3 :
  ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict (f ⁻¹' f '' s)) =
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
⊢ ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
have refine_3₁ : ∫⁻ (a : β) in f '' s, rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f ν = (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
Tactic: rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
    hf.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (m0 := mβ) (map f ν)
refine_3 :
  ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict (f ⁻¹' f '' s)) =
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
refine_3₁ :
  ∫⁻ (a : β) in f '' s, rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f ν = (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
⊢ ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
have refine_3₂ : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞)
Tactic: rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
    hf.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (m0 := mβ) (map f ν)
refine_3 :
  ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict (f ⁻¹' f '' s)) =
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
refine_3₁ :
  ∫⁻ (a : β) in f '' s, rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f ν = (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
refine_3₂ :
  Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞)
⊢ ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
have refine_3₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞)
Tactic: rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
    hf.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν
have rw : (fun (x : α) ↦
    (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
      (f x)) =ᶠ[ae ν]
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Tactic: rw [μ.haveLebesgueDecomposition_add ν, Measure.map_add _ _ hf.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
have this : SigmaFinite (m0 := mβ) (map f ν)
Tactic: have : SigmaFinite (map f ν) := hf.sigmaFinite_map
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this : SigmaFinite (m0 := mβ) (map f ν)
⊢ (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
have this₁ : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
Tactic: have : SigmaFinite (map f (μ.singularPart ν)) := hf.sigmaFinite_map
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
⊢ (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
have this₁ : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
Tactic: have : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν))) := hf.sigmaFinite_map
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
⊢ (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
have h_add : (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv
    (map f ν) =ᶠ[ae (F := Measure β) (map f ν)]
  rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
    rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν)
Tactic: have h_add := Measure.rnDeriv_add' ((μ.singularPart ν).map f)
    ((ν.withDensity (μ.rnDeriv ν)).map f) (ν.map f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv
      (map f ν) =ᶠ[ae (F := Measure β) (map f ν)]
    rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
      rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν)
⊢ (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
have h_add₁ : (ae ν).EventuallyEq (β := ℝ≥0∞)
  (fun (x : α) ↦
    (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
      (f x))
  fun (x : α) ↦
  (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
      rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
    (f x)
Tactic: rw [Filter.EventuallyEq, hf.ae_map_iff, ← Filter.EventuallyEq] at h_add
Cleared hypotheses: h_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x))
    fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
⊢ (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
have refine : (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦
  (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
      rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
    (f x)
Tactic: refine h_add.trans ((Measure.rnDeriv_add' _ _ _).trans ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x))
    fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
⊢ (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
have refine_1 : (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)
Tactic: refine Filter.EventuallyEq.add ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x))
    fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
refine_1 :
  (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)
⊢ (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
have refine_2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦
  rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν) (f x)
Tactic: refine Filter.EventuallyEq.add ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x))
    fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
⊢ (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)
have refine_1 : (ae ν).EventuallyEq (β := ℝ≥0∞) 0 fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)
Tactic: refine (Measure.rnDeriv_singularPart μ ν).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x))
    fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞) 0 fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)
have refine_1 : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)) 0
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this_3 : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x))
    fun (x : α) ↦
    (rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
        rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν))
      (f x)
this :
  (ae (F := Measure β) (map f ν)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) x) 0
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)) 0
have this₁ : ∀ᵐ (x : α) ∂ν, rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x) = 0 (f x)
Tactic: rw [Filter.EventuallyEq, hf.ae_map_iff] at this
Cleared hypotheses: this