awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f_1 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f_1)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f_1)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f_1 a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
h_1 :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
    (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞))
hf_eq :
  ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
hf'_eq :
  ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
e_s :
  ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) +
        ∫⁻ (c : γ),
          (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞)
          ((f' : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
e_s₁ :
  Measurable (β := ℝ≥0∞) fun (a_1 : β) ↦
    ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1)
⊢ ∫⁻ (x : β × γ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) x : ℝ≥0∞)
        ((f' : (a : β × γ) → ℝ≥0∞) x : ℝ≥0∞) ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞)
          ((f' : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [lintegral_add_left (SimpleFunc.measurable _), hf_eq, hf'_eq, ← lintegral_add_left]

Premises used: MeasureTheory.SimpleFunc.measurable, MeasureTheory.lintegral_add_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f_1 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f_1)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f_1)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f_1 a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
h_1 :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
    (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞))
hf_eq :
  ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
hf'_eq :
  ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (β := ℝ≥0∞) fun (a_1 : β) ↦
    ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1)

Tactic:
h_some_meas_integral f
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f_1 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f_1)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f_1)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f_1 a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
h_1 :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
    (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞))
hf_eq :
  ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
hf'_eq :
  ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (β := ℝ≥0∞) fun (a_1 : β) ↦
    ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1)

Tactic:
exact h_some_meas_integral f
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f_1 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f_1)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f_1)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f_1 a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
h_1 :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
    (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞))
hf_eq :
  ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
hf'_eq :
  ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
e_s :
  ∀ (b : β),
    ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) +
        ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ∫⁻ (c : γ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞)
          ((f' : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) +
        ∫⁻ (c : γ),
          (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞)
          ((f' : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f_1 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f_1)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f_1)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f_1 a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
h_1 :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
    (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞))
hf_eq :
  ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
hf'_eq :
  ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
b : β
e_s : Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (f : (a : β × γ) → ℝ≥0∞) (b, c)
⊢ ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) +
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
    ∫⁻ (c : γ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞)
        ((f' : (a : β × γ) → ℝ≥0∞) (b, c) : ℝ≥0∞) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
rw [lintegral_add_left]

Premises used: MeasureTheory.lintegral_add_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f_1 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f_1)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f_1)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f_1 a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
h_1 :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
    (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞))
hf_eq :
  ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
hf'_eq :
  ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
b : β
⊢ Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (f : (a : β × γ) → ℝ≥0∞) (b, c)

Tactic:
(SimpleFunc.measurable _).comp measurable_prodMk_left

Premises used: Measurable.comp, MeasureTheory.SimpleFunc.measurable, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f_1 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f_1)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f_1)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f_1 a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
n : ℕ
f f' : SimpleFunc (β × γ) ℝ≥0∞
h_1 :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
    (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞))
hf_eq :
  ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
hf'_eq :
  ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
b : β
⊢ Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (f : (a : β × γ) → ℝ≥0∞) (b, c)

Tactic:
exact (SimpleFunc.measurable _).comp measurable_prodMk_left

Premises used: Measurable.comp, MeasureTheory.SimpleFunc.measurable, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
change :
  ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
change ∫⁻ bc, f bc ∂(κ ⊗ₖ η) a = ∫⁻ b, ∫⁻ c, g b c ∂η (a, b) ∂κ a

Premises used: DFunLike.coe, ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
rw :
  ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (bc : β × γ), g bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
hf₁ : Measurable (Function.uncurry g)
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [← lintegral_compProd']

Premises used: ProbabilityTheory.Kernel.lintegral_compProd'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
simp_rw :
  ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (bc : β × γ), Function.curry f bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (bc : β × γ), g bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a

Tactic:
simp_rw [g, Function.curry_apply]

Premises used: Function.curry_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
hf₁ : Measurable f
⊢ Measurable (Function.uncurry g)

Tactic:
simp_rw [g, Function.uncurry_curry]

Premises used: Function.uncurry_curry
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ Measurable f

Tactic:
hf
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ Measurable f

Tactic:
exact hf
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a

Tactic:
have A : ∫⁻ z, f z ∂(κ ⊗ₖ η) a = ∫⁻ z, hf.mk f z ∂(κ ⊗ₖ η) a := lintegral_congr_ae hf.ae_eq_mk
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
h :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (a_1 : β) ↦ ∫⁻ (y : γ), f (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1)) fun (a_1 : β) ↦
    ∫⁻ (y : γ), AEMeasurable.mk f hf (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1)
⊢ ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
a_1 : β
ha : ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ), f (a_1, c) = AEMeasurable.mk f hf (a_1, c)
⊢ ∫⁻ (y : γ), f (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1) =
    ∫⁻ (y : γ), AEMeasurable.mk f hf (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1)

Tactic:
lintegral_congr_ae ha

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                    f (b, c) = AEMeasurable.mk f hf (b, c))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ≥0∞) ((fun (a_3 : β) ↦ ∫⁻ (y : γ), f (a_3, y) ∂(η : (a : α × β) → Measure γ) (a, a_3)) x)
                    ((fun (a_3 : β) ↦ ∫⁻ (y : γ), AEMeasurable.mk f hf (a_3, y) ∂(η : (a : α × β) → Measure γ) (a, a_3))
                      x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (a_1 : β)
    (ha : ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ), f (a_1, c) = AEMeasurable.mk f hf (a_1, c)),
    ∫⁻ (y : γ), f (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1) =
      ∫⁻ (y : γ), AEMeasurable.mk f hf (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (a_1 : β) ↦ ∫⁻ (y : γ), f (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1)) fun (a_1 : β) ↦
    ∫⁻ (y : γ), AEMeasurable.mk f hf (a_1, y) ∂(η : (a : α × β) → Measure γ) (a, a_1)

Tactic:
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_compProd, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
have B : ∫⁻ x, ∫⁻ y, f (x, y) ∂η (a, x) ∂κ a = ∫⁻ x, ∫⁻ y, hf.mk f (x, y) ∂η (a, x) ∂κ a := by
    apply lintegral_congr_ae
    filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha