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 (α × β) γ
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 α
rw₁ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        Kernel.sum fun (n : ℕ) ↦ 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.id ∥ₖ Kernel.sum κ.seq) ∘ₖ
    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 α
rw₁ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        Kernel.sum fun (n : ℕ) ↦ Kernel.id ∥ₖ κ.seq n) ∘ₖ
      copy α
rw₂ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ Kernel.sum κ.seq) ∘ₖ
      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.id ∥ₖ κ) ∘ₖ
    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 α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
⊢ κ ⊗ₖ η = 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 γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      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 α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ) ∘ₖ
        copy α
have rw : swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α =
  (Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ)) ∘ₖ
    copy α
Tactic: rw [← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_right,
    ← parallelComp_sum_left, 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 α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
rw :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
        swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ)) ∘ₖ
      copy α
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ) ∘ₖ
        copy α
have rw₁ : swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α =
  (Kernel.sum fun (n : ℕ) ↦
        swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
          (Kernel.id ∥ₖ copy β)) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α
Tactic: rw [← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_right,
    ← parallelComp_sum_left, 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 α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
rw :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
        swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ)) ∘ₖ
      copy α
rw₁ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
          swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β)) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ) ∘ₖ
        copy α
have rw₂ : swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α =
  (Kernel.sum fun (n : ℕ) ↦
          swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry) ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α
Tactic: rw [← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_right,
    ← parallelComp_sum_left, 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 α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
rw :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
        swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ)) ∘ₖ
      copy α
rw₁ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
          swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β)) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α
rw₂ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
            swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯) ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ) ∘ₖ
        copy α
have rw₃ : swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α =
  (Kernel.sum fun (n : ℕ) ↦ swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id)) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α
Tactic: rw [← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_right,
    ← parallelComp_sum_left, 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 (α × β) γ
inst_1 : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun (n : ℕ) ↦ Kernel.sum fun (m : ℕ) ↦ κ.seq n ⊗ₖ η.seq m
have simp_rw : κ ⊗ₖ η = Kernel.sum fun (n : ℕ) ↦ κ.seq n ⊗ₖ η
Tactic: simp_rw [← compProd_eq_sum_compProd_right, ← compProd_eq_sum_compProd_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 γ
s : Set (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ) (m : ℕ),
        (((κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((Kernel.sum fun (n : ℕ) ↦ Kernel.sum fun (m : ℕ) ↦ κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a :
          Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  (∑' (n : ℕ) (m : ℕ),
      (((κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s :
    ℝ≥0∞)
Tactic: rw [compProd_eq_sum_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 γ
s : Set (β × γ)
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
η : Kernel (α × β) γ
inst_1 : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ⊗ₖ η)
have rw : IsZeroOrMarkovKernel
  (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α)
Tactic: 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 α β
η : Kernel (α × β) γ
inst : IsFiniteKernel η
a : α
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
have pos : ∀ (hκ : IsSFiniteKernel κ),
  (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
Tactic: by_cases hκ : IsSFiniteKernel κ
-- 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 α β
η : Kernel (α × β) γ
inst : IsFiniteKernel η
a : α
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
      HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
have neg : ∀ (hκ : ¬IsSFiniteKernel κ),
  (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
Tactic: by_cases hκ : IsSFiniteKernel κ
-- 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 α β
η : Kernel (α × β) γ
inst : IsFiniteKernel η
a : α
hκ : ¬IsSFiniteKernel κ
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
have neg : (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
  HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
Tactic: rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]
-- 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 α β
η : Kernel (α × β) γ
inst : IsFiniteKernel η
a : α
hκ : IsSFiniteKernel κ
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
have pos : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) a ≤
  HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
Tactic: rw [compProd_apply .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 γ
s : Set (β × γ)
κ : Kernel α β
inst : IsFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsFiniteKernel η
⊢ IsFiniteKernel (κ ⊗ₖ η)
have rw : IsFiniteKernel
  (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α)
Tactic: 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 γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
⊢ IsSFiniteKernel (κ ⊗ₖ η)
have rw : IsSFiniteKernel
  (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
        (Kernel.id ∥ₖ copy β) ∘ₖ
      (Kernel.id ∥ₖ κ) ∘ₖ
    copy α)
Tactic: 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have pos : ∀ (hκ : IsSFiniteKernel κ),
  (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
Tactic: by_cases hκ : IsSFiniteKernel κ
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have neg : ∀ (hκ : ¬IsSFiniteKernel κ),
  (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
Tactic: by_cases hκ : IsSFiniteKernel κ
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have pos : ∀ (hη : IsSFiniteKernel η),
  (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
Tactic: by_cases hη : IsSFiniteKernel η