awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₂ :
  Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' 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₃ : Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
  (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s
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
⊢ ∫⁻ (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 β) ω
have h : ∀ (b : β),
  (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, b) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
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 : β
⊢ (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, b) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
have h : ∫⁻ (b_1 : δ),
    (((prodMkRight β η : (a : ε × β) → Measure β') (f ω, b) : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
  ∫⁻ (c : δ),
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
Tactic: rw [prod_apply' _ _ _ hs, prodMkRight_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 : δ),
      (((prodMkRight β η : (a : ε × β) → Measure β') (f ω, b) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
⊢ (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, b) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
have h₁ : ∫⁻ (b_1 : δ),
    (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
  ∫⁻ (c : δ),
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
Tactic: rw [prod_apply' _ _ _ hs, prodMkRight_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 : δ),
      (((prodMkRight β η : (a : ε × β) → Measure β') (f ω, b) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
h₁ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
⊢ (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, b) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
have h₂ : ∫⁻ (b_1 : δ),
    (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
  ∫⁻ (c : δ),
    (((η.comap f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
Tactic: rw [prod_apply' _ _ _ hs, prodMkRight_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 : δ),
      (((prodMkRight β η : (a : ε × β) → Measure β') (f ω, b) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
h₁ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
h₂ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η.comap f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
⊢ (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, b) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
have h₃ : ∫⁻ (b_1 : δ),
    (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
  ∫⁻ (c : δ),
    (((η : (a : ε) → Measure β') (f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
      (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
Tactic: rw [prod_apply' _ _ _ hs, prodMkRight_apply, comp_deterministic_eq_comap, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
have pos : ∀ (hκ : IsSFiniteKernel κ),
  μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    μ ⊗ₘ κ =
      bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
have neg : ∀ (hκ : ¬IsSFiniteKernel κ),
  μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
have pos : Eq (α := Measure (α × β)) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
  (bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β)))
Tactic: rw [compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
hκ : IsSFiniteKernel κ
pos :
  Eq (α := Measure (α × β)) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β)))
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
have pos₁ : Eq (α := Measure (α × β)) ((⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) : (a : α) → Measure (α × β)) ∘ₘ μ)
  (bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β)))
Tactic: rw [compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
hκ : IsSFiniteKernel κ
pos :
  Eq (α := Measure (α × β)) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β)))
pos₁ :
  Eq (α := Measure (α × β)) ((⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β)))
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
have pos₂ : Eq (α := Measure (α × β)) ((⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) : (a : α) → Measure (α × β)) ∘ₘ μ)
  ((⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) : (a : α) → Measure (α × β)) ∘ₘ μ)
Tactic: rw [compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
⊢ Eq (α := Measure (α × γ)) (μ.prod ((⇑κ : (a : β) → Measure γ) ∘ₘ ν))
    ((⇑(Kernel.id ∥ₖ κ) : (a : α × β) → Measure (α × γ)) ∘ₘ μ.prod ν)
have h : ∀ (s : Set (α × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.prod ((⇑κ : (a : β) → Measure γ) ∘ₘ ν) : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((⇑(Kernel.id ∥ₖ κ) : (a : α × β) → Measure (α × γ)) ∘ₘ μ.prod ν : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.prod ((⇑κ : (a : β) → Measure γ) ∘ₘ ν) : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((⇑(Kernel.id ∥ₖ κ) : (a : α × β) → Measure (α × γ)) ∘ₘ μ.prod ν : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (x : α), (((⇑κ : (a : β) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ =
  ∫⁻ (a : α × β),
    (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν
Tactic: rw [Measure.prod_apply hs, Measure.bind_apply hs (Kernel.aemeasurable _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (((⇑κ : (a : β) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ =
    ∫⁻ (a : α × β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν
have h : ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
  ∫⁻ (a : α × β),
    (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν
Tactic: simp_rw [Measure.bind_apply (measurable_prodMk_left hs) (Kernel.aemeasurable _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (a : α × β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν
have h : ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
  ∫⁻ (x : α),
    ∫⁻ (y : β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (x, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν ∂μ
Tactic: rw [MeasureTheory.lintegral_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
h :
  ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (x : α),
      ∫⁻ (y : β),
        (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (x, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν ∂μ
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (a : α × β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν
have h₁ : AEMeasurable (β := ℝ≥0∞)
  (fun (a : α × β) ↦
    (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s)
  (μ.prod ν)
Tactic: rw [MeasureTheory.lintegral_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (x : α),
      ∫⁻ (y : β),
        (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (x, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν ∂μ
have h : ∀ (a : α),
  ∫⁻ (a_1 : β), (((κ : (a : β) → Measure γ) a_1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν =
    ∫⁻ (y : β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (a_1 : β), (((κ : (a : β) → Measure γ) a_1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν =
    ∫⁻ (y : β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν
have h : ∀ (b : β),
  Eq (α := ℝ≥0∞) ((((κ : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
    ((((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, b) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: congr with b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
    ((((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, b) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : Measurable (β := ℝ≥0∞) fun (x : α) ↦
  (((κ : (a : β) → Measure γ) (a, b).2 : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: rw [Kernel.parallelComp_apply, Kernel.id_apply, Measure.prod_apply hs, lintegral_dirac']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
have rw : Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
  (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
Tactic: rw [Measure.prod_swap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
have h1 : Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
  (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
Tactic: have h1 : (κ ∘ₘ μ).prod ν = (ν.prod (κ ∘ₘ μ)).map Prod.swap := by rw [Measure.prod_swap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
have rw : Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
  ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
Tactic: rw [Measure.prod_swap]