-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma _root_.MeasurableEmbedding.rnDeriv_map_aux (hf : MeasurableEmbedding f)
    (hμν : μ ≪ ν) [SigmaFinite μ] [SigmaFinite ν] :
    (fun x ↦ (μ.map f).rnDeriv (ν.map f) (f x)) =ᵐ[ν] μ.rnDeriv ν

Proof state:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Tactic:
have hs_eq : s = f ⁻¹' (f '' s) := by rw [hf.injective.preimage_image]

Result:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
hs_eq : s = f ⁻¹' (f '' s)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Proof state:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
hs_eq : s = f ⁻¹' (f '' s)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Tactic:
have : SigmaFinite (ν.map f) := hf.sigmaFinite_map

Result:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
hs_eq : s = f ⁻¹' (f '' s)
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ s = f ⁻¹' (f '' s)

Tactic:
rw [hf.injective.preimage_image]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (fun x => (map f μ).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable fun x => (map f μ).rnDeriv (map f ν) (f x)

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)

case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν

Proof state:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν

Tactic:
rw [← hf.lintegral_map, Measure.setLIntegral_rnDeriv hμν]

Result:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable fun x => (map f μ).rnDeriv (map f ν) (f x)

Tactic:
exact (Measure.measurable_rnDeriv _ _).comp hf.measurable

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
exact Measure.measurable_rnDeriv _ _

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
hs_eq : s = f ⁻¹' (f '' s)
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Tactic:
rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
  hf.map_apply]

Result:
no goals