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 : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) a = Function.uncurry f a
⊢ ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b

Tactic:
simp only [Prod.forall, Function.uncurry_apply_pair] at h

Premises used: Prod.forall, Function.uncurry_apply_pair
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
simp_rw :
  ∫⁻ (bc : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (bc.1, bc.2) ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [← h]
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
⊢ Monotone F

Tactic:
have h_mono : Monotone F := fun i j hij b =>
    SimpleFunc.monotone_eapprox (Function.uncurry f) hij _
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
rw :
  ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (bc : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (bc.1, bc.2) ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [lintegral_iSup (fun n => (F n).measurable) h_mono]

Premises used: MeasureTheory.SimpleFunc.measurable, MeasureTheory.lintegral_iSup
-- 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_1 : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
a : β
hf₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)
h_mono₁ : Monotone.{0, u_3} (β := γ → ℝ≥0∞) fun (n : ℕ) (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)
⊢ ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, c) ∂(η : (a : α × β) → Measure γ) (a_1, a) =
    ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (a, c) ∂(η : (a : α × β) → Measure γ) (a_1, a)

Tactic:
rw [lintegral_iSup]

Premises used: MeasureTheory.lintegral_iSup
-- 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_1 : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)

Tactic:
fun n => (F n).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_1 : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)

Tactic:
exact fun n => (F n).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_1 : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ Monotone.{0, u_3} (β := γ → ℝ≥0∞) fun (n : ℕ) (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)

Tactic:
fun i j hij b => h_mono hij _

Premises used: Monotone, Prod.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_1 : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ Monotone.{0, u_3} (β := γ → ℝ≥0∞) fun (n : ℕ) (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)

Tactic:
exact fun i j hij b => h_mono hij _
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
⊢ ∀ (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)

Tactic:
have : ∀ b, ∫⁻ c, ⨆ n, F n (b, c) ∂η (a, b) = ⨆ n, ∫⁻ c, F n (b, c) ∂η (a, b) := by
    intro a
    rw [lintegral_iSup]
    · exact fun n => (F n).measurable.comp measurable_prodMk_left
    · exact fun i j hij b => h_mono hij _
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
simp_rw :
  ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ⨆ (n : ℕ),
        ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [this]
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
f' : SimpleFunc (β × γ) ℝ≥0∞
h₁ :
  ∀ (ab : β),
    ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab, c) ∂(η : (a : α × β) → Measure γ) (a, ab) =
      ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
          fun (b : β) ↦ (a, b))
        ab
⊢ Eq.{u_2 + 1} (α := (b : β) → ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b))
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))

Tactic:
ext1 ab
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
f' : SimpleFunc (β × γ) ℝ≥0∞
ab : β
⊢ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab, c) ∂(η : (a : α × β) → Measure γ) (a, ab) =
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
        fun (b : β) ↦ (a, b))
      ab

Tactic:
rfl
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
f' : SimpleFunc (β × γ) ℝ≥0∞
⊢ Eq.{u_2 + 1} (α := (b : β) → ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b))
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))

Tactic:
have :
      (fun b => ∫⁻ c, f' (b, c) ∂η (a, b)) =
        (fun ab => ∫⁻ c, f' (ab.2, c) ∂η ab) ∘ fun b => (a, b) := by
      ext1 ab; rfl
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this_1 :
  ∀ (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)
f' : SimpleFunc (β × γ) ℝ≥0∞
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b))
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))
rw :
  Measurable.{u_2, 0} (α := β) (β := ℝ≥0∞)
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
rw [this]
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this_1 :
  ∀ (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)
f' : SimpleFunc (β × γ) ℝ≥0∞
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b))
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))
⊢ Measurable.{u_2, 0} (α := β) (β := ℝ≥0∞)
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))

Tactic:
fun_prop
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
⊢ ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
have h_some_meas_integral :
    ∀ f' : SimpleFunc (β × γ) ℝ≥0∞, Measurable fun b => ∫⁻ c, f' (b, c) ∂η (a, b) := by
    intro f'
    have :
      (fun b => ∫⁻ c, f' (b, c) ∂η (a, b)) =
        (fun ab => ∫⁻ c, f' (ab.2, c) ∂η ab) ∘ fun b => (a, b) := by
      ext1 ab; rfl
    rw [this]
    fun_prop
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
rw :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
    (⨆ (n : ℕ),
      ∫⁻ (a_1 : β),
        ∫⁻ (c : γ),
          (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a)
hf₁ :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_mono₁ :
  Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (b : β) ↦
    ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ⨆ (n : ℕ),
        ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [lintegral_iSup]

Premises used: MeasureTheory.lintegral_iSup
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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 : ℕ),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
fun n => h_some_meas_integral (F n)
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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 : ℕ),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
exact fun n => h_some_meas_integral (F n)
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
⊢ Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (b : β) ↦
    ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
fun i j hij b => lintegral_mono fun c => h_mono hij _

Premises used: Monotone, Prod.mk, MeasureTheory.lintegral_mono
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
⊢ Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (b : β) ↦
    ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
exact fun i j hij b => lintegral_mono fun c => h_mono hij _

Premises used: MeasureTheory.lintegral_mono
-- 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 (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f 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)
e_s :
  Eq (α := ℕ → ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (n : ℕ) ↦
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
    (⨆ (n : ℕ),
      ∫⁻ (a_1 : β),
        ∫⁻ (c : γ),
          (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a)

Tactic:
congr