-- 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 α
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 α =
    (swap γ β ∘ₖ Kernel.sum fun (n : ℕ) ↦ η.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 α =
  swap γ β ∘ₖ (Kernel.sum η.seq ∥ₖ 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]