awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν_1 : Measure A
g_1 : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x

Tactic:
exact measurable_const_smul ..

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ Eq (α := ENNReal) ((g • μ : (a : Set A) → ENNReal) s : ENNReal)
    ((μ : (a : Set A) → ENNReal) (HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s) : ENNReal)

Tactic:
((MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)).map_apply _).trans ?_

Premises used: MeasurableEquiv.map_apply, DomMulAct.mk, Inv.inv, MulOpposite.unop, Equiv.symm, DFunLike.coe, Eq.trans, MeasurableEquiv.smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
refine :
  Eq (α := ENNReal)
    ((μ : (a : Set A) → ENNReal)
        ((⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹'
          s) :
      ENNReal)
    ((μ : (a : Set A) → ENNReal) (HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s) : ENNReal)
⊢ Eq (α := ENNReal) ((g • μ : (a : Set A) → ENNReal) s : ENNReal)
    ((μ : (a : Set A) → ENNReal) (HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s) : ENNReal)

Tactic:
refine ((MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)).map_apply _).trans ?_

Premises used: MeasurableEquiv.map_apply, DomMulAct.mk, Inv.inv, Equiv.symm, DFunLike.coe, Eq.trans, MeasurableEquiv.smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
h :
  (⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹' s =
    HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s
⊢ Eq (α := ENNReal)
    ((μ : (a : Set A) → ENNReal)
        ((⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹'
          s) :
      ENNReal)
    ((μ : (a : Set A) → ENNReal) (HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s) : ENNReal)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ (⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹' s =
    HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s

Tactic:
Set.preimage_smul_inv (DomMulAct.mk.symm g) s

Premises used: DomMulAct.mk, Set.preimage_smul_inv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ (⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹' s =
    HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s

Tactic:
exact Set.preimage_smul_inv (DomMulAct.mk.symm g) s

Premises used: DomMulAct.mk, Set.preimage_smul_inv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
r : ℝ≥0
g : Gᵈᵐᵃ
μ : Measure A
⊢ HSMul.hSMul (β := Measure A) r
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) μ) =
    map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) (r • μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ ν : Measure A
g : G
⊢ SMulCommClass.{u_1, 0, u_2} Gᵈᵐᵃ ℝ≥0 (Measure A)

Tactic:
.symm ..

Premises used: SMulCommClass.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
rw : ν.withDensity (μ.rnDeriv ν)
| μ

Tactic:
rw [haveLebesgueDecomposition_add μ ν, this, zero_add]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, zero_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
conv_rhs : ν.withDensity (μ.rnDeriv ν) = μ
conv_rhs₁ : ν.withDensity (μ.rnDeriv ν) = ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, zero_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
suffices : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
suffices μ.singularPart ν = 0 by
    conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ μ.singularPart ν = 0

Tactic:
(singularPart_eq_zero μ ν).mpr h

Premises used: Iff.mpr, MeasureTheory.Measure.singularPart_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ μ.singularPart ν = 0

Tactic:
exact (singularPart_eq_zero μ ν).mpr h

Premises used: Iff.mpr, MeasureTheory.Measure.singularPart_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ μ ≪ ν ↔ ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
⟨withDensity_rnDeriv_eq μ ν, fun h => h ▸ withDensity_absolutelyContinuous _ _⟩

Premises used: MeasureTheory.Measure.rnDeriv, Eq.rec, Iff.intro, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
rw : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x
⊢ ∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x

Tactic:
rw [← Measure.withDensity_rnDeriv_eq _ _ hμν,
    ae_withDensity_iff (Measure.measurable_rnDeriv _ _), Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.ae_withDensity_iff, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x

Tactic:
ae_of_all _ (fun x hx ↦ hx.pos)

Premises used: Ne.pos, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x

Tactic:
exact ae_of_all _ (fun x hx ↦ hx.pos)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x

Tactic:
(absolutelyContinuous_withDensity_rnDeriv hμν).ae_le ?_

Premises used: Filter.Eventually, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
refine : {x : α | (fun (x : α) ↦ 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))
⊢ ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x

Tactic:
refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_le ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_le, MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
h :
  ∀ (x : α) (hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x)
    (hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x), 0 < ν.rnDeriv μ x
⊢ {x : α | (fun (x : α) ↦ 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))

Tactic:
filter_upwards [Measure.rnDeriv_pos (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)),
    (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).ae_le
    (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ))] with x hx hx2

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
x : α
hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x
hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x
h h₁ h₂ h₃ : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x
⊢ 0 < ν.rnDeriv μ x

Tactic:
rwa [← hx2]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
| (μ.withDensity f).rnDeriv ν

Tactic:
rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm, MeasureTheory.withDensity_add_measure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
conv_rhs :
  ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν

Tactic:
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm, MeasureTheory.withDensity_add_measure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ SigmaFinite ((μ.singularPart ν).withDensity f)

Tactic:
have : SigmaFinite ((μ.singularPart ν).withDensity f) :=
    SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.singularPart_le _ _) hf_ne_top)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : SigmaFinite ((μ.singularPart ν).withDensity f)
