awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ μ.singularPart ν' ⟂ₘ ν'

Tactic:
mutuallySingular_singularPart μ ν'

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ μ.singularPart ν' ⟂ₘ ν'

Tactic:
exact mutuallySingular_singularPart μ ν'

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
rw : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
| μ.rnDeriv ν

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 α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
conv_rhs : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv ν

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 α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)

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

Premises used: MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv, MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
refine :
  μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae (μ.withDensity (ν.rnDeriv μ))]
    μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)

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

Premises used: MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv, MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae (μ.withDensity (ν.rnDeriv μ))]
    μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)

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

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.withDensity, Filter.EventuallyEq.symm, MeasureTheory.Measure.MutuallySingular.symm, MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae (μ.withDensity (ν.rnDeriv μ))]
    μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)

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

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.withDensity, Filter.EventuallyEq.symm, MeasureTheory.Measure.MutuallySingular.symm, MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
this : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ

Tactic:
(rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm

Premises used: Measurable.inv, MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
this : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
rw rw₁ : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
this : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
⊢ (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
rnDeriv_withDensity _ (measurable_rnDeriv _ _)

Premises used: MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
this : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
calc : (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
calc (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
          (rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
    _ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
    _ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.Measure.rnDeriv, Inv.inv, Measurable.inv, MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
suffices : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
suffices μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ) by
    calc (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
          (rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
    _ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
    _ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
rw : (ν.withDensity (μ.rnDeriv ν)).withDensity ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ = ν
⊢ μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)

Tactic:
rw [withDensity_rnDeriv_eq _ _ hνμ, ← withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
rw : (μ.rnDeriv ν)⁻¹
| ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹

Tactic:
rw [withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
conv : (ν.withDensity (μ.rnDeriv ν)).withDensity (μ.rnDeriv ν)⁻¹ = ν
⊢ (ν.withDensity (μ.rnDeriv ν)).withDensity ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ = ν

Tactic:
conv in ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ => rw [withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
x : α
hx : 0 < μ.rnDeriv ν x
⊢ μ.rnDeriv ν x ≠ 0

Tactic:
hx.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 < μ.rnDeriv ν x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : 0 < μ.rnDeriv ν x), μ.rnDeriv ν x ≠ 0
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0

Tactic:
filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne'

Premises used: MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
rw rw₁ : ν = ν
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity fun (x : α) ↦ (μ.rnDeriv ν x)⁻¹) = ν

Tactic:
rw [withDensity_inv_same (measurable_rnDeriv _ _)
    (by filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne')
    (rnDeriv_ne_top _ _)]

Premises used: MeasureTheory.withDensity_inv_same, MeasureTheory.Measure.rnDeriv_ne_top, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
(this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))

Premises used: Filter.EventuallyEq.trans, And.right, And.left, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
refine : (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))

Premises used: Filter.EventuallyEq.trans, And.right, And.left, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)

Premises used: MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.inv_rnDeriv_aux, MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)

Premises used: MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.inv_rnDeriv_aux, MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
suffices :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
suffices (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
      ∧ ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ by
    refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
    exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
left : (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
right : ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h :
  ∀ (x : α) (hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x),
    (μ.rnDeriv ν)⁻¹ x = (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ x
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹

Tactic:
filter_upwards [rnDeriv_withDensity_rnDeriv hμν] with x hx

Premises used: MeasureTheory.Measure.rnDeriv_withDensity_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
h : μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x
⊢ (μ.rnDeriv ν)⁻¹ x = (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ x

Tactic:
simp only [Pi.inv_apply, inv_inj]

Premises used: inv_inj, Pi.inv_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x

Tactic:
hx.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x

Tactic:
exact hx.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
(Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ)).symm

Premises used: MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
exact (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ)).symm

Premises used: MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : ∀ (x : α) (hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x), (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x
⊢ (ν.rnDeriv μ)⁻¹ =ᶠ[ae μ] μ.rnDeriv ν

Tactic:
filter_upwards [inv_rnDeriv hμν] with x hx

Premises used: MeasureTheory.Measure.inv_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x

Tactic:
simp only [Pi.inv_apply, ← hx, inv_inv]

Premises used: inv_inv, Pi.inv_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
rw :
  (∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x) ∧
    ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
⊢ ∀ᵐ (a : α) ∂ν, μ.rnDeriv ν a ≠ 0 → p a

Tactic:
rw [ν.haveLebesgueDecomposition_add μ, ae_add_measure_iff]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.ae_add_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
left : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
right : ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
⊢ (∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x) ∧
    ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
left : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x ≠ 0 → p x
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

Tactic:
rw [← ν.haveLebesgueDecomposition_add μ]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0

Tactic:
have : ∀ᵐ x ∂(ν.singularPart μ), μ.rnDeriv ν x = 0 := μ.rnDeriv_eq_zero_ae_singularPart ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
this : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
x : α
hx : μ.rnDeriv ν x = 0
h_absurd : μ.rnDeriv ν x ≠ 0
⊢ p x

Tactic:
absurd hx h_absurd

Premises used: absurd
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
this : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = 0) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0 → p x) x} x}
      a
h₂ h₃ : ∀ (x : α) (hx : μ.rnDeriv ν x = 0) (h_absurd : μ.rnDeriv ν x ≠ 0), p x
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x ≠ 0 → p x

Tactic:
filter_upwards [this] with x hx h_absurd using absurd hx h_absurd
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ μ.withDensity (ν.rnDeriv μ) ≪ μ

Tactic:
have h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ := withDensity_absolutelyContinuous _ _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
right : ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv ν x ≠ 0 → p x
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

Tactic:
rw [← ν.haveLebesgueDecomposition_add μ]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
right : ∀ᵐ (x : α) ∂μ, μ.rnDeriv ν x ≠ 0 → p x
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv ν x ≠ 0 → p x

Tactic:
suffices ∀ᵐx ∂μ, μ.rnDeriv ν x ≠ 0 → p x from h_ac this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h_1 : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
a : α
h : p a
h₁ : μ.rnDeriv ν a ≠ 0 → p a
⊢ μ.rnDeriv ν a ≠ 0 → p a

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h_1 : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
a : α
h : p a
h_2 : μ.rnDeriv ν a ≠ 0
⊢ p a

Tactic:
h