awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞) (fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)) 0
have refine_1 : (ae (F := Measure β) (map f ν)).EventuallyEq (β := ℝ≥0∞)
  (fun (x : β) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) x) 0
Tactic: suffices (fun x ↦ ((μ.singularPart ν).map f).rnDeriv (ν.map f) x) =ᵐ[ν.map f] 0 by
      rw [Filter.EventuallyEq, hf.ae_map_iff] at this
      exact this
-- 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 (F := Measure β) (map f ν)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) x) 0
have refine_1 : @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)
Tactic: refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl
-- 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 ν
⊢ Eq (α := Measure β) (map f (ν.withDensity (μ.rnDeriv ν)))
    (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- 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 ν
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν
Tactic: rw [hf.map_apply, withDensity_apply _ (hf.measurable hs), withDensity_apply _ hs,
    setLIntegral_map hs (Measure.measurable_rnDeriv _ _) hf.measurable]
-- 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 ν
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν
have h : ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
Tactic: refine setLIntegral_congr_fun_ae (hf.measurable hs) ?_
-- 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 ν
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) x = μ.rnDeriv ν x) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) x} x}
    a
Tactic: filter_upwards [hf.rnDeriv_map μ ν] with a ha _ using ha.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 ν
s : Set β
hs : MeasurableSet s
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) x = μ.rnDeriv ν x) x}
            x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) x} x}
      a
⊢ ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
have h₁ : ∀ (a : α),
  rnDeriv (m := mβ) (map f μ) (map f ν) (f a) = μ.rnDeriv ν a →
    a ∈ f ⁻¹' s → μ.rnDeriv ν a = rnDeriv (m := mβ) (map f μ) (map f ν) (f a)
Tactic: filter_upwards [hf.rnDeriv_map μ ν] with a ha _ using ha.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 ν
| map f μ
have rw : map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
Tactic: rw [μ.haveLebesgueDecomposition_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 ν
⊢ map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
have conv_lhs : map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
  HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
Tactic: conv_lhs => rw [μ.haveLebesgueDecomposition_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 ν
⊢ map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
have rw : HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν))) =
  HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
Tactic: rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]
-- 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 ν
rw :
  HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν))) =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
⊢ map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
have rw₁ : HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν))) =
  HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))
Tactic: rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]
-- 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 ν
⊢ Eq (α := Measure β) (singularPart (map f μ) (map f ν)) (map f (μ.singularPart ν))
have h_add : map f μ =
  HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
Tactic: have h_add : μ.map f = (μ.singularPart ν).map f
      + (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f)) := by
    conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
    rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]
-- 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 ν
h_add :
  map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
⊢ Eq (α := Measure β) (singularPart (map f μ) (map f ν)) (map f (μ.singularPart ν))
have refine : @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)
Tactic: refine (Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ
have nth_rw : ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)
Tactic: nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)
have rw : ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α), (μ.rnDeriv ν * f) a ∂ν
Tactic: rw [lintegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂μ
have nth_rw : ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)
Tactic: nth_rw 2 [← Measure.withDensity_rnDeriv_eq μ ν hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)
have rw : ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν
Tactic: rw [setLIntegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Integrable.{u_4, u_3} (ε := E) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ
have nth_rw : Integrable.{u_4, u_3} (ε := E) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔
  Integrable f (ν.withDensity (μ.rnDeriv ν))
Tactic: nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Integrable.{u_4, u_3} (ε := E) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔
    Integrable f (ν.withDensity (μ.rnDeriv ν))
have rw : Integrable f (ν.withDensity (μ.rnDeriv ν)) ↔ Integrable f (ν.withDensity (μ.rnDeriv ν))
Tactic: rw [← integrable_withDensity_iff_integrable_smul' (E := E)
    (measurable_rnDeriv μ ν) (rnDeriv_lt_top μ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α), f x ∂μ)
have rw : Eq.{u_4 + 1} (α := E) (∫ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)) (∫ (x : α), f x ∂μ)
Tactic: rw [← integral_withDensity_eq_integral_toReal_smul (measurable_rnDeriv _ _) (rnDeriv_lt_top _ _),
    withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
rw : Eq.{u_4 + 1} (α := E) (∫ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α), f x ∂μ)
have rw₁ : Eq.{u_4 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
Tactic: rw [← integral_withDensity_eq_integral_toReal_smul (measurable_rnDeriv _ _) (rnDeriv_lt_top _ _),
    withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α) in s, f x ∂μ)
have hf : Measurable (μ.rnDeriv ν)
Tactic: rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul, withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
hf : Measurable (μ.rnDeriv ν)
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α) in s, f x ∂μ)
have hf_top : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
Tactic: rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul, withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SigmaFinite μ
f : α → E
inst_3 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α) in s, f x ∂μ)
have hf : Measurable (μ.rnDeriv ν)
Tactic: rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul', withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SigmaFinite μ
f : α → E
inst_3 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
hf : Measurable (μ.rnDeriv ν)
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α) in s, f x ∂μ)
have hf_top : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
Tactic: rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul', withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)
have rw : ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ) ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
Tactic: rw [← mconv_withDensity_eq_mlconvolution (by fun_prop) (by fun_prop),
    withDensity_rnDeriv_eq _ _ hν₁, withDensity_rnDeriv_eq _ _ hν₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
rw : ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ) ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)
have rw₁ : ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
Tactic: rw [← mconv_withDensity_eq_mlconvolution (by fun_prop) (by fun_prop),
    withDensity_rnDeriv_eq _ _ hν₁, withDensity_rnDeriv_eq _ _ hν₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
rw : ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ) ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
rw₁ : ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)
have rw₂ : ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ ν₂
Tactic: rw [← mconv_withDensity_eq_mlconvolution (by fun_prop) (by fun_prop),
    withDensity_rnDeriv_eq _ _ hν₁, withDensity_rnDeriv_eq _ _ hν₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ
have this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
Tactic: have := HaveLebesgueDecomposition.mconv hν₁ hν₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ
have rw : ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞
Tactic: rw [← withDensity_eq_iff (by fun_prop) (by fun_prop),
    withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂),
    mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SigmaFinite μ
ν₁ ν₂ : Measure G
inst_5 : SigmaFinite ν₁
inst_6 : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ
have rw : μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite (by fun_prop) (by fun_prop),
    ← mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂,
    withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SigmaFinite μ
ν₁ ν₂ : Measure G
inst_5 : SigmaFinite ν₁
inst_6 : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
rw : μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ
have rw₁ : μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = ν₁ ∗ₘ ν₂
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite (by fun_prop) (by fun_prop),
    ← mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂,
    withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SigmaFinite μ
ν₁ ν₂ : Measure G
inst_5 : SigmaFinite ν₁
inst_6 : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
rw : μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)
rw₁ : μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = ν₁ ∗ₘ ν₂
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ
have rw₂ : ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ ν₂
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite (by fun_prop) (by fun_prop),
    ← mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂,
    withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : (↑v : Set α → M) = (↑w : Set α → M)
⊢ v = w
have mk : ∀ (measureOf' : Set α → M) (empty' : measureOf' ∅ = 0)
  (not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0)
  (m_iUnion' :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf' (f i)) (measureOf' (⋃ (i : ℕ), f i)))
  (h :
    (↑{ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
            VectorMeasure α M } :
        Set α → M) =
      (↑w : Set α → M)),
  { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
      VectorMeasure α M } =
    w
Tactic: cases v
Cleared hypotheses: v, h