awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1_1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2_1 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
x : 𝓧
h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x
h : Ne (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (μ.rnDeriv ν x)) =
    μ.rnDeriv ν x

Tactic:
rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]

Premises used: mul_assoc, ENNReal.inv_mul_cancel, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1_1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2_1 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
x : 𝓧
h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [hν]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1_1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2_1 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
x : 𝓧
h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
have h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν := by
    have h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν' :=
      Measure.rnDeriv_smul_left_of_ne_top' (μ := ν') (ν := μ) (by simp [hν])
    have h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν' := by
      rwa [Measure.ae_ennreal_smul_measure_eq] at h1'
      simp
    have h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν :=
      Measure.rnDeriv_smul_right_of_ne_top' (μ := ν) (ν := μ) (by simp) (by simp [hν])
    filter_upwards [h1, h2] with x h1 h2
    rw [h1, Pi.smul_apply, smul_eq_mul, h2]
    simp only [inv_inv, Pi.smul_apply, smul_eq_mul]
    rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]
    · simp [hν]
    · simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
rw :
  (ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ))⁻¹ * ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν =
    (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [integral_smul_measure, smul_eq_mul, ENNReal.toReal_inv]

Premises used: ENNReal.toReal_inv, smul_eq_mul, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
e_a : Eq (α := ℝ) (∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν) (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν)
⊢ (ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ))⁻¹ * ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν =
    (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
⊢ Eq (α := ℝ) (∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν) (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
e_a : (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal
⊢ Eq (α := ℝ) (∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν) (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h : ∀ (x : 𝓧) (hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x), f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [h_rnDeriv_eq] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
x : 𝓧
hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x
h h₁ : f (μ.rnDeriv ν x).toReal = f (μ.rnDeriv ν x).toReal
⊢ f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
⊢ ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
have h_eq : ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν'
      = (ν.real univ)⁻¹ * ∫ x, f ((μ.rnDeriv ν x).toReal) ∂ν := by
    rw [integral_smul_measure, smul_eq_mul, ENNReal.toReal_inv]
    congr 1
    refine integral_congr_ae ?_
    filter_upwards [h_rnDeriv_eq] with x hx
    rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
neg :
  ∀ (h : f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν'),
    ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
neg₁ : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν'
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
have h : f (μ'.real univ) ≤ ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν' :=
    le_integral_rnDeriv_of_ac hf_cvx hf_cont ?_ hμν'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [hν]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
neg : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν'

Tactic:
refine Integrable.smul_measure ?_ (by simp [hν])

Premises used: MeasureTheory.Integrable.smul_measure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν

Tactic:
(integrable_congr ?_).mpr hf_int

Premises used: Iff.mpr, MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
neg : (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν

Tactic:
refine (integrable_congr ?_).mpr hf_int

Premises used: Iff.mpr, MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : ∀ (x : 𝓧) (hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x), f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [h_rnDeriv_eq] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
x : 𝓧
hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x
h h₁ : f (μ.rnDeriv ν x).toReal = f (μ.rnDeriv ν x).toReal
⊢ f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν'
neg :
  ∀ (h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν),
    ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
neg₁ : ∀ (h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹), 0 < (ν.real univ)⁻¹
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [h_eq, mul_comm, ← div_le_iff₀, div_eq_inv_mul, inv_inv] at h

Premises used: div_le_iff₀, inv_inv, mul_comm, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h₁ : μ.real univ / ν.real univ = μ'.real univ
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
convert! h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ μ.real univ / ν.real univ = μ'.real univ

Tactic:
simp only [div_eq_inv_mul, Measure.smul_apply, smul_eq_mul, ENNReal.toReal_mul,
      ENNReal.toReal_inv, μ', measureReal_def]

Premises used: ENNReal.toReal_inv, ENNReal.toReal_mul, MeasureTheory.Measure.smul_apply, MeasureTheory.measureReal_def, smul_eq_mul, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : 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_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹
⊢ 0 < (ν.real univ)⁻¹

Tactic:
simp [ENNReal.toReal_pos_iff, hν, measureReal_def]

Premises used: ENNReal.toReal_pos_iff, MeasureTheory.measureReal_def