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 : β) (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 :
  ∀ (n : ℕ),
    ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
      ∫⁻ (a_1 : β),
        ∫⁻ (c : γ),
          (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
⊢ 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

Tactic:
ext1 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 : ℕ
⊢ ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a

Tactic:
SimpleFunc.induction ?_ ?_ (F n)

Premises used: MeasureTheory.SimpleFunc.induction
-- 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 : ℕ
e_s :
  ∀ (c : ℝ≥0∞) {s : Set (β × γ)} (hs : MeasurableSet s),
    ∫⁻ (a : β × γ),
        (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0) : (a : β × γ) → ℝ≥0∞)
          a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
      ∫⁻ (a_1 : β),
        ∫⁻ (c_1 : γ),
          (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0) : (a : β × γ) → ℝ≥0∞)
            (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
e_s₁ :
  ∀ ⦃f g : SimpleFunc (β × γ) ℝ≥0∞⦄,
    Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
        (Function.support (M := ℝ≥0∞) (⇑g : (a : β × γ) → ℝ≥0∞)) →
      ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
          ∫⁻ (a_2 : β),
            ∫⁻ (c : γ),
              (f : (a : β × γ) → ℝ≥0∞) (a_2, c) ∂(η : (a : α × β) → Measure γ) (a, a_2) ∂(κ : (a : α) → Measure β) a →
        ∫⁻ (a : β × γ), (g : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
            ∫⁻ (a_3 : β),
              ∫⁻ (c : γ),
                (g : (a : β × γ) → ℝ≥0∞) (a_3, c) ∂(η : (a : α × β) → Measure γ) (a, a_3) ∂(κ : (a : α) → Measure β) a →
          ∫⁻ (a : β × γ), (f + g : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
            ∫⁻ (a_4 : β),
              ∫⁻ (c : γ),
                (f + g : (a : β × γ) → ℝ≥0∞)
                  (a_4, c) ∂(η : (a : α × β) → Measure γ) (a, a_4) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a

Tactic:
refine SimpleFunc.induction ?_ ?_ (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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
hs : MeasurableSet s
e_s :
  HMul.hMul (β := ℝ≥0∞) c
      ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞) =
    ∫⁻ (a_1 : β),
      ∫⁻ (c_1 : γ),
        s.indicator (fun (x : β × γ) ↦ c)
          (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (a : β × γ),
      (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0) : (a : β × γ) → ℝ≥0∞)
        a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c_1 : γ),
        (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0) : (a : β × γ) → ℝ≥0∞)
          (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a

Tactic:
simp +unfoldPartialApp only [SimpleFunc.const_zero,
      SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
      Set.piecewise_eq_indicator, Function.const, lintegral_indicator_const hs]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, MeasureTheory.lintegral_indicator_const, Function.const, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const
-- 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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
hs : MeasurableSet s
e_s :
  ∫⁻ (a_1 : β),
      HMul.hMul (β := ℝ≥0∞) c
        ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s) :
          ℝ≥0∞) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c_1 : γ),
        s.indicator (fun (x : β × γ) ↦ c)
          (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
rw :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ HMul.hMul (β := ℝ≥0∞) c
      ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞) =
    ∫⁻ (a_1 : β),
      ∫⁻ (c_1 : γ),
        s.indicator (fun (x : β × γ) ↦ c)
          (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [compProd_apply hs, ← lintegral_const_mul c _]

Premises used: ProbabilityTheory.Kernel.compProd_apply, MeasureTheory.lintegral_const_mul
-- 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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
(measurable_kernel_prodMk_left ((measurable_fst.snd.prodMk measurable_snd) hs)).comp
        measurable_prodMk_left

Premises used: Measurable.comp, Set.Mem, setOf, Measurable.prodMk, Set.preimage, measurable_snd, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, measurable_fst, measurable_prodMk_left, Measurable.snd
-- 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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
exact (measurable_kernel_prodMk_left ((measurable_fst.snd.prodMk measurable_snd) hs)).comp
        measurable_prodMk_left

Premises used: Measurable.comp, Measurable.prodMk, measurable_snd, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, measurable_fst, measurable_prodMk_left, Measurable.snd
-- 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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
hs : MeasurableSet s
e_s :
  Eq.{u_2 + 1} (α := β → ℝ≥0∞)
    (fun (a_1 : β) ↦
      HMul.hMul (β := ℝ≥0∞) c
        ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s) : ℝ≥0∞))
    fun (a_1 : β) ↦ ∫⁻ (c_1 : γ), s.indicator (fun (x : β × γ) ↦ c) (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1)
