chore: fix the lemma name condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (#30545)

There is a `prodMkRight` in the statement, not a `prodMkLeft`.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/Probability/Independence/Conditional.lean

@@ -863,7 +863,7 @@ theorem condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
 /-- Two random variables `f, g` are conditionally independent given a third `k` iff the
 conditional distribution of `f` given `k` and `g` is equal to the conditional distribution of `f`
 given `k`. -/
-theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
+theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight
     {γ : Type*} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β']
     (hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) :
@@ -907,6 +907,9 @@ theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
   rw [h1, h2]
   exact ⟨fun h ↦ by rw [h], fun h ↦ by rw [h1_symm, h1, h2_symm, h2, h]⟩
 
+@[deprecated (since := "2025-10-14")] alias condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft :=
+  condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight
+
 section iCondIndepFun
 variable {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}