-- 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
calc :
  Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ
      (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
calc₁ :
  ((⇑(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 (𝓧 × 𝓧))
calc₂ :
  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) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
calc₃ :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
calc₄ :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
calc₅ :
  Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    (Measure.map f μ ⊗ₘ Kernel.id)
⊢ Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) = Measure.map f μ ⊗ₘ Kernel.id

Tactic:
calc μ.map f ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
  _ = (Kernel.deterministic f hf ∘ₘ μ)
      ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) := by
    rw [Measure.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ
      Kernel.copy 𝓧 ∘ₘ Kernel.deterministic f hf ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp,
      ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ
      Kernel.copy Ω ∘ₘ μ := by rw [parallelProd_posterior_comp_copy_comp]
  _ = (Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
  _ = (Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ := by -- `deterministic` is used here
    rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_copy]
  _ = μ.map f ⊗ₘ Kernel.id := by
    rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]

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