⊢ ∫⁻ (a_1 : β),
      HMul.hMul (β := ℝ≥0∞) c
        ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s) :
          ℝ≥0∞) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c_1 : γ),
        s.indicator (fun (x : β × γ) ↦ c)
          (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a

Tactic:
congr
-- 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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
hs : MeasurableSet s
e_s :
  ∀ (b : β),
    HMul.hMul (β := ℝ≥0∞) c
        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) =
      ∫⁻ (c_1 : γ), s.indicator (fun (x : β × γ) ↦ c) (b, c_1) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ Eq.{u_2 + 1} (α := β → ℝ≥0∞)
    (fun (a_1 : β) ↦
      HMul.hMul (β := ℝ≥0∞) c
        ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s) : ℝ≥0∞))
    fun (a_1 : β) ↦ ∫⁻ (c_1 : γ), s.indicator (fun (x : β × γ) ↦ c) (a_1, c_1) ∂(η : (a : α × β) → Measure γ) (a, a_1)

Tactic:
ext1 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 : β → γ → ℝ≥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 : ℕ
c : ℝ≥0∞
s : Set (β × γ)
hs : MeasurableSet s
b : β
e_s e_s₁ :
  HMul.hMul (β := ℝ≥0∞) c
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) =
    ∫⁻ (c_1 : γ), s.indicator (fun (x : β × γ) ↦ c) (b, c_1) ∂(η : (a : α × β) → Measure γ) (a, b)

Tactic:
rw [lintegral_indicator_const_comp measurable_prodMk_left hs]

Premises used: MeasureTheory.lintegral_indicator_const_comp, 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∞
e_s :
  Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
      (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞)) →
    ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
        ∫⁻ (a_2 : β),
          ∫⁻ (c : γ),
            (f : (a : β × γ) → ℝ≥0∞) (a_2, c) ∂(η : (a : α × β) → Measure γ) (a, a_2) ∂(κ : (a : α) → Measure β) a →
      ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
          ∫⁻ (a_3 : β),
            ∫⁻ (c : γ),
              (f' : (a : β × γ) → ℝ≥0∞) (a_3, c) ∂(η : (a : α × β) → Measure γ) (a, a_3) ∂(κ : (a : α) → Measure β) a →
        ∫⁻ (a : β × γ), (f + f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
          ∫⁻ (a_4 : β),
            ∫⁻ (c : γ),
              (f + f' : (a : β × γ) → ℝ≥0∞)
                (a_4, c) ∂(η : (a : α × β) → Measure γ) (a, a_4) ∂(κ : (a : α) → Measure β) a
⊢ Disjoint (α := Set (β × γ)) (Function.support (M := ℝ≥0∞) (⇑f : (a : β × γ) → ℝ≥0∞))
      (Function.support (M := ℝ≥0∞) (⇑f' : (a : β × γ) → ℝ≥0∞)) →
    ∫⁻ (a : β × γ), (f : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
        ∫⁻ (a_2 : β),
          ∫⁻ (c : γ),
            (f : (a : β × γ) → ℝ≥0∞) (a_2, c) ∂(η : (a : α × β) → Measure γ) (a, a_2) ∂(κ : (a : α) → Measure β) a →
      ∫⁻ (a : β × γ), (f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
          ∫⁻ (a_3 : β),
            ∫⁻ (c : γ),
              (f' : (a : β × γ) → ℝ≥0∞) (a_3, c) ∂(η : (a : α × β) → Measure γ) (a, a_3) ∂(κ : (a : α) → Measure β) a →
        ∫⁻ (a : β × γ), (f + f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
          ∫⁻ (a_4 : β),
            ∫⁻ (c : γ),
              (f + f' : (a : β × γ) → ℝ≥0∞)
                (a_4, c) ∂(η : (a : α × β) → Measure γ) (a, a_4) ∂(κ : (a : α) → Measure β) a

Tactic:
_
-- 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 : β × γ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) a : ℝ≥0∞)
        ((f' : (a : β × γ) → ℝ≥0∞) a : ℝ≥0∞) ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : β × γ) → ℝ≥0∞) (a_1, c) : ℝ≥0∞)
          ((f' : (a : β × γ) → ℝ≥0∞) (a_1, c) :
            ℝ≥0∞) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (a : β × γ), (f + f' : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (f + f' : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [SimpleFunc.coe_add, Pi.add_apply]

Premises used: MeasureTheory.SimpleFunc.coe_add, Pi.add_apply