awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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)
⊢ 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
have 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
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
have 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
Tactic: refine SimpleFunc.induction ?_ ?_ (F n)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: refine SimpleFunc.induction ?_ ?_ (F n)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ 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
have 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
Tactic: rw [compProd_apply hs, ← lintegral_const_mul c _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ 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
have rw : Measurable (β := ℝ≥0∞) fun (b : β) ↦
  (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [compProd_apply hs, ← lintegral_const_mul c _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ 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)
have 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)
Tactic: ext1 b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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 : β
⊢ 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)
have 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∞)
Tactic: rw [lintegral_indicator_const_comp measurable_prodMk_left hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: simp_rw [SimpleFunc.coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: rw [lintegral_add_left (SimpleFunc.measurable _), hf_eq, hf'_eq, ← lintegral_add_left]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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
have e_s₁ : Measurable (β := ℝ≥0∞) fun (a_1 : β) ↦
  ∫⁻ (c : γ), (f : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1)
Tactic: rw [lintegral_add_left (SimpleFunc.measurable _), hf_eq, hf'_eq, ← lintegral_add_left]