-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
calc :
  Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓨 × 𝓨) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓨) (mα := m𝓨)
          (Measure.bind.{u_2, u_3} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑η : (a : 𝓧) → Measure 𝓨))
          (⇑(Kernel.copy 𝓨) : (a : 𝓨) → Measure (𝓨 × 𝓨)))
        (⇑(Kernel.id ∥ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨 × 𝓨) → Measure (𝓨 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
    (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × 𝓧) → Measure (𝓨 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
calc₁ :
  Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × 𝓧) → Measure (𝓨 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
calc₂ :
  Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
calc₃ :
  Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
    (Measure.bind (α := Ω × 𝓨) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace)
          ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ) (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
        (⇑(Kernel.id ∥ₖ η) : (a : Ω × 𝓧) → Measure (Ω × 𝓨)))
      (⇑(Kernel.swap Ω 𝓨) : (a : Ω × 𝓨) → Measure (𝓨 × Ω)))
⊢ Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓨 × 𝓨) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓨) (mα := m𝓨)
          (Measure.bind.{u_2, u_3} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑η : (a : 𝓧) → Measure 𝓨))
          (⇑(Kernel.copy 𝓨) : (a : 𝓨) → Measure (𝓨 × 𝓨)))
        (⇑(Kernel.id ∥ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨 × 𝓨) → Measure (𝓨 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
    (Measure.bind (α := Ω × 𝓨) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace)
          ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ) (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
        (⇑(Kernel.id ∥ₖ η) : (a : Ω × 𝓧) → Measure (Ω × 𝓨)))
      (⇑(Kernel.swap Ω 𝓨) : (a : Ω × 𝓨) → Measure (𝓨 × Ω)))

Tactic:
calc (Kernel.id ∥ₖ κ†μ) ∘ₘ (Kernel.id ∥ₖ η†(κ ∘ₘ μ)) ∘ₘ (Kernel.copy 𝓨) ∘ₘ η ∘ₘ κ ∘ₘ μ
  _ = (Kernel.id ∥ₖ κ†μ) ∘ₘ (η ∥ₖ Kernel.id) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
    rw [parallelProd_posterior_comp_copy_comp]
  _ = (η ∥ₖ Kernel.id) ∘ₘ (Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]
  _ = (η ∥ₖ Kernel.id) ∘ₘ (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [parallelProd_posterior_comp_copy_comp]
  _ = (Kernel.swap _ _) ∘ₘ (Kernel.id ∥ₖ η) ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    simp_rw [Measure.comp_assoc]
    conv_rhs => rw [← Kernel.comp_assoc]
    rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]

Premises used: MeasureTheory.Measure.bind, ProbabilityTheory.Kernel.id, ProbabilityTheory.posterior, ProbabilityTheory.Kernel.swap, ProbabilityTheory.Kernel.parallelComp, DFunLike.coe, ProbabilityTheory.Kernel.copy