awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
inst : IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ κ
have rw : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ κ
Tactic: rw [parallelComp_id_left_comp_parallelComp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
inst : IsSFiniteKernel κ
⊢ η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ κ
have e_η : κ ∘ₖ Kernel.id = κ
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
⊢ ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) = ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf)
have h : ∀ (ω : γ) (s : Set (δ × β')) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext ω s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s ∂(κ : (a : γ) → Measure β) ω =
  ∫⁻ (b : β),
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) ∂(κ : (a : γ) → Measure β) ω
Tactic: rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_prod_deterministic,
    lintegral_comp, lintegral_prod_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) ∂(κ : (a : γ) → Measure β) ω
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
  ∫⁻ (c : δ),
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) b
Tactic: rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_prod_deterministic,
    lintegral_comp, lintegral_prod_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) ∂(κ : (a : γ) → Measure β) ω
h₁ :
  Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) b
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₂ : Measurable (β := ℝ≥0∞) fun (b : δ) ↦
  (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_prod_deterministic,
    lintegral_comp, lintegral_prod_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) ∂(κ : (a : γ) → Measure β) ω
h₁ :
  Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) b
h₂ :
  Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₃ : Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
  (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s
Tactic: rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_prod_deterministic,
    lintegral_comp, lintegral_prod_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) ∂(κ : (a : γ) → Measure β) ω
have h : ∀ (b : β),
  (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
Tactic: congr with b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
have h : ∫⁻ (b_1 : δ),
    (((prodMkLeft β η : (a : β × ε) → Measure β') (b, f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
  ∫⁻ (c : δ),
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
Tactic: rw [prod_apply' _ _ _ hs, prodMkLeft_apply, comp_deterministic_eq_comap, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
h :
  ∫⁻ (b_1 : δ),
      (((prodMkLeft β η : (a : β × ε) → Measure β') (b, f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
⊢ (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
have h₁ : ∫⁻ (b_1 : δ),
    (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
  ∫⁻ (c : δ),
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
Tactic: rw [prod_apply' _ _ _ hs, prodMkLeft_apply, comp_deterministic_eq_comap, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
h :
  ∫⁻ (b_1 : δ),
      (((prodMkLeft β η : (a : β × ε) → Measure β') (b, f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
h₁ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
⊢ (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
have h₂ : ∫⁻ (b_1 : δ),
    (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
  ∫⁻ (c : δ),
    (((η.comap f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
Tactic: rw [prod_apply' _ _ _ hs, prodMkLeft_apply, comp_deterministic_eq_comap, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
h :
  ∫⁻ (b_1 : δ),
      (((prodMkLeft β η : (a : β × ε) → Measure β') (b, f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
h₁ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
h₂ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η.comap f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
⊢ (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
have h₃ : ∫⁻ (b_1 : δ),
    (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
  ∫⁻ (c : δ),
    (((η : (a : ε) → Measure β') (f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
Tactic: rw [prod_apply' _ _ _ hs, prodMkLeft_apply, comp_deterministic_eq_comap, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
⊢ ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) = ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf)
have h : ∀ (ω : γ) (s : Set (δ × β')) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext ω s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (c : β),
    (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, c) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s ∂(κ : (a : γ) → Measure β) ω =
  ∫⁻ (c : β),
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, c) ∂(κ : (a : γ) → Measure β) ω
Tactic: rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_deterministic_prod,
    lintegral_comp, lintegral_deterministic_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∫⁻ (c : β),
      (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, c) : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (c : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, c) ∂(κ : (a : γ) → Measure β) ω
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
  ∫⁻ (c : δ),
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) b
Tactic: rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_deterministic_prod,
    lintegral_comp, lintegral_deterministic_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∫⁻ (c : β),
      (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, c) : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (c : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, c) ∂(κ : (a : γ) → Measure β) ω
h₁ :
  Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) b
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₂ : Measurable (β := ℝ≥0∞) fun (b : δ) ↦
  (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_deterministic_prod,
    lintegral_comp, lintegral_deterministic_prod]