-- Mathlib/MeasureTheory/Decomposition/IntegralRNDeriv.lean
/-- For a convex continuous function `f` on `[0, ∞)`, if `μ` is absolutely continuous
with respect to `ν`, then
`(ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν`. -/
lemma mul_le_integral_rnDeriv_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousWithinAt f (Ici 0) 0)
    (hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) (hμν : μ ≪ ν) :
    (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal)
      ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
⊢ (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
have : NeZero ν := ⟨hν⟩

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this : NeZero ν
⊢ (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹ • μ.rnDeriv ν'
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
have h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν :=
  Measure.rnDeriv_smul_right_of_ne_top' (μ := ν) (ν := μ) (by simp) (by simp [hν])

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2 : μ.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν

Proof state:
case neg.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
h : (ν univ).toReal * f (μ' univ).toReal ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
⊢ (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
convert h

Result:
case h.e'_3.h.e'_6.h.e'_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
h : (ν univ).toReal * f (μ' univ).toReal ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
⊢ (μ univ).toReal / (ν univ).toReal = (μ' univ).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹ • μ.rnDeriv ν'
⊢ (ν univ)⁻¹ ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case neg.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
⊢ (fun x => f (μ'.rnDeriv ν' x).toReal) =ᶠ[ae ν] fun x => f (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [h_rnDeriv_eq] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
x : α
hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x
⊢ f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal