-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
rw :
  Eq (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)) : (a : 𝓧 × 𝓧) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
rw₁ :
  Eq (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ)) :
        (a : 𝓧 × 𝓧) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
⊢ ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ
      (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧))

Tactic:
rw [Measure.compProd_eq_parallelComp_comp_copy_comp,
      ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]

Premises used: MeasureTheory.Measure.comp_assoc, MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp, ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp