awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal) ν

Tactic:
integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable
    (Measure.lintegral_rnDeriv_lt_top _ _).ne

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.lintegral_rnDeriv_lt_top, MeasureTheory.integrable_toReal_of_lintegral_ne_top, MeasureTheory.Measure.measurable_rnDeriv, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
inl : ∀ (hx : Membership.mem (γ := Set ℝ) (Ici 0) 0), ContinuousWithinAt f (Ici 0) 0
inr : ∀ (hx_pos : 0 < x), ContinuousWithinAt f (Ici 0) x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hx : Membership.mem (γ := Set ℝ) (Ici 0) 0
⊢ ContinuousWithinAt f (Ici 0) 0

Tactic:
hf_cont
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hx : Membership.mem (γ := Set ℝ) (Ici 0) 0
⊢ ContinuousWithinAt f (Ici 0) 0

Tactic:
exact hf_cont
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
⊢ Membership.mem (γ := Set ℝ) (interior (Ici 0)) x → ContinuousWithinAt f (interior (Ici 0)) x

Tactic:
have h := hf_cvx.continuousOn_interior x
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : Membership.mem (γ := Set ℝ) (interior (Ici 0)) x → ContinuousWithinAt f (interior (Ici 0)) x
⊢ 0 < x → ContinuousWithinAt f (Ioi 0) x

Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h

Premises used: Set.mem_Ioi, Set.nonempty_Iio, interior_Ici'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : 0 < x → ContinuousWithinAt f (Ioi 0) x
⊢ 0 < x → ContinuousAt f x

Tactic:
rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h

Premises used: Ioi_mem_nhds, continuousWithinAt_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : 0 < x → ContinuousAt f x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
(h hx_pos).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : 0 < x → ContinuousAt f x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
exact (h hx_pos).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
⊢ ContinuousOn f (Ici 0)

Tactic:
have hf_cont' : ContinuousOn f (Ici 0) := by
    intro x hx
    rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos
    · exact hf_cont
    · have h := hf_cvx.continuousOn_interior x
      simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h
      rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h
      exact (h hx_pos).continuousWithinAt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
rw rw₁ : f (μ.real univ) = f (μ.real univ)
⊢ f (μ.real univ) = f (∫ (x : 𝓧), (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
rw [Measure.integral_toReal_rnDeriv hμν]

Premises used: MeasureTheory.Measure.integral_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
rw : f (⨍ (x : 𝓧), (μ.rnDeriv ν x).toReal ∂ν) ≤ ⨍ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ f (∫ (x : 𝓧), (μ.rnDeriv ν x).toReal ∂ν) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [← average_eq_integral, ← average_eq_integral]

Premises used: MeasureTheory.average_eq_integral
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ ∀ᵐ (x : 𝓧) ∂ν, Membership.mem (γ := Set ℝ) (Ici 0) (μ.rnDeriv ν x).toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ f (⨍ (x : 𝓧), (μ.rnDeriv ν x).toReal ∂ν) ≤ ⨍ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
exact ConvexOn.map_average_le hf_cvx hf_cont' isClosed_Ici (by simp)
      Measure.integrable_toReal_rnDeriv hf_int

Premises used: ConvexOn.map_average_le, isClosed_Ici, MeasureTheory.Measure.integrable_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
calc : f (μ.real univ) = f (∫ (x : 𝓧), (μ.rnDeriv ν x).toReal ∂ν)
calc₁ : f (∫ (x : 𝓧), (μ.rnDeriv ν x).toReal ∂ν) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ f (μ.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
calc f (μ.real univ)
    = f (∫ x, (μ.rnDeriv ν x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν]
  _ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := by
    rw [← average_eq_integral, ← average_eq_integral]
    exact ConvexOn.map_average_le hf_cvx hf_cont' isClosed_Ici (by simp)
      Measure.integrable_toReal_rnDeriv hf_int

Premises used: Set.univ, MeasureTheory.Measure.real, MeasureTheory.Measure.rnDeriv, ENNReal.toReal, MeasureTheory.integral
-- 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μν : μ ≪ ν
pos : ∀ (hν : ν = 0), ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
neg : ∀ (hν : ¬ν = 0), ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
by_cases hν : ν = 0
-- 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
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

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
⊢ NeZero ν

Tactic:
have : NeZero ν := ⟨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 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
⊢ 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 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
⊢ IsFiniteMeasure μ'

Tactic:
have : IsFiniteMeasure μ' := μ.smul_finite (by 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 μ'
⊢ μ' ≪ ν'

Tactic:
have hμν' : μ' ≪ ν' := hμν.smul _
-- 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μν' : μ' ≪ ν'
⊢ 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μν' : μ' ≪ ν'
⊢ μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')

Tactic:
have h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν' :=
      Measure.rnDeriv_smul_left_of_ne_top' (μ := ν') (ν := μ) (by 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 ν')
hc : Ne (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')

Tactic:
rwa [Measure.ae_ennreal_smul_measure_eq] at h1'

Premises used: MeasureTheory.Measure.ae_ennreal_smul_measure_eq
-- 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 ν')
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')

Tactic:
have h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν' := by
      rwa [Measure.ae_ennreal_smul_measure_eq] at h1'
      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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
⊢ 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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
⊢ μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)

Tactic:
have h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν :=
      Measure.rnDeriv_smul_right_of_ne_top' (μ := ν) (ν := μ) (by simp) (by 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 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
h :
  ∀ (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),
    μ'.rnDeriv ν' x = μ.rnDeriv ν x
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
filter_upwards [h1, h2] with x h1 h2
-- 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 :
  HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x) =
    μ.rnDeriv ν x
⊢ μ'.rnDeriv ν' x = μ.rnDeriv ν x

Tactic:
rw [h1, Pi.smul_apply, smul_eq_mul, h2]

Premises used: smul_eq_mul, Pi.smul_apply
-- 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 :
  HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (μ.rnDeriv ν x)) =
    μ.rnDeriv ν x
⊢ HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x) =
    μ.rnDeriv ν x

Tactic:
simp only [inv_inv, Pi.smul_apply, smul_eq_mul]

Premises used: inv_inv, smul_eq_mul, Pi.smul_apply