awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int_1 :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top_1 : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
⊢ f (μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
    f (∫⁻ (b : 𝓨), μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal
have rw : f (μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
  f (μ.rnDeriv ν a * ∫⁻ (a_1 : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, a_1) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal
Tactic: rw [lintegral_const_mul _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int_1 :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top_1 : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
⊢ f (∫⁻ (b : 𝓨), μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
    f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal
have e_a : ∫⁻ (b : 𝓨), μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a =
  ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int_1 :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top_1 : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
⊢ ∫⁻ (b : 𝓨), μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a =
    ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a
have e_a : (ae (F := Measure 𝓨) ((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨)).EventuallyEq (β := ℝ≥0∞)
  (fun (b : 𝓨) ↦ μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b)) fun (b : 𝓨) ↦ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int_1 :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top_1 : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
⊢ (ae (F := Measure 𝓨) ((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : 𝓨) ↦ μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b)) fun (b : 𝓨) ↦ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
have h : ∀ (a_1 : 𝓨),
  Membership.mem (γ := Set 𝓨)
    {x : 𝓨 |
      Membership.mem (γ := Set 𝓨)
          {x : 𝓨 |
            (fun (b : 𝓨) ↦ μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)) x}
          x →
        Membership.mem (γ := Set 𝓨)
          {x : 𝓨 |
            (fun (x : 𝓨) ↦
                Eq (α := ℝ≥0∞) ((fun (b : 𝓨) ↦ μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b)) x)
                  ((fun (b : 𝓨) ↦ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)) x))
              x}
          x}
    a_1
Tactic: filter_upwards [h_mul_eq] with b hb using hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int_1 :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top_1 : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
⊢ f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
    f (@integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal)
have rw : f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
  f (∫⁻ (a_1 : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, a_1) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal
Tactic: rw [integral_toReal (by fun_prop) h_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int_1 :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top_1 : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
⊢ f (@integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal) ≤
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal
have rw : f (⨍ (x : 𝓨), ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, x)).toReal ∂(η : (a : 𝓧) → Measure 𝓨) a) ≤
  ⨍ (x : 𝓨), f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, x)).toReal ∂(η : (a : 𝓧) → Measure 𝓨) a
Tactic: rw [← average_eq_integral, ← average_eq_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ ContinuousWithinAt f (Ici 0) x
have inl : ∀ (hx : Membership.mem (γ := Set ℝ) (Ici 0) 0), ContinuousWithinAt f (Ici 0) 0
Tactic: rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
inl : ∀ (hx : Membership.mem (γ := Set ℝ) (Ici 0) 0), ContinuousWithinAt f (Ici 0) 0
⊢ ContinuousWithinAt f (Ici 0) x
have inr : ∀ (hx_pos : 0 < x), ContinuousWithinAt f (Ici 0) x
Tactic: rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
⊢ ContinuousWithinAt f (Ici 0) x
have h : ContinuousWithinAt f (interior (Ici 0)) x
Tactic: have h := hf_cvx.continuousOn_interior x (by simpa)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : ContinuousWithinAt f (interior (Ici 0)) x
⊢ ContinuousWithinAt f (Ici 0) x
have h₁ : ContinuousAt f x
Tactic: simp only [nonempty_Iio, interior_Ici',
        continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
have hf_cont : 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_at
    · have h := hf_cvx.continuousOn_interior x (by simpa)
      simp only [nonempty_Iio, interior_Ici',
        continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h
      exact h.continuousWithinAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
have obtain : ∀ (c c' : ℝ) (h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x), Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
Tactic: obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x :=
    hf_cvx.exists_affine_le_real isClosed_Ici hf_cont.lowerSemicontinuousOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') ν
have funProp : ‖c'‖ₑ ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
Tactic: refine integrable_of_le_of_le (f := fun a ↦ f (μ.rnDeriv ν a).toReal)
    (g₁ := fun x ↦ c * (μ.rnDeriv ν x).toReal + c')
    (g₂ := fun x ↦ ∫ b, f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal ∂(η x))
    ?_ ?_ ?_ (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
have refine_2 : (ae ν).EventuallyLE (β := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal
Tactic: refine integrable_of_le_of_le (f := fun a ↦ f (μ.rnDeriv ν a).toReal)
    (g₁ := fun x ↦ c * (μ.rnDeriv ν x).toReal + c')
    (g₂ := fun x ↦ ∫ b, f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal ∂(η x))
    ?_ ?_ ?_ (by fun_prop) ?_