-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma inv_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Proof state:
case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

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

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : 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 _ _)

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x

Tactic:
exact hx.symm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
constructor

Result:
case left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹

case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ (μ.rnDeriv ν)⁻¹ x = (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ x

Tactic:
simp only [Pi.inv_apply, inv_inj]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.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 _ _)

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Proof state:
case left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹

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

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ (μ.rnDeriv ν)⁻¹ x = (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ

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

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