awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
have rw : Eq (α := Measure (γ × β))
  (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ)) (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
  (bind (α := α × β) (mα := Prod.instMeasurableSpace)
    ((⇑(Kernel.deterministic Prod.swap sorry) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
Tactic: rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 γ) ∘ₘ μ)))
rw :
  Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.deterministic Prod.swap ⋯) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
⊢ Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
have rw₁ : Eq (α := Measure (γ × β))
  (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ)) (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
  (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ)) (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
Tactic: rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 (γ × β))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
have rw : Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
  (bind (α := β × γ) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
    (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
Tactic: rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
-- 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 γ) ∘ₘ μ)))
rw :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
⊢ Eq (α := Measure (γ × β))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
have rw₁ : Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
  ((⇑(Kernel.swap β γ ∘ₖ (Kernel.id ∥ₖ κ)) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
Tactic: rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
-- 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 γ) ∘ₘ μ)))
rw :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
rw₁ :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
    ((⇑(Kernel.swap β γ ∘ₖ (Kernel.id ∥ₖ κ)) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
⊢ Eq (α := Measure (γ × β))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
have rw₂ : Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
  ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
Tactic: rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
-- 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 (γ × β))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
have rw : Eq (α := Measure (γ × β))
  (bind (α := β × γ) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
    (⇑(Kernel.deterministic Prod.swap sorry) : (a : β × γ) → Measure (γ × β)))
  (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
Tactic: rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 γ) ∘ₘ μ)))
rw :
  Eq (α := Measure (γ × β))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.deterministic Prod.swap ⋯) : (a : β × γ) → Measure (γ × β)))
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
⊢ Eq (α := Measure (γ × β))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
have rw₁ : Eq (α := Measure (γ × β)) (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
  (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
Tactic: rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
have calc : Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
  (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ)) (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
Tactic: calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 γ) ∘ₘ μ)))
calc :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
have calc₁ : Eq (α := Measure (γ × β))
  (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ)) (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
  (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
Tactic: calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 γ) ∘ₘ μ)))
calc :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
calc₁ :
  Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
have calc₂ : Eq (α := Measure (γ × β))
  (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
  (bind (α := β × γ) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
    (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
Tactic: calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 γ) ∘ₘ μ)))
calc :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
calc₁ :
  Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
calc₂ :
  Eq (α := Measure (γ × β))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
have calc₃ : Eq (α := Measure (γ × β))
  (bind (α := β × γ) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
    (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
  (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
Tactic: calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
have h2 : Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
  (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
Tactic: have h2 : (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν) = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
    calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- 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 κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
h2 :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
have h2₁ : Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
  (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
Tactic: rw [← Measure.prod_comp_right, ← h1] at h2
Cleared hypotheses: h2
-- 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 α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
have pos : ∀ (hμ : SFinite μ), (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
Tactic: by_cases hμ : SFinite μ
-- 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 α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
pos : ∀ (hμ : SFinite μ), (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
have neg : ∀ (hμ : ¬SFinite μ), (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
Tactic: by_cases hμ : SFinite μ
-- 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 α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
have pos : bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) =
  μ ⊗ₘ (η ∘ₖ κ)
Tactic: rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
    Kernel.parallelComp_comp_prod, Kernel.id_comp]
-- 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 α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) =
    μ ⊗ₘ (η ∘ₖ κ)
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
have pos₁ : Eq (α := Measure (α × γ))
  (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)))
  ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
    Kernel.parallelComp_comp_prod, Kernel.id_comp]
-- 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 α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) =
    μ ⊗ₘ (η ∘ₖ κ)
pos₁ :
  Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
have pos₂ : Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ η ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
  ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
    Kernel.parallelComp_comp_prod, Kernel.id_comp]