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_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_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
have 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)
Tactic: congr with 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_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 : β
⊢ ∫⁻ (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)
have e_s : Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (f : (a : β × γ) → ℝ≥0∞) (b, c)
Tactic: rw [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 : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have change : ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
  ∫⁻ (b : β), ∫⁻ (c : γ), g b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: change ∫⁻ bc, f bc ∂(κ ⊗ₖ η) a = ∫⁻ b, ∫⁻ c, g b c ∂η (a, b) ∂κ a
-- 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 f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
  ∫⁻ (bc : β × γ), g bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
Tactic: rw [← lintegral_compProd']
-- 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 f
g : β → γ → ℝ≥0∞ := Function.curry f
rw :
  ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (bc : β × γ), g bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have hf₁ : Measurable (Function.uncurry g)
Tactic: rw [← lintegral_compProd']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
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 =
    ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have 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
-- 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 : 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
have 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)
Tactic: apply lintegral_congr_ae
-- 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 : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
⊢ (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)
have 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
Tactic: filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha
-- 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 : 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
⊢ (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)
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (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: filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
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
⊢ ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have B : ∫⁻ (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
-- 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 : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
B :
  ∫⁻ (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
⊢ ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have hf₁ : Measurable (AEMeasurable.mk f hf)
Tactic: rw [A, B, lintegral_compProd]
-- 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 f
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have simp_rw : ∫⁻ (z : β × γ), f z ∂((κ ⊗ₖ η).restrict (s := s ×ˢ t) sorry : (a : α) → Measure (β × γ)) a =
  ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht,
    lintegral_compProd _ _ _ hf, Kernel.restrict_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 : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
simp_rw :
  ∫⁻ (z : β × γ), f z ∂((κ ⊗ₖ η).restrict (s := s ×ˢ t) ⋯ : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have simp_rw₁ : ∫⁻ (z : β × γ), f z ∂(κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a =
  ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht,
    lintegral_compProd _ _ _ hf, Kernel.restrict_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 : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
simp_rw :
  ∫⁻ (z : β × γ), f z ∂((κ ⊗ₖ η).restrict (s := s ×ˢ t) ⋯ : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
simp_rw₁ :
  ∫⁻ (z : β × γ), f z ∂(κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have simp_rw₂ : ∫⁻ (b : β),
    ∫⁻ (c : γ),
      f
        (b,
          c) ∂(η.restrict (s := t) ht : (a : α × β) → Measure γ)
        (a, b) ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a =
  ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht,
    lintegral_compProd _ _ _ hf, Kernel.restrict_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 : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (z : β × γ) in SProd.sprod (β := Set γ) s Set.univ, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have simp_rw : ∫⁻ (x : β) in s, ∫⁻ (y : γ) in Set.univ, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [setLIntegral_compProd κ η a hf hs MeasurableSet.univ, Measure.restrict_univ]
-- 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 f
t : Set γ
ht : MeasurableSet t
⊢ ∫⁻ (z : β × γ) in SProd.sprod (α := Set β) Set.univ t, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
have simp_rw : ∫⁻ (x : β) in Set.univ, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [setLIntegral_compProd κ η a hf MeasurableSet.univ ht, Measure.restrict_univ]
-- 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 (α × β) γ
⊢ κ ⊗ₖ η = Kernel.sum fun (n : ℕ) ↦ κ.seq n ⊗ₖ η
have simp_rw : swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α =
  Kernel.sum fun (n : ℕ) ↦
    swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ.seq n) ∘ₖ
      copy α
Tactic: simp_rw [compProd_def]
-- 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 (α × β) γ
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ.seq n) ∘ₖ
        copy α
have rw : swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α =
  (Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ.seq n)) ∘ₖ
    copy α
Tactic: rw [← comp_sum_left, ← comp_sum_right, ← parallelComp_sum_right, kernel_sum_seq]
-- 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 (α × β) γ
rw :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
        swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ.seq n)) ∘ₖ
      copy α
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ.seq n) ∘ₖ
        copy α
have rw₁ : swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α =
  (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      Kernel.sum fun (n : ℕ) ↦ Kernel.id ∥ₖ κ.seq n) ∘ₖ
    copy α
Tactic: rw [← comp_sum_left, ← comp_sum_right, ← parallelComp_sum_right, kernel_sum_seq]