⊢ SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f)

Tactic:
have : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f) :=
    SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.withDensity_rnDeriv_le _ _) hf_ne_top)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this_1 : SigmaFinite ((μ.singularPart ν).withDensity f)
this : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Tactic:
(rnDeriv_add_of_mutuallySingular _ _ _ (mutuallySingular_singularPart μ ν).withDensity).symm

Premises used: MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.withDensity, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this_1 : SigmaFinite ((μ.singularPart ν).withDensity f)
this : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Tactic:
exact (rnDeriv_add_of_mutuallySingular _ _ _ (mutuallySingular_singularPart μ ν).withDensity).symm

Premises used: MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.withDensity, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
rw : (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
| μ.rnDeriv (ν.withDensity f)

Tactic:
rw [μ.haveLebesgueDecomposition_add ν, add_comm]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
conv_rhs :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)

Tactic:
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
⊢ ν ≪ ν.withDensity f

Tactic:
have hν_ac : ν ≪ ν.withDensity f := withDensity_absolutelyContinuous' hf hf_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)

Tactic:
hν_ac.ae_eq ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
refine :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)

Tactic:
refine hν_ac.ae_eq ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
⊢ SigmaFinite (ν.withDensity f)

Tactic:
have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
this : SigmaFinite (ν.withDensity f)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)

Tactic:
(rnDeriv_add_of_mutuallySingular _ _ _ ?_).symm

Premises used: MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
this : SigmaFinite (ν.withDensity f)
refine : μ.singularPart ν ⟂ₘ ν.withDensity f
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)

Tactic:
refine (rnDeriv_add_of_mutuallySingular _ _ _ ?_).symm

Premises used: MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
this : SigmaFinite (ν.withDensity f)
⊢ μ.singularPart ν ⟂ₘ ν.withDensity f

Tactic:
((mutuallySingular_singularPart μ ν).symm.withDensity).symm

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.withDensity, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
this : SigmaFinite (ν.withDensity f)
⊢ μ.singularPart ν ⟂ₘ ν.withDensity f

Tactic:
exact ((mutuallySingular_singularPart μ ν).symm.withDensity).symm

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.withDensity, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x

Tactic:
(Measure.eq_rnDeriv₀ ?_ Measure.MutuallySingular.zero_left ?_).symm

Premises used: MeasureTheory.Measure.eq_rnDeriv₀, MeasureTheory.Measure.MutuallySingular.zero_left, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
refine_1 : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ f x * μ.rnDeriv ν x) ν
refine_2 : μ.withDensity f = 0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x

Tactic:
refine (Measure.eq_rnDeriv₀ ?_ Measure.MutuallySingular.zero_left ?_).symm

Premises used: MeasureTheory.Measure.eq_rnDeriv₀, MeasureTheory.Measure.MutuallySingular.zero_left, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ f x * μ.rnDeriv ν x) ν

Tactic:
hf.mul (Measure.measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, AEMeasurable.mul, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ f x * μ.rnDeriv ν x) ν

Tactic:
exact hf.mul (Measure.measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, AEMeasurable.mul, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
refine_2 :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity f = 0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
refine_2 : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]

Premises used: zero_add, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν)
| ∫⁻ (a : α) in s, f a ∂μ

Tactic:
rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
refine_2 : ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

Tactic:
conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq