awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 ν)
⊢ (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

Premises used: Filter.EventuallyEq, MeasurableEmbedding.ae_map_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 ν

Tactic:
h_add.trans ((Measure.rnDeriv_add' _ _ _).trans ?_).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_add', Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 :
  (μ.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)
⊢ (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
refine h_add.trans ((Measure.rnDeriv_add' _ _ _).trans ?_).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_add', Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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)

Tactic:
Filter.EventuallyEq.add ?_ ?_

Premises used: Filter.EventuallyEq.add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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)
refine_2 :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦
    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)

Tactic:
refine Filter.EventuallyEq.add ?_ ?_

Premises used: Filter.EventuallyEq.add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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)

Tactic:
(Measure.rnDeriv_singularPart μ ν).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : (ae ν).EventuallyEq (β := ℝ≥0∞) 0 fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)
⊢ (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)

Tactic:
refine (Measure.rnDeriv_singularPart μ ν).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 :
  (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)) 0
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞) 0 fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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
⊢ ∀ᵐ (x : α) ∂ν, rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x) = 0 (f x)

Tactic:
rw [Filter.EventuallyEq, hf.ae_map_iff] at this

Premises used: Filter.EventuallyEq, MeasurableEmbedding.ae_map_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : ∀ᵐ (x : α) ∂ν, rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x) = 0 (f x)
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)) 0

Tactic:
this

Premises used: Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : ∀ᵐ (x : α) ∂ν, rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x) = 0 (f x)
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) (f x)) 0

Tactic:
exact this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 :
  (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

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
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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

Tactic:
Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)
⊢ (ae (F := Measure β) (map f ν)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) x) 0

Tactic:
refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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)
⊢ @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)

Tactic:
hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

Premises used: MeasurableEmbedding.mutuallySingular_map, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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)
⊢ @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)

Tactic:
exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

Premises used: MeasurableEmbedding.mutuallySingular_map, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦
    rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν) (f x)

Tactic:
(hf.rnDeriv_map_aux (withDensity_absolutelyContinuous _ _)).symm

Premises used: MeasurableEmbedding.rnDeriv_map_aux, MeasureTheory.withDensity_absolutelyContinuous, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦
    rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν) (f x)

Tactic:
exact (hf.rnDeriv_map_aux (withDensity_absolutelyContinuous _ _)).symm

Premises used: MeasurableEmbedding.rnDeriv_map_aux, MeasureTheory.withDensity_absolutelyContinuous, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
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∞)
⊢ Eq (α := Measure β) (map f (ν.withDensity (μ.rnDeriv ν)))
    (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν
⊢ 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:
rw [hf.map_apply, withDensity_apply _ (hf.measurable hs), withDensity_apply _ hs,
    setLIntegral_map hs (Measure.measurable_rnDeriv _ _) hf.measurable]

Premises used: MeasureTheory.setLIntegral_map, MeasurableEmbedding.map_apply, MeasurableEmbedding.measurable, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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) ∂ν

Tactic:
setLIntegral_congr_fun_ae (hf.measurable hs) ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
⊢ ∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν

Tactic:
refine setLIntegral_congr_fun_ae (hf.measurable hs) ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : α
ha : rnDeriv (m := mβ) (map f μ) (map f ν) (f a) = μ.rnDeriv ν a
h : a ∈ f ⁻¹' s → μ.rnDeriv ν a = rnDeriv (m := mβ) (map f μ) (map f ν) (f a)
⊢ a ∈ f ⁻¹' s → μ.rnDeriv ν a = rnDeriv (m := mβ) (map f μ) (map f ν) (f a)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
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 : α
ha : rnDeriv (m := mβ) (map f μ) (map f ν) (f a) = μ.rnDeriv ν a
h : a ∈ f ⁻¹' s
⊢ μ.rnDeriv ν a = rnDeriv (m := mβ) (map f μ) (map f ν) (f a)

Tactic:
ha.symm

Premises used: Eq.symm