-- 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 η
rw :
  Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ ∘ₖ (η ∥ₖ 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 (𝓨 × Ω)))
rw₁ :
  Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(η ∥ₖ Kernel.id ∘ₖ (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 (𝓨 × Ω)))
rw₂ rw₃ :
  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 (𝓨 × Ω)))
⊢ 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 (𝓨 × Ω)))

Tactic:
rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]

Premises used: ProbabilityTheory.Kernel.parallelComp_comm, MeasureTheory.Measure.comp_assoc