awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)

Tactic:
have h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) := by
    rw [Measure.integrable_compProd_iff]
    swap; · exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)
    simp only [ne_eq, enorm_ne_top, not_false_eq_true, integrable_const_enorm,
      Filter.eventually_true, integral_const, probReal_univ, smul_eq_mul, one_mul, true_and]
    rw [← integrable_norm_iff (by fun_prop)]
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
rw :
  Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
    Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
rw [h_iff_κ]
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
⟨fun h_int ↦ ?_, fun ⟨h_int1, h_int2⟩ ↦ h_int1.add h_int2⟩

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.Integrable, Real.log, Prod.fst, _private.0.InformationTheory.integrable_llr_compProd_iff.match_3, ENNReal.toReal, HAdd.hAdd, Iff.intro, MeasureTheory.Integrable.add, MeasureTheory.Measure.compProd
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
refine :
  ∀
    (h_int :
      Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)),
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
refine ⟨fun h_int ↦ ?_, fun ⟨h_int1, h_int2⟩ ↦ h_int1.add h_int2⟩
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
⊢ μ ≪ ν

Tactic:
have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_ac_μν₁ : μ ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν_1 : μ ≪ ν
h_ac_κη_1 : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
rw :
  Integrable (ε := ℝ)
      (fun (x : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal * (log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal))
      (ν ⊗ₘ η) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
⊢ Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)

Tactic:
rw [← integrable_rnDeriv_mul_log_iff h_ac,
      integrable_congr (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη)]

Premises used: MeasureTheory.integrable_congr, InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add, MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν_1 : μ ≪ ν
h_ac_κη_1 : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (ε := ℝ)
      (fun (x : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal * (log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal))
      (ν ⊗ₘ η) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)

Tactic:
integrable_toReal_rnDeriv_mul_iff h_ac

Premises used: MeasureTheory.integrable_toReal_rnDeriv_mul_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν_1 : μ ≪ ν
h_ac_κη_1 : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (ε := ℝ)
      (fun (x : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal * (log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal))
      (ν ⊗ₘ η) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)

Tactic:
exact integrable_toReal_rnDeriv_mul_iff h_ac

Premises used: MeasureTheory.integrable_toReal_rnDeriv_mul_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
⊢ Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)

Tactic:
have h_int_iff : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
      Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal +
        log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) := by
    have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
    rw [← integrable_rnDeriv_mul_log_iff h_ac,
      integrable_congr (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη)]
    exact integrable_toReal_rnDeriv_mul_iff h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
⊢ Integrable (llr μ ν) μ

Tactic:
have h_int1 := integrable_llr_of_integrable_llr_compProd h_ac (h_int_iff.2 h_int)
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)

Tactic:
rw [h_iff_κ] at h_int1
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
rw :
  ∀ (h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ))
    (h_int_iff :
      Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
        Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ))
    (h_int1 : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)),
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
rw₁ : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
rw [integrable_add_iff_integrable_right'] at h_int

Premises used: MeasureTheory.integrable_add_iff_integrable_right'
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
⟨h_int1, h_int⟩

Premises used: And.intro
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
exact ⟨h_int1, h_int⟩
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)

Tactic:
h_int1

Premises used: MeasureTheory.llr
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)

Tactic:
exact h_int1
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ μ ≪ ν

Tactic:
have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (llr μ ν) μ

Tactic:
have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp h_int
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
⊢ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp h_int
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
rw :
  (∀ᵐ (x : 𝓧) ∂μ, @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ log ((∂μ/∂ν) (x, y).1).toReal) ((κ : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦ @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖log ((∂μ/∂ν) (x, y).1).toReal‖) μ
rw₁ : AEStronglyMeasurable (β := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)

Tactic:
rw [Measure.integrable_compProd_iff]

Premises used: MeasureTheory.Measure.integrable_compProd_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
simp : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖log ((∂μ/∂ν) x).toReal‖) μ
⊢ (∀ᵐ (x : 𝓧) ∂μ, @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ log ((∂μ/∂ν) (x, y).1).toReal) ((κ : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦ @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖log ((∂μ/∂ν) (x, y).1).toReal‖) μ

Tactic:
simp only [ne_eq, enorm_ne_top, not_false_eq_true, integrable_const_enorm,
      Filter.eventually_true, integral_const, probReal_univ, smul_eq_mul, one_mul, true_and]

Premises used: ne_eq, Filter.eventually_true, MeasureTheory.integral_const, MeasureTheory.probReal_univ, MeasureTheory.integrable_const_enorm, smul_eq_mul, not_false_eq_true, enorm_ne_top, one_mul, true_and
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ AEStronglyMeasurable (llr μ ν) μ

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h_int_μν : Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ‖llr μ ν a‖) μ)
    (h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)),
    Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖log ((∂μ/∂ν) x).toReal‖) μ
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖log ((∂μ/∂ν) x).toReal‖) μ

Tactic:
rwa [← integrable_norm_iff (by fun_prop)] at h_int_μν

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ StronglyMeasurable (β := ℝ) fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ AEStronglyMeasurable (β := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)

Tactic:
have h_int1 : Integrable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ) := by
    rw [Measure.integrable_compProd_iff]
    · simp only [ne_eq, enorm_ne_top, not_false_eq_true, integrable_const_enorm,
      Filter.eventually_true, integral_const, probReal_univ, smul_eq_mul, one_mul, true_and]
      rwa [← integrable_norm_iff (by fun_prop)] at h_int_μν
    · exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)