awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
pos :
  ∀ (h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0),
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
      ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal *
        (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
have neg : ∀ (h_zero2 : ¬((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0),
  ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Tactic: by_cases h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔ Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have h_ac_μν : μ ≪ ν
Tactic: have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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_μν : μ ≪ ν
⊢ Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔ Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
Tactic: have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have rw : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
  Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Tactic: rw [← integrable_rnDeriv_mul_log_iff h_ac,
    integrable_congr (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη),
    integrable_toReal_rnDeriv_mul_iff h_ac]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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) (μ ⊗ₘ κ)
have rw : Integrable (llr μ ν) μ ↔
  (∀ᵐ (x : 𝓧) ∂μ, @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ llr μ ν (x, y).1) ((κ : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦ @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖llr μ ν (x, y).1‖) μ
Tactic: rw [Measure.integrable_compProd_iff]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
rw :
  Integrable (llr μ ν) μ ↔
    (∀ᵐ (x : 𝓧) ∂μ, @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ llr μ ν (x, y).1) ((κ : (a : 𝓧) → Measure 𝓨) x)) ∧
      Integrable (ε := ℝ)
        (fun (x : 𝓧) ↦ @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖llr μ ν (x, y).1‖) μ
⊢ Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
have rw₁ : AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
Tactic: rw [Measure.integrable_compProd_iff]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 μ ν) μ ↔
    (∀ᵐ (x : 𝓧) ∂μ, @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ llr μ ν (x, y).1) ((κ : (a : 𝓧) → Measure 𝓨) x)) ∧
      Integrable (ε := ℝ)
        (fun (x : 𝓧) ↦ @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖llr μ ν (x, y).1‖) μ
have simp : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖llr μ ν x‖) μ
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]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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‖) μ
have rw : Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ‖llr μ ν a‖) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖llr μ ν x‖) μ
Tactic: rw [← integrable_norm_iff (by fun_prop)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
    Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have h_iff_κ : 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)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have rw : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
  Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Tactic: rw [h_iff_κ]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have refine : ∀
  (h_int :
    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⟩
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
have rw : Integrable (ε := ℝ)
    (fun (x : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal * (log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal))
    (ν ⊗ₘ η) ↔
  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_κη)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have h_int_iff : 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
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have h_int1 : Integrable (llr μ ν) μ
Tactic: have h_int1 := integrable_llr_of_integrable_llr_compProd h_ac (h_int_iff.2 h_int)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have h_int1₁ : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
Tactic: rw [h_iff_κ] at h_int1
Cleared hypotheses: h_int1
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Tactic: rw [integrable_add_iff_integrable_right'] at h_int
Cleared hypotheses: h_int, h_int_iff, h_int1
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
have rw₁ : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)
Tactic: rw [integrable_add_iff_integrable_right'] at h_int
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have h_ac_μν : μ ≪ ν
Tactic: have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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_μν : μ ≪ ν
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
Tactic: have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have h_int_μν : Integrable (llr μ ν) μ
Tactic: have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp h_int
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 μ ν) μ
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Tactic: have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp h_int
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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) (μ ⊗ₘ κ)
have 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‖) μ
Tactic: rw [Measure.integrable_compProd_iff]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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‖) μ
⊢ Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
have rw₁ : AEStronglyMeasurable (β := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
Tactic: rw [Measure.integrable_compProd_iff]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ (∀ᵐ (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‖) μ
have simp : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖log ((∂μ/∂ν) x).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]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (x : 𝓧) ↦ ‖log ((∂μ/∂ν) x).toReal‖) μ
have rwa : ∀ (h_int_μν : Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ‖llr μ ν a‖) μ)
  (h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)),
  Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖log ((∂μ/∂ν) x).toReal‖) μ
Tactic: rwa [← integrable_norm_iff (by fun_prop)] at h_int_μν
Cleared hypotheses: h_int_μν, h_int_κη