diff --git a/LeanBandits.lean b/LeanBandits.lean
index 457152e6..2e400a2f 100644
--- a/LeanBandits.lean
+++ b/LeanBandits.lean
@@ -5,8 +5,6 @@ import LeanBandits.Bandit
 import LeanBandits.ETC
 import LeanBandits.ForMathlib.CondDistrib
 import LeanBandits.ForMathlib.IdentDistrib
-import LeanBandits.ForMathlib.KernelCompositionLemmas
-import LeanBandits.ForMathlib.KernelCompositionParallelComp
 import LeanBandits.ForMathlib.KernelSub
 import LeanBandits.ForMathlib.Measurable
 import LeanBandits.ForMathlib.SubGaussian
diff --git a/LeanBandits/Algorithm.lean b/LeanBandits/Algorithm.lean
index cc7a9ce1..b2005563 100644
--- a/LeanBandits/Algorithm.lean
+++ b/LeanBandits/Algorithm.lean
@@ -5,7 +5,6 @@ Authors: Rémy Degenne, Paulo Rauber
 -/
 import Mathlib
 import LeanBandits.ForMathlib.CondDistrib
-import LeanBandits.ForMathlib.KernelCompositionLemmas
 import LeanBandits.ForMathlib.Measurable
 import LeanBandits.ForMathlib.Traj
 
@@ -132,6 +131,54 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R]
     Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) :=
   MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R)
 
+lemma step_eq_eval_comp_hist (n : ℕ) :
+    step (α := α) (R := R) n = (fun x ↦ x ⟨n, by simp⟩) ∘ (hist n) := rfl
+
+lemma action_eq_eval_comp_hist (n : ℕ) :
+    action (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist n) := rfl
+
+lemma reward_eq_eval_comp_hist (n : ℕ) :
+    reward (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist n) := rfl
+
+lemma measurable_step_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (step n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [step_eq_eval_comp_hist]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma adapted_step [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α]
+    [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R] :
+    Adapted (Learning.filtration α R) (fun n ↦ step (α := α) (R := R) n) :=
+  fun n ↦ (measurable_step_filtration n).stronglyMeasurable
+
+lemma measurable_hist_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (hist n) := by
+  simp [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe,
+    measurable_iff_comap_le]
+
+-- todo: due to the type of `Adapted` and the fact that `Iic n → α × R` depends on `n`, we cannot
+-- state that `hist` is adapted.
+
+lemma measurable_action_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (action n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [action_eq_eval_comp_hist]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α] :
+    Adapted (Learning.filtration α R) action :=
+  fun n ↦ (measurable_action_filtration n).stronglyMeasurable
+
+lemma measurable_reward_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (reward n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [reward_eq_eval_comp_hist]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R] :
+    Adapted (Learning.filtration α R) reward :=
+  fun n ↦ (measurable_reward_filtration n).stronglyMeasurable
+
 lemma condDistrib_step [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
     condDistrib (step (n + 1)) (hist n) (trajMeasure alg env)
@@ -143,7 +190,7 @@ lemma condDistrib_action [StandardBorelSpace α] [Nonempty α] [StandardBorelSpa
     condDistrib (action (n + 1)) (hist n) (trajMeasure alg env)
       =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := by
   rw [← fst_comp_step]
-  refine (condDistrib_comp' (by fun_prop) (by fun_prop) (by fun_prop)).trans ?_
+  refine (condDistrib_comp _ (by fun_prop) (by fun_prop)).trans ?_
   filter_upwards [condDistrib_step alg env n] with h h_eq
   rw [Kernel.map_apply _ (by fun_prop), h_eq, ← Kernel.map_apply _ (by fun_prop), ← Kernel.fst_eq,
     fst_stepKernel]
@@ -154,8 +201,8 @@ lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpa
       =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := by
   have h_step := condDistrib_step alg env n
   have h_action := condDistrib_action alg env n
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_step h_action ⊢
-  rw [h_action, Measure.compProd_assoc, ← stepKernel, ← h_step,
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_step h_action ⊢
+  rw [h_action, ← Measure.compProd_assoc, ← stepKernel, ← h_step,
     Measure.map_map (by fun_prop) (by fun_prop)]
   rfl
 
@@ -182,7 +229,7 @@ lemma condDistrib_reward_zero [StandardBorelSpace R] [Nonempty R]
       =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0 := by
   have h_step := (hasLaw_step_zero alg env).map_eq
   have h_action := (hasLaw_action_zero alg env).map_eq
-  rwa [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop), h_action]
+  rwa [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h_action]
 
 section DetAlgorithm
 
@@ -209,39 +256,6 @@ lemma action_zero_detAlgorithm [MeasurableSingletonClass α] : action 0 =ᵐ[
     simp [detAlgorithm]
   exact ae_of_ae_map (by fun_prop) h_eq
 
-lemma action_eq_eval_comp_hist (n : ℕ) :
-    action (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist n) := rfl
-
-lemma reward_eq_eval_comp_hist (n : ℕ) :
-    reward (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist n) := rfl
-
-lemma measurable_hist_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (hist n) := by
-  simp [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe,
-    measurable_iff_comap_le]
-
--- todo: due to the type of `Adapted` and the fact that `Iic n → α × R` depends on `n`, we cannot
--- state that `hist` is adapted.
-
-lemma measurable_action_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (action n) := by
-  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
-  rw [action_eq_eval_comp_hist]
-  exact measurable_comp_comap _ (by fun_prop)
-
-lemma adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
-    [SecondCountableTopology α] [OpensMeasurableSpace α] :
-    Adapted (Learning.filtration α R) action :=
-  fun n ↦ (measurable_action_filtration n).stronglyMeasurable
-
-lemma measurable_reward_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (reward n) := by
-  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
-  rw [reward_eq_eval_comp_hist]
-  exact measurable_comp_comap _ (by fun_prop)
-
-lemma adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
-    [SecondCountableTopology R] [OpensMeasurableSpace R] :
-    Adapted (Learning.filtration α R) reward :=
-  fun n ↦ (measurable_reward_filtration n).stronglyMeasurable
-
 lemma action_detAlgorithm_ae_eq
     [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (n : ℕ) :
@@ -275,13 +289,13 @@ lemma condDistrib_reward_stationaryEnv [StandardBorelSpace α] [Nonempty α]
     condDistrib (reward n) (action n) 𝔓 =ᵐ[(𝔓).map (action n)] ν := by
   cases n with
   | zero =>
-    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)]
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)]
     change (𝔓).map (step 0) = (𝔓).map (action 0) ⊗ₘ ν
     rw [(hasLaw_action_zero alg (stationaryEnv ν)).map_eq,
       (hasLaw_step_zero alg (stationaryEnv ν)).map_eq, stationaryEnv_ν0]
   | succ n =>
     have h_eq := condDistrib_reward alg (stationaryEnv ν) n
-    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_eq ⊢
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_eq ⊢
     have : (𝔓).map (action (n + 1)) = ((𝔓).map (fun x ↦ (hist n x, action (n + 1) x))).snd := by
       rw [Measure.snd_map_prodMk (by fun_prop)]
     simp only [stationaryEnv_feedback] at h_eq
diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean
index 1fadc7f8..0fe0c865 100644
--- a/LeanBandits/Bandit.lean
+++ b/LeanBandits/Bandit.lean
@@ -6,7 +6,6 @@ Authors: Rémy Degenne, Paulo Rauber
 import Mathlib
 import LeanBandits.Algorithm
 import LeanBandits.ForMathlib.CondDistrib
-import LeanBandits.ForMathlib.KernelCompositionLemmas
 import LeanBandits.ForMathlib.Traj
 
 /-!
@@ -196,6 +195,8 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R]
     Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) :=
   MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R)
 
+section Laws
+
 lemma hasLaw_step_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
     HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) :=
   Learning.hasLaw_step_zero alg (stationaryEnv ν)
@@ -236,32 +237,32 @@ lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α]
       (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) :=
   Learning.condIndepFun_reward_hist_action n
 
+end Laws
+
 section DetAlgorithm
 
 variable {nextArm : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextArm n)}
   {arm0 : α} {ν : Kernel α R} [IsMarkovKernel ν]
 
-lemma HasLaw_arm_zero_detAlgorithm :
-    HasLaw (arm 0) (Measure.dirac arm0)
-      (Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν) where
+local notation "𝔓t" => Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν
+
+lemma HasLaw_arm_zero_detAlgorithm : HasLaw (arm 0) (Measure.dirac arm0) 𝔓t where
   map_eq := (hasLaw_arm_zero _ _).map_eq
 
 lemma arm_zero_detAlgorithm [MeasurableSingletonClass α] :
-    arm 0 =ᵐ[Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν] fun _ ↦ arm0 := by
-  have h_eq : ∀ᵐ x ∂((Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν).map (arm 0)), x
-      = arm0 := by
+    arm 0 =ᵐ[𝔓t] fun _ ↦ arm0 := by
+  have h_eq : ∀ᵐ x ∂(((𝔓t).map (arm 0))), x = arm0 := by
     rw [(hasLaw_arm_zero _ _).map_eq]
     simp [detAlgorithm]
   exact ae_of_ae_map (by fun_prop) h_eq
 
 lemma arm_detAlgorithm_ae_eq (n : ℕ) :
-    arm (n + 1) =ᵐ[Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν]
-      fun h ↦ nextArm n (fun i ↦ h i) := by
+    arm (n + 1) =ᵐ[𝔓t] fun h ↦ nextArm n (fun i ↦ h i) := by
+  -- rhs equals nextArm n ∘ hist n
   sorry
 
 example [MeasurableSingletonClass α] :
-    ∀ᵐ h ∂(Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν),
-    arm 0 h = arm0 ∧ ∀ n, arm (n + 1) h = nextArm n (fun i ↦ h i) := by
+    ∀ᵐ h ∂(𝔓t), arm 0 h = arm0 ∧ ∀ n, arm (n + 1) h = nextArm n (fun i ↦ h i) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨arm_zero_detAlgorithm, arm_detAlgorithm_ae_eq⟩
 
diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean
index 91e525a6..7689d834 100644
--- a/LeanBandits/ForMathlib/CondDistrib.lean
+++ b/LeanBandits/ForMathlib/CondDistrib.lean
@@ -8,7 +8,6 @@ import Mathlib.Probability.Independence.Basic
 import Mathlib.Probability.Independence.Conditional
 import Mathlib.Probability.Kernel.CompProdEqIff
 import Mathlib.Probability.Kernel.Composition.Lemmas
-import LeanBandits.ForMathlib.KernelCompositionParallelComp
 import LeanBandits.ForMathlib.KernelSub
 
 open MeasureTheory ProbabilityTheory Finset
@@ -21,38 +20,6 @@ variable {α β γ δ Ω Ω' : Type*}
   [mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω'] [Nonempty Ω']
   {X : α → β} {Y : α → Ω} {Z : α → Ω'} {T : α → γ}
 
-lemma MeasurableSpace.comap_prodMk (X : α → β) (Y : α → γ) :
-    MeasurableSpace.comap (fun ω ↦ (X ω, Y ω)) inferInstance = mβ.comap X ⊔ mγ.comap Y := by
-  rw [← generateFrom_prod, MeasurableSpace.comap_generateFrom,
-    MeasurableSpace.comap_eq_generateFrom, MeasurableSpace.comap_eq_generateFrom,
-    MeasurableSpace.generateFrom_sup_generateFrom]
-  have : (Set.preimage fun ω ↦ (X ω, Y ω)) ''
-        Set.image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
-      = {x | ∃ a, MeasurableSet a ∧ ∃ b, MeasurableSet b ∧ X ⁻¹' a ∩ Y ⁻¹' b = x} := by
-    ext
-    simp [Set.mk_preimage_prod]
-  rw [this]
-  refine le_antisymm (MeasurableSpace.generateFrom_le ?_) (MeasurableSpace.generateFrom_le ?_)
-  · rintro _ ⟨a, ha, b, hb, rfl⟩
-    refine MeasurableSet.inter ?_ ?_
-    · exact MeasurableSpace.measurableSet_generateFrom <| .inl ⟨a, ha, rfl⟩
-    · exact MeasurableSpace.measurableSet_generateFrom <| .inr ⟨b, hb, rfl⟩
-  · refine fun t ht ↦ MeasurableSpace.measurableSet_generateFrom ?_
-    cases ht with
-    | inl h =>
-      obtain ⟨s, hs, rfl⟩ := h
-      exact ⟨s, hs, .univ, .univ, by simp⟩
-    | inr h =>
-      obtain ⟨t, ht, rfl⟩ := h
-      exact ⟨.univ, .univ, t, ht, by simp⟩
-
-lemma map_trim_comap {f : α → β} (hf : Measurable f) :
-    @Measure.map _ _ (mβ.comap f) _ f (μ.trim hf.comap_le) = μ.map f := by
-  ext s hs
-  rw [Measure.map_apply hf hs, Measure.map_apply _ hs, trim_measurableSet_eq]
-  · exact ⟨s, hs, rfl⟩
-  · exact Measurable.of_comap_le le_rfl
-
 lemma ae_map_iff_ae_trim {f : α → β} (hf : Measurable f) {p : β → Prop}
     (hp : MeasurableSet { x | p x }) :
     (∀ᵐ y ∂μ.map f, p y) ↔ ∀ᵐ x ∂(μ.trim hf.comap_le), p (f x) := by
@@ -76,156 +43,15 @@ lemma trim_eq_map {hm : m ≤ mα} : μ.trim hm = @Measure.map _ _ mα m id μ :
     simp only [Set.preimage_id_eq, id_eq]
     exact hm _ ht
 
-lemma comp_congr {κ η : Kernel α β} (h : ∀ᵐ a ∂μ, κ a = η a) :
-    κ ∘ₘ μ = η ∘ₘ μ :=
-  bind_congr_right h
-
-lemma copy_comp_map (hX : AEMeasurable X μ) :
-    Kernel.copy β ∘ₘ (μ.map X) = μ.map (fun a ↦ (X a, X a)) := by
-  rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX]
-  congr
-
-lemma compProd_deterministic [SFinite μ] (hX : Measurable X) :
-    μ ⊗ₘ Kernel.deterministic X hX = μ.map (fun a ↦ (a, X a)) := by
-  rw [compProd_eq_comp_prod, Kernel.id, Kernel.deterministic_prod_deterministic,
-    deterministic_comp_eq_map]
-  rfl
-
 lemma trim_comap_apply (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) :
     μ.trim hX.comap_le (X ⁻¹' s) = μ.map X s := by
   rw [trim_measurableSet_eq, Measure.map_apply (by fun_prop) hs]
   exact ⟨s, hs, rfl⟩
 
-lemma ext_prod {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {μ ν : Measure (α × β)} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (h : ∀ {s : Set α} {t : Set β} (_ : MeasurableSet s) (_ : MeasurableSet t),
-      μ (s ×ˢ t) = ν (s ×ˢ t)) :
-    μ = ν := by
-  ext s hs
-  have h_univ : μ .univ = ν .univ := by
-    rw [← Set.univ_prod_univ]
-    exact h .univ .univ
-  refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod (by simp)
-    ?_ ?_ ?_ s hs
-  · intro t ht
-    simp only [Set.mem_image2, Set.mem_setOf_eq] at ht
-    obtain ⟨s, hs, t, ht, rfl⟩ := ht
-    exact h hs ht
-  · intro t ht
-    simp_rw [measure_compl ht (measure_ne_top _ _)]
-    intro h
-    rw [h, h_univ]
-  · intro f h_disj hf h_eq
-    simp_rw [measure_iUnion h_disj hf, h_eq]
-
-lemma ext_prod_iff {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {μ ν : Measure (α × β)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    μ = ν ↔ ∀ {s : Set α} {t : Set β} (_ : MeasurableSet s) (_ : MeasurableSet t),
-      μ (s ×ˢ t) = ν (s ×ˢ t) :=
-  ⟨fun h s t hs ht ↦ by rw [h], Measure.ext_prod⟩
-
-lemma ext_prod₃ {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (h : ∀ {s : Set α} {t : Set β} {u : Set γ} (_ : MeasurableSet s) (_ : MeasurableSet t)
-      (_ : MeasurableSet u), μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) :
-    μ = ν := by
-  ext s hs
-  have h_univ : μ .univ = ν .univ := by
-    simp_rw [← Set.univ_prod_univ]
-    exact h .univ .univ .univ
-  let C₂ := Set.image2 (· ×ˢ ·) { t : Set β | MeasurableSet t } { u : Set γ | MeasurableSet u }
-  let C := Set.image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } C₂
-  refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
-  · refine (generateFrom_eq_prod (C := { s : Set α | MeasurableSet s }) (D := C₂) (by simp)
-      generateFrom_prod isCountablySpanning_measurableSet ?_).symm
-    exact isCountablySpanning_measurableSet.prod isCountablySpanning_measurableSet
-  · exact MeasurableSpace.isPiSystem_measurableSet.prod isPiSystem_prod
-  · intro t ht
-    simp only [Set.mem_image2, Set.mem_setOf_eq, exists_exists_and_exists_and_eq_and, C, C₂] at ht
-    obtain ⟨s, hs, t, ht, u, hu, rfl⟩ := ht
-    exact h hs ht hu
-  · intro t ht
-    simp_rw [measure_compl ht (measure_ne_top _ _)]
-    intro h
-    rw [h, h_univ]
-  · intro f h_disj hf h_eq
-    simp_rw [measure_iUnion h_disj hf, h_eq]
-
-lemma ext_prod₃_iff {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    μ = ν ↔ (∀ {s : Set α} {t : Set β} {u : Set γ},
-      MeasurableSet s → MeasurableSet t → MeasurableSet u →
-      μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) :=
-  ⟨fun h s t u hs ht hu ↦ by rw [h], Measure.ext_prod₃⟩
-
-lemma ext_prod₃_iff' {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {mγ : MeasurableSpace γ} {μ ν : Measure ((α × β) × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    μ = ν ↔ (∀ {s : Set α} {t : Set β} {u : Set γ},
-      MeasurableSet s → MeasurableSet t → MeasurableSet u →
-      μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)) := by
-  have : μ = ν ↔ μ.map MeasurableEquiv.prodAssoc = ν.map MeasurableEquiv.prodAssoc := by
-    refine ⟨fun h ↦ by rw [h], fun h ↦ ?_⟩
-    have h_map_map (μ : Measure ((α × β) × γ)) :
-        μ = (μ.map MeasurableEquiv.prodAssoc).map MeasurableEquiv.prodAssoc.symm := by
-      simp
-    rw [h_map_map μ, h_map_map ν, h]
-  rw [this, ext_prod₃_iff]
-  have h_eq (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ}
-      (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u) :
-      ν.map MeasurableEquiv.prodAssoc (s ×ˢ (t ×ˢ u)) = ν ((s ×ˢ t) ×ˢ u) := by
-    rw [map_apply (by fun_prop) (hs.prod (ht.prod hu))]
-    congr 1
-    ext x
-    simp [MeasurableEquiv.prodAssoc]
-  refine ⟨fun h s t u hs ht hu ↦ ?_, fun h s t u hs ht hu ↦ ?_⟩
-    <;> specialize h hs ht hu
-  · rwa [h_eq μ hs ht hu, h_eq ν hs ht hu] at h
-  · rwa [h_eq μ hs ht hu, h_eq ν hs ht hu]
-
-alias ⟨_, ext_prod₃'⟩ := ext_prod₃_iff'
-
 end MeasureTheory.Measure
 
 namespace ProbabilityTheory
 
-lemma Kernel.prod_apply_prod {κ : Kernel α β} {η : Kernel α γ}
-    [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set β} {t : Set γ} {a : α} :
-    (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by
-  rw [Kernel.prod_apply, Measure.prod_prod]
-
-lemma Kernel.compProd_assoc {κ : Kernel α β} {η : Kernel (α × β) γ} {ξ : Kernel (α × β × γ) δ}
-    [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel ξ] :
-    (κ ⊗ₖ η) ⊗ₖ ξ
-      = (κ ⊗ₖ (η ⊗ₖ (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)))).map
-        MeasurableEquiv.prodAssoc.symm := by
-  ext a s hs
-  rw [compProd_apply hs, map_apply' _ (by fun_prop) _ hs,
-    compProd_apply (hs.preimage (by fun_prop)), lintegral_compProd]
-  swap; · exact measurable_kernel_prodMk_left' hs a
-  congr with b
-  rw [compProd_apply]
-  swap; · exact hs.preimage (by fun_prop)
-  congr
-
-lemma _root_.MeasureTheory.Measure.compProd_assoc
-    {μ : Measure α} {κ : Kernel α β} {η : Kernel (α × β) γ}
-    [SFinite μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
-    (μ ⊗ₘ κ) ⊗ₘ η = (μ ⊗ₘ (κ ⊗ₖ η)).map MeasurableEquiv.prodAssoc.symm := by
-  ext s hs
-  rw [Measure.compProd_apply hs, Measure.map_apply (by fun_prop) hs,
-    Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.lintegral_compProd]
-  swap; · exact Kernel.measurable_kernel_prodMk_left hs
-  congr with a
-  rw [Kernel.compProd_apply]
-  swap; · exact hs.preimage (by fun_prop)
-  congr
-
-lemma _root_.MeasureTheory.Measure.compProd_assoc'
-    {μ : Measure α} {κ : Kernel α β} {η : Kernel (α × β) γ}
-    [SFinite μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
-    μ ⊗ₘ (κ ⊗ₖ η) = ((μ ⊗ₘ κ) ⊗ₘ η).map MeasurableEquiv.prodAssoc := by
-  simp [Measure.compProd_assoc]
-
 section IndepFun
 
 -- fix the lemma in mathlib to allow different types for the functions
@@ -235,91 +61,6 @@ theorem CondIndepFun.symm'
     CondIndepFun m hm g f μ :=
   Kernel.IndepFun.symm hfg
 
-lemma Kernel.indepFun_const_left {κ : Kernel α β} [IsZeroOrMarkovKernel κ] (c : δ) (X : β → γ) :
-    IndepFun (fun _ ↦ c) X κ μ := by
-  rw [IndepFun, MeasurableSpace.comap_const]
-  exact indep_bot_left _
-
-lemma Kernel.indepFun_const_right {κ : Kernel α β} [IsZeroOrMarkovKernel κ] (X : β → γ) (c : δ) :
-    IndepFun X (fun _ ↦ c) κ μ :=
-  (Kernel.indepFun_const_left c X).symm
-
-lemma condIndepFun_const_left [StandardBorelSpace α] {hm : m ≤ mα} [IsFiniteMeasure μ]
-    (c : γ) (X : α → β) :
-    CondIndepFun m hm (fun _ ↦ c) X μ :=
-  Kernel.indepFun_const_left c X
-
-lemma condIndepFun_const_right [StandardBorelSpace α] {hm : m ≤ mα}
-    [IsFiniteMeasure μ] (X : α → β) (c : γ) :
-    CondIndepFun m hm X (fun _ ↦ c) μ :=
-  Kernel.indepFun_const_right X c
-
-lemma condIndepFun_of_measurable_left [StandardBorelSpace α] {hm : m ≤ mα} [IsFiniteMeasure μ]
-    {X : α → β} {Y : α → γ} (hX : Measurable[m] X) (hY : Measurable Y) :
-    CondIndepFun m hm X Y μ := by
-  rw [condIndepFun_iff _ hm _ _ (hX.mono hm le_rfl) hY]
-  rintro _ _ ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
-  have h_ind_eq ω : (X ⁻¹' s ∩ Y ⁻¹' t).indicator (fun _ ↦ (1 : ℝ)) ω
-      = (X ⁻¹' s).indicator (fun _ ↦ (1 : ℝ)) ω * (Y ⁻¹' t).indicator (fun _ ↦ (1 : ℝ)) ω := by
-    simp only [Set.indicator, Set.mem_inter_iff, Set.mem_preimage, mul_ite, mul_one, mul_zero]
-    split_ifs with h1 h2 h3 h4 h5
-    · rfl
-    · exfalso
-      rw [Set.mem_inter_iff] at h1
-      refine h3 h1.1
-    · exfalso
-      rw [Set.mem_inter_iff] at h1
-      exact h2 h1.2
-    · exfalso
-      rw [Set.mem_inter_iff] at h1
-      exact h1 ⟨h5, h4⟩
-    · rfl
-    · rfl
-  calc μ[(X ⁻¹' s ∩ Y ⁻¹' t).indicator fun ω ↦ (1 : ℝ)|m]
-  _ = μ[fun ω ↦ (X ⁻¹' s).indicator (fun _ ↦ 1) ω * (Y ⁻¹' t).indicator (fun _ ↦ 1) ω|m] := by
-      simp_rw [← h_ind_eq]
-  _ =ᵐ[μ] fun ω ↦ (X ⁻¹' s).indicator (fun _ ↦ 1) ω * μ[(Y ⁻¹' t).indicator (fun _ ↦ 1)|m] ω := by
-    refine condExp_mul_of_stronglyMeasurable_left ?_ ?_ ?_
-    · exact (Measurable.indicator (by fun_prop) (hX hs)).stronglyMeasurable
-    · have : ((X ⁻¹' s).indicator fun x ↦ (1 : ℝ)) * (Y ⁻¹' t).indicator (fun x ↦ 1)
-          = (X ⁻¹' s ∩ Y ⁻¹' t).indicator (fun _ ↦ (1 : ℝ)) := by ext; simp [h_ind_eq]
-      rw [this]
-      rw [integrable_indicator_iff]
-      · exact (integrable_const (1 : ℝ)).integrableOn
-      · exact (hm _ (hX hs)).inter (hY ht)
-    · rw [integrable_indicator_iff]
-      · exact (integrable_const (1 : ℝ)).integrableOn
-      · exact hY ht
-  _ =ᵐ[μ] μ[(X ⁻¹' s).indicator fun ω ↦ 1|m] * μ[(Y ⁻¹' t).indicator fun ω ↦ 1|m] := by
-    nth_rw 2 [condExp_of_stronglyMeasurable hm]
-    · rfl
-    · exact (Measurable.indicator (by fun_prop) (hX hs)).stronglyMeasurable
-    · rw [integrable_indicator_iff]
-      · exact (integrable_const (1 : ℝ)).integrableOn
-      · exact hm _ (hX hs)
-
-lemma condIndepFun_of_measurable_right [StandardBorelSpace α] {hm : m ≤ mα} [IsFiniteMeasure μ]
-    {X : α → β} {Y : α → γ} (hX : Measurable X) (hY : Measurable[m] Y) :
-    CondIndepFun m hm X Y μ := by
-  refine CondIndepFun.symm' ?_
-  exact condIndepFun_of_measurable_left hY hX
-
-@[inherit_doc CondIndepFun]
-notation3 X " ⟂ᵢ[" Z ", " hZ "; " μ "] " Y =>
-  CondIndepFun (MeasurableSpace.comap Z inferInstance) (Measurable.comap_le hZ) X Y μ
-
-lemma condIndepFun_self_left [StandardBorelSpace α] [IsFiniteMeasure μ]
-    {X : α → β} {Z : α → δ} (hX : Measurable X) (hZ : Measurable Z) :
-    Z ⟂ᵢ[Z, hZ; μ] X := by -- CondIndepFun (mδ.comap Z) hZ.comap_le Z X μ := by
-  refine condIndepFun_of_measurable_left ?_ hX
-  rw [measurable_iff_comap_le]
-
-lemma condIndepFun_self_right [StandardBorelSpace α] [IsFiniteMeasure μ]
-    {X : α → β} {Z : α → δ} (hX : Measurable X) (hZ : Measurable Z) :
-    X ⟂ᵢ[Z, hZ; μ] Z := by -- CondIndepFun (mδ.comap Z) hZ.comap_le X Z μ := by
-  refine condIndepFun_of_measurable_right hX ?_
-  rw [measurable_iff_comap_le]
-
 lemma Kernel.IndepFun.of_prod_right {ε Ω : Type*} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
     {μ : Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ} {T : α → ε}
     (h : IndepFun X (fun ω ↦ (Y ω, T ω)) κ μ) :
@@ -351,9 +92,8 @@ lemma CondIndepFun.of_prod_left {ε : Type*} {mε : MeasurableSpace ε}
 lemma CondIndepFun.prod_right [StandardBorelSpace α] [IsFiniteMeasure μ]
     {X : α → β} {Y : α → γ} {Z : α → δ}
     (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
-    (h : X ⟂ᵢ[Z, hZ; μ] Y) :-- CondIndepFun (mδ.comap Z) hZ.comap_le X Y μ) :
+    (h : X ⟂ᵢ[Z, hZ; μ] Y) :
     X ⟂ᵢ[Z, hZ; μ] (fun ω ↦ (Y ω, Z ω)) := by
-    -- CondIndepFun (mδ.comap Z) hZ.comap_le X (fun ω ↦ (Y ω, Z ω)) μ := by
   sorry
 
 end IndepFun
@@ -362,108 +102,12 @@ section CondDistrib
 
 variable [IsFiniteMeasure μ]
 
-lemma condDistrib_comp_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
-    condDistrib Y X μ ∘ₘ (μ.map X) = μ.map Y := by
-  rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX]
-
-lemma condDistrib_congr {X' : α → β} {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') (hX : X =ᵐ[μ] X') :
-    condDistrib Y X μ = condDistrib Y' X' μ := by
-  rw [condDistrib, condDistrib]
-  congr 1
-  rw [Measure.map_congr]
-  filter_upwards [hX, hY] with a ha hb using by rw [ha, hb]
-
-lemma condDistrib_congr_right {X' : α → β} (hX : X =ᵐ[μ] X') :
-    condDistrib Y X μ = condDistrib Y X' μ :=
-  condDistrib_congr (by rfl) hX
-
-lemma condDistrib_congr_left {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') :
-    condDistrib Y X μ = condDistrib Y' X μ :=
-  condDistrib_congr hY (by rfl)
-
-lemma condDistrib_ae_eq_of_measure_eq_compProd₀
-    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (κ : Kernel β Ω) [IsFiniteKernel κ]
-    (hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) :
-    condDistrib Y X μ =ᵐ[μ.map X] κ := by
-  suffices ∀ᵐ x ∂μ.map (hX.mk X), κ x = condDistrib (hY.mk Y) (hX.mk X) μ x by
-    symm
-    rw [Measure.map_congr hX.ae_eq_mk]
-    convert this using 3 with b
-    rw [condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk, Filter.EventuallyEq]
-  refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) hX.measurable_mk hY.measurable_mk κ
-    ((Eq.trans ?_ hκ).trans ?_)
-  · refine Measure.map_congr ?_
-    filter_upwards [hX.ae_eq_mk, hY.ae_eq_mk] with a haX haY using by rw [haX, haY]
-  · rw [Measure.map_congr hX.ae_eq_mk]
-
-lemma condDistrib_ae_eq_iff_measure_eq_compProd₀
-    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (κ : Kernel β Ω) [IsFiniteKernel κ] :
-  (condDistrib Y X μ =ᵐ[μ.map X] κ) ↔ μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ := by
-  refine ⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd₀ hX hY κ⟩
-  rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY]
-
-lemma condDistrib_comp' (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
-    {f : Ω → Ω'} (hf : Measurable f) :
-    condDistrib (f ∘ Y) X μ =ᵐ[μ.map X] (condDistrib Y X μ).map f := by
-  refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_
-  calc μ.map (fun x ↦ (X x, (f ∘ Y) x))
-  _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by
-    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
-    rfl
-  _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by
-    rw [compProd_map_condDistrib hY]
-  _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by
-    rw [Measure.compProd_eq_comp_prod, ← Measure.deterministic_comp_eq_map (by fun_prop),
-      Measure.compProd_eq_comp_prod, Measure.comp_assoc]
-    congr
-    rw [← Kernel.deterministic_comp_eq_map hf, ← Kernel.parallelComp_comp_copy,
-      ← Kernel.parallelComp_comp_copy, ← Kernel.parallelComp_id_left_comp_parallelComp,
-      ← Kernel.deterministic_parallelComp_deterministic (by fun_prop), Kernel.comp_assoc,
-      ← Kernel.id]
-
-lemma condDistrib_comp (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) :
-    condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by
-  refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_
-  rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX]
-  rfl
-
-lemma condDistrib_const (hX : AEMeasurable X μ) (c : Ω) :
-    condDistrib (fun _ ↦ c) X μ =ᵐ[μ.map X] Kernel.deterministic (fun _ ↦ c) (by fun_prop) := by
-  have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl
-  conv_lhs => rw [this]
-  filter_upwards [condDistrib_comp hX (by fun_prop : Measurable (fun _ ↦ c))] with b hb
-  rw [hb]
-
-lemma condDistrib_fst_prod (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
-    (ν : Measure γ) [IsProbabilityMeasure ν] :
-    condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν) =ᵐ[μ.map X] condDistrib Y X μ := by
-  symm
-  refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) hX hY _ ?_
-  have hX_map : (μ.prod ν).map (fun ω ↦ X ω.1) = μ.map X := by
-    calc (μ.prod ν).map (fun ω ↦ X ω.1)
-    _ = ((μ.prod ν).map Prod.fst).map X := by
-      rw [AEMeasurable.map_map_of_aemeasurable ?_ (by fun_prop)]
-      · rfl
-      · rw [Measure.map_fst_prod]
-        exact hX.smul_measure _
-    _ = μ.map X := by simp [Measure.map_fst_prod]
-  rw [← hX_map, compProd_map_condDistrib]
-  · calc μ.map (fun x ↦ (X x, Y x))
-    _ = ((μ.prod ν).map Prod.fst).map (fun a ↦ (X a, Y a)) := by simp [Measure.map_fst_prod]
-    _ = (μ.prod ν).map (fun a ↦ (X a.1, Y a.1)) := by
-      rw [AEMeasurable.map_map_of_aemeasurable ?_ (by fun_prop)]
-      · rfl
-      · simp only [Measure.map_fst_prod, measure_univ, one_smul]
-        fun_prop
-  · fun_prop
-
 lemma condDistrib_prod_left [StandardBorelSpace β] [Nonempty β]
     (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hT : AEMeasurable T μ) :
     condDistrib (fun ω ↦ (X ω, Y ω)) T μ
       =ᵐ[μ.map T] condDistrib X T μ ⊗ₖ condDistrib Y (fun ω ↦ (T ω, X ω)) μ := by
-  refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) hT (by fun_prop)
-    (condDistrib X T μ ⊗ₖ condDistrib Y (fun ω ↦ (T ω, X ω)) μ) ?_
-  rw [Measure.compProd_assoc', compProd_map_condDistrib hX, compProd_map_condDistrib hY,
+  refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) T (by fun_prop) ?_
+  rw [← Measure.compProd_assoc', compProd_map_condDistrib hX, compProd_map_condDistrib hY,
     AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
   rfl
 
@@ -475,7 +119,7 @@ lemma fst_condDistrib_prod [StandardBorelSpace β] [Nonempty β]
 
 lemma condDistrib_of_indepFun (h : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
     condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by
-  refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) hX hY _ ?_
+  refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) X hY ?_
   simp only [Measure.compProd_const]
   exact (indepFun_iff_map_prod_eq_prod_map_map hX hY).mp h
 
@@ -486,273 +130,6 @@ lemma indepFun_iff_condDistrib_eq_const (hX : AEMeasurable X μ) (hY : AEMeasura
     Measure.compProd_congr h]
   simp
 
--- todo: use this to refactor `indepFun_iff_map_prod_eq_prod_map_map`
-theorem Kernel.indepFun_iff_map_prod_eq_prod_map_map {Ω' α β γ : Type*}
-    {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ}
-    {μ : Measure Ω'} [IsFiniteMeasure μ]
-    {κ : Kernel Ω' α} [IsFiniteKernel κ]
-    -- TODO: relax this to CountableOrCountablyGenerated once it is fixed
-    [StandardBorelSpace β] [StandardBorelSpace γ]
-    (hf : Measurable X) (hg : Measurable T) :
-    IndepFun X T κ μ ↔ κ.map (fun ω ↦ (X ω, T ω)) =ᵐ[μ] κ.map X ×ₖ κ.map T := by
-  classical
-  rw [indepFun_iff_measure_inter_preimage_eq_mul]
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · rw [← Kernel.compProd_eq_iff]
-    have : (μ ⊗ₘ κ.map fun ω ↦ (X ω, T ω)) = μ ⊗ₘ (κ.map X ×ₖ κ.map T)
-        ↔ ∀ {u : Set Ω'} {s : Set β} {t : Set γ},
-        MeasurableSet u → MeasurableSet s → MeasurableSet t →
-        (μ ⊗ₘ κ.map (fun ω ↦ (X ω, T ω))) (u ×ˢ s ×ˢ t)
-          = (μ ⊗ₘ (κ.map X ×ₖ κ.map T)) (u ×ˢ s ×ˢ t) := by
-      refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
-      exact Measure.ext_prod₃ h
-    rw [this]
-    intro u s t hu hs ht
-    rw [Measure.compProd_apply (hu.prod (hs.prod ht)),
-      Measure.compProd_apply (hu.prod (hs.prod ht))]
-    refine lintegral_congr_ae ?_
-    have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp
-    simp_rw [h_set_eq]
-    filter_upwards [h s t hs ht] with ω hω
-    by_cases hωu : ω ∈ u
-    swap; · simp [hωu]
-    simp only [hωu, ↓reduceIte]
-    rw [Kernel.map_apply _ (by fun_prop), Measure.map_apply (by fun_prop) (hs.prod ht)]
-    rw [Set.mk_preimage_prod, hω, Kernel.prod_apply_prod, Kernel.map_apply' _ (by fun_prop),
-        Kernel.map_apply' _ (by fun_prop)]
-    exacts [ht, hs]
-  · intro s t hs ht
-    filter_upwards [h] with ω hω
-    calc (κ ω) (X ⁻¹' s ∩ T ⁻¹' t)
-    _ = (κ.map (fun ω ↦ (X ω, T ω))) ω (s ×ˢ t) := by
-      rw [← Kernel.deterministic_comp_eq_map, ← deterministic_prod_deterministic hf hg,
-        Kernel.comp_apply, Measure.bind_apply (hs.prod ht) (by fun_prop)]
-      simp_rw [Kernel.prod_apply_prod, Kernel.deterministic_apply' hf _ hs,
-        Kernel.deterministic_apply' hg _ ht]
-      calc (κ ω) (X ⁻¹' s ∩ T ⁻¹' t)
-      _ = ∫⁻ a, (X ⁻¹' s ∩ T ⁻¹' t).indicator (fun x ↦ 1) a ∂κ ω := by
-        simp [lintegral_indicator ((hf hs).inter (hg ht))]
-      _ = ∫⁻ a, (X ⁻¹' s).indicator (fun x ↦ 1) a * (T ⁻¹' t).indicator (fun x ↦ 1) a ∂κ ω := by
-        congr with a
-        simp only [Set.indicator_apply, Set.mem_inter_iff, Set.mem_preimage, mul_ite, mul_one,
-          mul_zero]
-        by_cases has : X a ∈ s <;> simp [has]
-      _ = ∫⁻ a, s.indicator (fun x ↦ 1) (X a) * t.indicator (fun x ↦ 1) (T a) ∂κ ω := rfl
-    _ = ((κ.map X) ×ₖ (κ.map T)) ω (s ×ˢ t) := by rw [hω]
-    _ = (κ ω) (X ⁻¹' s) * (κ ω) (T ⁻¹' t) := by
-      rw [Kernel.prod_apply_prod, Kernel.map_apply' _ (by fun_prop),
-        Kernel.map_apply' _ (by fun_prop)]
-      exacts [ht, hs]
-
-lemma Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map {Ω' α β γ : Type*}
-    {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ}
-    {μ : Measure Ω'} [IsFiniteMeasure μ]
-    {κ : Kernel Ω' α} [IsFiniteKernel κ]
-    -- TODO: relax this to CountableOrCountablyGenerated once it is fixed
-    [StandardBorelSpace β] [StandardBorelSpace γ]
-    (hf : Measurable X) (hg : Measurable T) :
-    IndepFun X T κ μ ↔ (μ ⊗ₘ κ.map fun ω ↦ (X ω, T ω)) = μ ⊗ₘ (κ.map X ×ₖ κ.map T) := by
-  rw [Kernel.indepFun_iff_map_prod_eq_prod_map_map hf hg, Kernel.compProd_eq_iff]
-
-theorem condIndepFun_iff_map_prod_eq_prod_map_map {α : Type*} {m mα : MeasurableSpace α}
-    [StandardBorelSpace α] {X : α → β} {T : α → γ}
-    {hm : m ≤ mα} {μ : Measure α} [IsFiniteMeasure μ]
-    -- TODO: relax this to CountableOrCountablyGenerated once it is fixed
-    [StandardBorelSpace β] [StandardBorelSpace γ]
-    (hX : Measurable X) (hT : Measurable T) :
-    CondIndepFun m hm X T μ
-      ↔ (condExpKernel μ m).map (fun ω ↦ (X ω, T ω))
-        =ᵐ[μ.trim hm] (((condExpKernel μ m).map X) ×ₖ ((condExpKernel μ m).map T)) :=
-  Kernel.indepFun_iff_map_prod_eq_prod_map_map hX hT
-
-lemma condIndepFun_iff_map_prod_eq_prod_comp_trim
-    {α : Type*} {m mα : MeasurableSpace α} [StandardBorelSpace α] {X : α → β} {T : α → γ}
-    {hm : m ≤ mα} {μ : Measure α} [IsFiniteMeasure μ]
-    -- TODO: relax this to CountableOrCountablyGenerated once it is fixed
-    [StandardBorelSpace β] [StandardBorelSpace γ]
-    (hX : Measurable X) (hT : Measurable T) :
-    CondIndepFun m hm X T μ
-      ↔ @Measure.map _ _ _ (m.prod _) (fun ω ↦ (ω, X ω, T ω)) μ
-        = (Kernel.id ×ₖ ((condExpKernel μ m).map X ×ₖ (condExpKernel μ m).map T)) ∘ₘ μ.trim hm := by
-  unfold CondIndepFun
-  rw [Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hX hT]
-  congr!
-  · calc (μ.trim hm ⊗ₘ (condExpKernel μ m).map fun ω ↦ (X ω, T ω))
-    _ = (Kernel.id ∥ₖ Kernel.deterministic (fun ω ↦ (X ω, T ω)) (by fun_prop))
-        ∘ₘ (μ.trim hm ⊗ₘ (condExpKernel μ m)) := by
-      rw [Measure.compProd_eq_parallelComp_comp_copy_comp, ← Kernel.deterministic_comp_eq_map,
-        ← Kernel.parallelComp_id_left_comp_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
-        Kernel.parallelComp_comp_copy, ← Measure.comp_assoc, Measure.compProd_eq_comp_prod]
-    _ = (Kernel.id ∥ₖ Kernel.deterministic (fun ω ↦ (X ω, T ω)) (by fun_prop))
-        ∘ₘ (@Measure.map _ _ mα (m.prod mα) (fun ω ↦ (ω, ω)) μ) := by
-      congr
-      exact compProd_trim_condExpKernel hm
-    _ = _ := by
-      rw [← Measure.deterministic_comp_eq_map, Measure.comp_assoc,
-        ← Kernel.deterministic_prod_deterministic (g := fun ω ↦ ω),
-        Kernel.parallelComp_comp_prod, Kernel.deterministic_comp_deterministic, Kernel.id_comp,
-        Kernel.deterministic_prod_deterministic, Measure.deterministic_comp_eq_map]
-      · rfl
-      · exact Measurable.mono measurable_id le_rfl hm
-      · fun_prop
-  · rw [Measure.compProd_eq_comp_prod]
-
-lemma condDistrib_apply_ae_eq_condExpKernel_map
-    {α : Type*} {mα : MeasurableSpace α} [StandardBorelSpace α]
-    [StandardBorelSpace β] [Nonempty β]
-    {X : α → β} {T : α → γ} {μ : Measure α} [IsFiniteMeasure μ]
-    (hX : Measurable X) (hT : Measurable T) {s : Set β} (hs : MeasurableSet s) :
-    (fun a ↦ condDistrib X T μ (T a) s)
-      =ᵐ[μ] fun a ↦ (condExpKernel μ (MeasurableSpace.comap T inferInstance)).map X a s := by
-  have hT_meas {s : Set γ} (hs : MeasurableSet s) :
-      MeasurableSet[MeasurableSpace.comap T inferInstance] (T ⁻¹' s) := by
-    rw [MeasurableSpace.measurableSet_comap]
-    exact ⟨s, hs, rfl⟩
-  have h1 := condDistrib_ae_eq_condExp hT hX (μ := μ) hs
-  simp_rw [Kernel.map_apply _ hX, Measure.map_apply hX hs]
-  have h2 := condExpKernel_ae_eq_condExp hT.comap_le (μ := μ) (hX hs)
-  filter_upwards [h1, h2] with a ha₁ ha₂
-  rw [Measure.real] at ha₁ ha₂
-  rw [← ENNReal.toReal_eq_toReal (by simp) (by simp), ha₁, ha₂]
-
-omit [Nonempty Ω'] in
-theorem condIndepFun_comap_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
-    {α : Type*} {mα : MeasurableSpace α} [StandardBorelSpace α]
-    {X : α → β} {T : α → γ} {Z : α → Ω'} {μ : Measure α} [IsFiniteMeasure μ]
-    [StandardBorelSpace β] [StandardBorelSpace γ] [Nonempty β] [Nonempty γ]
-    (hX : Measurable X) (hT : Measurable T) (hZ : Measurable Z) :
-    (X ⟂ᵢ[Z, hZ; μ] T) -- CondIndepFun _ hZ.comap_le X T μ
-      ↔ μ.map (fun ω ↦ (Z ω, X ω, T ω))
-        = (Kernel.id ×ₖ (condDistrib X Z μ ×ₖ condDistrib T Z μ)) ∘ₘ μ.map Z := by
-  rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hX hT]
-  simp_rw [Measure.ext_prod₃_iff]
-  have hZ_meas {s : Set Ω'} (hs : MeasurableSet s) :
-      MeasurableSet[MeasurableSpace.comap Z inferInstance] (Z ⁻¹' s) := by
-    rw [MeasurableSpace.measurableSet_comap]
-    exact ⟨s, hs, rfl⟩
-  have h_left {s : Set Ω'} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
-      (hu : MeasurableSet u) :
-      (μ.map (fun ω ↦ (Z ω, X ω, T ω))) (s ×ˢ t ×ˢ u)
-        = (@Measure.map _ _ _ ((MeasurableSpace.comap Z inferInstance).prod inferInstance)
-          (fun ω ↦ (ω, X ω, T ω)) μ) ((Z ⁻¹' s) ×ˢ t ×ˢ u) := by
-    rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)),
-      Measure.map_apply _ ((hZ_meas hs).prod (ht.prod hu))]
-    · simp [Set.mk_preimage_prod]
-    · refine Measurable.prodMk ?_ (by fun_prop)
-      exact Measurable.mono measurable_id le_rfl hZ.comap_le
-  have h_right {s : Set Ω'} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
-      (hu : MeasurableSet u) :
-      ((Kernel.id ×ₖ (condDistrib X Z μ ×ₖ condDistrib T Z μ)) ∘ₘ μ.map Z) (s ×ˢ t ×ˢ u)
-      = ((Kernel.id ×ₖ
-        ((condExpKernel μ (MeasurableSpace.comap Z inferInstance)).map X ×ₖ
-          (condExpKernel μ (MeasurableSpace.comap Z inferInstance)).map T)) ∘ₘ
-        μ.trim hZ.comap_le) ((Z ⁻¹' s) ×ˢ t ×ˢ u) := by
-    rw [Measure.bind_apply ((hZ_meas hs).prod (ht.prod hu)) (by fun_prop),
-      Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop), lintegral_map ?_ (by fun_prop),
-      lintegral_trim]
-    rotate_left
-    · exact Kernel.measurable_coe _ ((hZ_meas hs).prod (ht.prod hu))
-    · exact Kernel.measurable_coe _ (hs.prod (ht.prod hu))
-    refine lintegral_congr_ae ?_
-    filter_upwards [condDistrib_apply_ae_eq_condExpKernel_map hX hZ ht,
-      condDistrib_apply_ae_eq_condExpKernel_map hT hZ hu] with a haX haT
-    simp_rw [Kernel.prod_apply_prod]
-    simp only [Kernel.id_apply, Measure.dirac_apply]
-    rw [@Measure.dirac_apply' _ (MeasurableSpace.comap Z inferInstance) _ _ (hZ_meas hs)]
-    congr
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · intro s t u hs ht hu
-    specialize h (s := Z ⁻¹' s) (hZ_meas hs) ht hu
-    convert h
-    · exact h_left hs ht hu
-    · exact h_right hs ht hu
-  · rintro _ t u ⟨s, hs, rfl⟩ ht hu
-    specialize h hs ht hu
-    convert h
-    · exact (h_left hs ht hu).symm
-    · exact (h_right hs ht hu).symm
-
-omit [Nonempty Ω'] in
-lemma condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
-    [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
-    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) :
-    (Y ⟂ᵢ[Z, hZ; μ] X)-- CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ
-      ↔ condDistrib Y (fun ω ↦ (X ω, Z ω)) μ
-          =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] Kernel.prodMkLeft _ (condDistrib Y Z μ) := by
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (μ := μ) (hX.prodMk hZ).aemeasurable
-    hY.aemeasurable, condIndepFun_comap_iff_map_prod_eq_prod_condDistrib_prod_condDistrib hY hX hZ,
-    Measure.compProd_eq_comp_prod]
-  let e : Ω' × Ω × β ≃ᵐ (β × Ω') × Ω := {
-    toFun := fun p ↦ ((p.2.2, p.1), p.2.1)
-    invFun := fun p ↦ (p.1.2, p.2, p.1.1)
-    left_inv p := by simp
-    right_inv p := by simp
-    measurable_toFun := by simp only [Equiv.coe_fn_mk]; fun_prop
-    measurable_invFun := by simp only [Equiv.coe_fn_symm_mk]; fun_prop }
-  have h_eq : ((condDistrib X Z μ ×ₖ Kernel.id) ×ₖ condDistrib Y Z μ) ∘ₘ μ.map Z
-      = (Kernel.id ×ₖ Kernel.prodMkLeft β (condDistrib Y Z μ)) ∘ₘ μ.map (fun a ↦ (X a, Z a)) := by
-    calc ((condDistrib X Z μ ×ₖ Kernel.id) ×ₖ condDistrib Y Z μ) ∘ₘ μ.map Z
-    _ = (Kernel.id ×ₖ Kernel.prodMkLeft β (condDistrib Y Z μ)) ∘ₘ Kernel.swap _ _
-        ∘ₘ (μ.map Z ⊗ₘ condDistrib X Z μ) := by
-      rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc, Measure.comp_assoc]
-      congr
-      rw [Kernel.comp_assoc, Kernel.swap_prod]
-      ext ω : 1
-      simp_rw [Kernel.prod_apply]
-      rw [Kernel.comp_apply, Kernel.prod_apply, Kernel.id_apply, ← Measure.compProd_eq_comp_prod]
-      ext s hs
-      rw [Measure.compProd_apply hs, Measure.prod_apply hs]
-      simp only [Kernel.prodMkLeft_apply]
-      rw [lintegral_prod, lintegral_prod]
-      · simp_rw [lintegral_dirac]
-      · refine Measurable.aemeasurable ?_
-        have : Measurable fun a ↦ (Kernel.prodMkLeft _ (condDistrib Y Z μ) a) (Prod.mk a ⁻¹' s) :=
-          Kernel.measurable_kernel_prodMk_left hs
-        exact this
-      · refine Measurable.aemeasurable ?_
-        have : Measurable fun x ↦ (Kernel.const _ ((condDistrib Y Z μ) ω) x) (Prod.mk x ⁻¹' s) :=
-          Kernel.measurable_kernel_prodMk_left hs
-        exact this
-    _ = (Kernel.id ×ₖ Kernel.prodMkLeft β (condDistrib Y Z μ)) ∘ₘ μ.map (fun a ↦ (X a, Z a)) := by
-      congr
-      rw [compProd_map_condDistrib hX.aemeasurable, Measure.swap_comp,
-        Measure.map_map (by fun_prop) (by fun_prop)]
-      rfl
-  rw [← h_eq]
-  have h1 : μ.map (fun x ↦ ((X x, Z x), Y x)) = (μ.map (fun a ↦ (Z a , Y a, X a))).map e := by
-    rw [Measure.map_map (by fun_prop) (by fun_prop)]
-    congr
-  have h1_symm : μ.map (fun a ↦ (Z a , Y a, X a))
-      = (μ.map (fun x ↦ ((X x, Z x), Y x))).map e.symm := by
-    rw [h1, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
-      Measure.map_id]
-  have h2 : (condDistrib X Z μ ×ₖ Kernel.id ×ₖ condDistrib Y Z μ) ∘ₘ μ.map Z
-      = ((Kernel.id ×ₖ (condDistrib Y Z μ ×ₖ condDistrib X Z μ)) ∘ₘ μ.map Z).map e := by
-    rw [← Measure.deterministic_comp_eq_map e.measurable, Measure.comp_assoc]
-    congr
-    ext ω : 1
-    rw [Kernel.prod_apply, Kernel.prod_apply, Kernel.id_apply, Kernel.comp_apply,
-      Kernel.prod_apply, Kernel.prod_apply, Kernel.id_apply, Measure.deterministic_comp_eq_map]
-    rw [Measure.ext_prod₃_iff']
-    intro s t u hs ht hu
-    rw [Measure.prod_prod, Measure.prod_prod,
-      Measure.map_apply (by fun_prop) ((hs.prod ht).prod hu)]
-    have : e ⁻¹' ((s ×ˢ t) ×ˢ u) = t ×ˢ u ×ˢ s := by
-      ext x
-      simp only [MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, Set.mem_preimage, Set.mem_prod, e]
-      tauto
-    rw [this]
-    simp_rw [Measure.prod_prod]
-    ring
-  have h2_symm : (Kernel.id ×ₖ (condDistrib Y Z μ ×ₖ condDistrib X Z μ)) ∘ₘ μ.map Z
-      = ((condDistrib X Z μ ×ₖ Kernel.id ×ₖ condDistrib Y Z μ) ∘ₘ μ.map Z).map e.symm := by
-    rw [h2, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
-      Measure.map_id]
-  rw [h1, h2]
-  exact ⟨fun h ↦ by rw [h], fun h ↦ by rw [h1_symm, h1, h2_symm, h2, h]⟩
-
 lemma Measure.snd_compProd_prodMkLeft {α β γ : Type*}
     {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
     {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] :
@@ -764,6 +141,17 @@ lemma Measure.snd_compProd_prodMkLeft {α β γ : Type*}
   simp only [Kernel.prodMkLeft_apply]
   congr
 
+lemma Measure.snd_compProd_prodMkRight {α β γ : Type*}
+    {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    {μ : Measure (α × β)} [SFinite μ] {κ : Kernel α γ} [IsSFiniteKernel κ] :
+    (μ ⊗ₘ (κ.prodMkRight β)).snd = κ ∘ₘ μ.fst := by
+  ext s hs
+  rw [Measure.snd_apply hs, Measure.compProd_apply (hs.preimage (by fun_prop)),
+    Measure.bind_apply hs (by fun_prop), Measure.fst,
+    lintegral_map (κ.measurable_coe hs) (by fun_prop)]
+  simp only [Kernel.prodMkRight_apply]
+  congr
+
 lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*}
     {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
     {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] :
@@ -776,6 +164,20 @@ lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*}
   · exact Kernel.measurable_kernel_prodMk_left hs
   · exact hs.preimage (by fun_prop)
 
+lemma Measure.todo {α β γ : Type*}
+    {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    {μ : Measure (α × β)} [SFinite μ] {κ : Kernel α γ} [IsSFiniteKernel κ] :
+    (((((μ ⊗ₘ (κ.prodMkRight β))).map Prod.swap).map MeasurableEquiv.prodAssoc.symm).fst).map
+        Prod.swap
+      = μ.fst ⊗ₘ κ := by
+  rw [Measure.map_map (by fun_prop) (by fun_prop), Measure.fst,
+    Measure.map_map (by fun_prop) (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop)]
+  ext s hs
+  rw [Measure.map_apply (by fun_prop) hs, Measure.compProd_apply hs,
+    Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.fst, lintegral_map _ (by fun_prop)]
+  · congr
+  · exact Kernel.measurable_kernel_prodMk_left hs
+
 lemma ProbabilityMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α}
     {μ ν : ProbabilityMeasure α} :
     μ = ν ↔ (μ : Measure α) = ν := Subtype.ext_iff
@@ -802,6 +204,7 @@ theorem FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) =
   rfl
 
 instance : CanonicallyOrderedAdd (FiniteMeasure α) where
+  le_add_self := sorry -- was not needed before?
   exists_add_of_le {μ ν} hμν := by
     refine ⟨ν - μ, ?_⟩
     rw [FiniteMeasure.ext_iff_coe]
@@ -825,30 +228,51 @@ lemma Kernel.prodMkLeft_ae_eq_iff [MeasurableSpace.CountableOrCountablyGenerated
   · classical
     exact Kernel.measurableSet_eq κ η
 
-omit [Nonempty Ω'] in
-lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
+lemma Kernel.prodMkRight_ae_eq_iff [MeasurableSpace.CountableOrCountablyGenerated α β]
+    {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η]
+    {μ : Measure (α × γ)} :
+    κ.prodMkRight γ =ᵐ[μ] η.prodMkRight γ ↔ κ =ᵐ[μ.fst] η := by
+  rw [Measure.fst, Filter.EventuallyEq, Filter.EventuallyEq, ae_map_iff (by fun_prop)]
+  · simp
+  · classical
+    exact Kernel.measurableSet_eq κ η
+
+omit [StandardBorelSpace Ω'] [Nonempty Ω'] in
+lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight
     [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
     (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) {η : Kernel Ω' Ω}
     [IsMarkovKernel η]
-    (h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) :
+    (h : condDistrib Y (fun ω ↦ (Z ω, X ω)) μ =ᵐ[μ.map (fun ω ↦ (Z ω, X ω))] η.prodMkRight _) :
     Y ⟂ᵢ[Z, hZ; μ] X := by
   have hη_eq : condDistrib Y Z μ =ᵐ[μ.map Z] η := by
-    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h ⊢
-    have h_snd : μ.map Z = (μ.map (fun ω ↦ (X ω, Z ω))).snd := by
-      rw [Measure.snd_map_prodMk hX]
-    rw [h_snd, ← Measure.snd_prodAssoc_compProd_prodMkLeft, ← h,
-      Measure.map_map (by fun_prop) (by fun_prop), Measure.snd_map_prodMk (by fun_prop)]
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h ⊢
+    have h_fst : μ.map Z = (μ.map (fun ω ↦ (Z ω, X ω))).fst := by
+      rw [Measure.fst_map_prodMk hX]
+    rw [h_fst, ← Measure.todo, ← h, Measure.map_map (by fun_prop) (by fun_prop),
+      Measure.map_map (by fun_prop) (by fun_prop), Measure.fst,
+      Measure.map_map (by fun_prop) (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop)]
     congr
-  rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft hX hY hZ]
+  symm
+  rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ]
   refine h.trans ?_
-  rw [Kernel.prodMkLeft_ae_eq_iff, Measure.snd_map_prodMk (by fun_prop)]
+  rw [Kernel.prodMkRight_ae_eq_iff, Measure.fst_map_prodMk (by fun_prop)]
   exact hη_eq.symm
 
+omit [StandardBorelSpace Ω'] [Nonempty Ω'] in
+lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
+    [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
+    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) {η : Kernel Ω' Ω}
+    [IsMarkovKernel η]
+    (h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) :
+    Y ⟂ᵢ[Z, hZ; μ] X := by
+  refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight hX hY hZ ?_ (η := η)
+  sorry
+
 /-- Law of `Y` conditioned on `X`. -/
 notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ
 
 -- generalize to map instead of fst
-omit [Nonempty Ω'] in
+omit [StandardBorelSpace Ω'] [Nonempty Ω'] in
 lemma condIndepFun_fst_prod [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
     [StandardBorelSpace γ]
     (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
@@ -856,12 +280,12 @@ lemma condIndepFun_fst_prod [StandardBorelSpace α] [StandardBorelSpace β] [Non
     (h_indep : CondIndepFun (mΩ'.comap Z) hZ.comap_le Y X μ) :
     CondIndepFun (mΩ'.comap (fun ω ↦ Z ω.1)) (hZ.comp measurable_fst).comap_le
       (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν) := by
-  rw [condIndepFun_comap_iff_map_prod_eq_prod_condDistrib_prod_condDistrib (by fun_prop)
+  rw [condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib (by fun_prop)
     (by fun_prop) (by fun_prop)] at h_indep ⊢
   have h1 : 𝓛[fun ω ↦ Y ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[Y | Z; μ] :=
-    condDistrib_fst_prod (Y := Y) (X := Z) (ν := ν) (μ := μ) (by fun_prop) (by fun_prop)
+    condDistrib_fst_prod (Y := Y) (X := Z) (ν := ν) (μ := μ) (by fun_prop)
   have h2 : 𝓛[fun ω ↦ X ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[X | Z; μ] :=
-    condDistrib_fst_prod (Y := X) (X := Z) (ν := ν) (μ := μ) (by fun_prop) (by fun_prop)
+    condDistrib_fst_prod (Y := X) (X := Z) (ν := ν) (μ := μ) (by fun_prop)
   have h_fst1 : (μ.prod ν).map (fun ω ↦ Z ω.1) = μ.map Z := by
     conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst,
       Measure.map_map (by fun_prop) (by fun_prop)]
@@ -929,10 +353,6 @@ end CondDistrib
 
 section Cond
 
-lemma ae_cond_of_forall_mem {μ : Measure α} {s : Set α}
-    (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) :
-    ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _
-
 lemma condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β]
     [IsFiniteMeasure μ]
     (hX : Measurable X) (hY : Measurable Y) :
@@ -966,18 +386,19 @@ lemma cond_of_condIndepFun [StandardBorelSpace α] [StandardBorelSpace β] [None
     (hZ : Measurable Z)
     (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ)
     (hX : Measurable X) (hY : Measurable Y) {b : β} {ω : Ω'}
-    (hμ : μ (X ⁻¹' {b} ∩ Z ⁻¹' {ω}) ≠ 0) :
-    (μ[|X ⁻¹' {b} ∩ Z ⁻¹' {ω}]).map Y = (μ[|Z ⁻¹' {ω}]).map Y := by
-  have h := (condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft hX hY hZ).mp h
-  have h_left := condDistrib_ae_eq_cond (hX.prodMk hZ) hY (μ := μ)
+    (hμ : μ (Z ⁻¹' {ω} ∩ X ⁻¹' {b}) ≠ 0) :
+    (μ[|Z ⁻¹' {ω} ∩ X ⁻¹' {b}]).map Y = (μ[|Z ⁻¹' {ω}]).map Y := by
+  symm at h
+  have h := (condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ).mp h
+  have h_left := condDistrib_ae_eq_cond (hZ.prodMk hX) hY (μ := μ)
   have h_right := condDistrib_ae_eq_cond hZ hY (μ := μ)
   rw [Filter.EventuallyEq, ae_iff_of_countable] at h h_left h_right
-  specialize h (b, ω)
-  specialize h_left (b, ω)
+  specialize h (ω, b)
+  specialize h_left (ω, b)
   specialize h_right ω
   rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at h h_left h_right
   rw [← Set.singleton_prod_singleton, Set.mk_preimage_prod] at h h_left
-  have hZ_ne : μ (Z ⁻¹' {ω}) ≠ 0 := fun h ↦ hμ (measure_mono_null Set.inter_subset_right h)
+  have hZ_ne : μ (Z ⁻¹' {ω}) ≠ 0 := fun h ↦ hμ (measure_mono_null Set.inter_subset_left h)
   rw [← h_right hZ_ne, ← h_left hμ, h hμ]
   simp
 
diff --git a/LeanBandits/ForMathlib/KernelCompositionLemmas.lean b/LeanBandits/ForMathlib/KernelCompositionLemmas.lean
deleted file mode 100644
index 154af51f..00000000
--- a/LeanBandits/ForMathlib/KernelCompositionLemmas.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-import Mathlib.Probability.Kernel.Composition.Lemmas
-import LeanBandits.ForMathlib.KernelCompositionParallelComp
-
-open MeasureTheory ProbabilityTheory
-open scoped ENNReal
-
-variable {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
-  {μ : Measure α} {ν : Measure β} {κ : Kernel α β}
-
--- PR: https://github.com/leanprover-community/mathlib4/pull/29555
-lemma MeasureTheory.Measure.compProd_map [SFinite μ] [IsSFiniteKernel κ]
-    {f : β → γ} (hf : Measurable f) :
-    μ ⊗ₘ (κ.map f) = (μ ⊗ₘ κ).map (Prod.map id f) := by
-  calc μ ⊗ₘ (κ.map f)
-  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
-    rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
-      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
-  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
-  _ = (μ ⊗ₘ κ).map (Prod.map id f) := by
-    rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
diff --git a/LeanBandits/ForMathlib/KernelCompositionParallelComp.lean b/LeanBandits/ForMathlib/KernelCompositionParallelComp.lean
deleted file mode 100644
index 4dd863f8..00000000
--- a/LeanBandits/ForMathlib/KernelCompositionParallelComp.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import Mathlib.Probability.Kernel.Composition.ParallelComp
-
-open MeasureTheory
-open scoped ENNReal
-
-namespace ProbabilityTheory.Kernel
-
-variable {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
-  {κ : Kernel α β} {η : Kernel γ δ} {x : α × γ}
-
--- PR: https://github.com/leanprover-community/mathlib4/pull/29555
-lemma parallelComp_apply_prod [IsSFiniteKernel κ] [IsSFiniteKernel η] (s : Set β) (t : Set δ) :
-    (κ ∥ₖ η) x (s ×ˢ t) = (κ x.1 s) * (η x.2 t) := by
-  rw [parallelComp_apply, Measure.prod_prod]
-
--- PR: https://github.com/leanprover-community/mathlib4/pull/29555
-lemma deterministic_parallelComp_deterministic
-    {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g) :
-    (deterministic f hf) ∥ₖ (deterministic g hg)
-      = deterministic (Prod.map f g) (hf.prodMap hg) := by
-  ext x : 1
-  rw [parallelComp_apply, deterministic_apply, deterministic_apply, deterministic_apply, Prod.map,
-    Measure.dirac_prod_dirac]
-
-end ProbabilityTheory.Kernel
diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean
index 43e852e6..eb509fc3 100644
--- a/LeanBandits/ForMathlib/Traj.lean
+++ b/LeanBandits/ForMathlib/Traj.lean
@@ -1,7 +1,6 @@
 import Mathlib.Probability.Kernel.IonescuTulcea.Traj
 import Mathlib.Probability.Kernel.CondDistrib
 import LeanBandits.ForMathlib.CondDistrib
-import LeanBandits.ForMathlib.KernelCompositionLemmas
 
 open Filter Finset Function MeasurableEquiv MeasurableSpace MeasureTheory Preorder ProbabilityTheory
 
@@ -38,7 +37,7 @@ def trajMeasure (μ₀ : Measure (X 0)) (κ : (n : ℕ) → Kernel (Π i : Iic n
 instance : IsProbabilityMeasure (trajMeasure μ₀ κ) := by
   rw [trajMeasure]
   have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero _).symm) :=
-    isProbabilityMeasure_map <| by fun_prop
+    Measure.isProbabilityMeasure_map <| by fun_prop
   infer_instance
 
 -- Probability/Kernel/IonescuTulcea/Traj.lean
@@ -79,7 +78,7 @@ lemma condDistrib_trajMeasure_ae_eq_kernel {a : ℕ}
     [StandardBorelSpace (X (a + 1))] [Nonempty (X (a + 1))] :
     condDistrib (fun x ↦ x (a + 1)) (frestrictLe a) (trajMeasure μ₀ κ)
       =ᵐ[(trajMeasure μ₀ κ).map (frestrictLe a)] κ a := by
-  apply condDistrib_ae_eq_of_measure_eq_compProd₀ (by measurability) (by measurability)
+  apply condDistrib_ae_eq_of_measure_eq_compProd _ (by measurability)
   exact trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map.symm
 
 lemma traj_zero_map_eval_zero :
diff --git a/LeanBandits/Regret.lean b/LeanBandits/Regret.lean
index c0720afe..600e4bab 100644
--- a/LeanBandits/Regret.lean
+++ b/LeanBandits/Regret.lean
@@ -56,10 +56,10 @@ lemma monotone_pullCount (a : α) (h : ℕ → α × ℝ) : Monotone (pullCount
 
 lemma pullCount_eq_pullCount_add_one (t : ℕ) (h : ℕ → α × ℝ) :
     pullCount (arm t h) (t + 1) h = pullCount (arm t h) t h + 1 := by
-  simp [pullCount, range_succ, filter_insert]
+  simp [pullCount, range_add_one, filter_insert]
 
 lemma pullCount_eq_pullCount (ha : arm t h ≠ a) :  pullCount a (t + 1) h = pullCount a t h := by
-  simp [pullCount, range_succ, filter_insert, ha]
+  simp [pullCount, range_add_one, filter_insert, ha]
 
 lemma pullCount_add_one :
     pullCount a (t + 1) h = pullCount a t h + if arm t h = a then 1 else 0 := by
@@ -257,15 +257,16 @@ lemma rewardByCount_pullCount_add_one_eq_reward (t : ℕ) (h : ℕ → α × ℝ
 lemma sum_rewardByCount_eq_sumRewards
     (a : α) (t : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) :
     ∑ m ∈ Icc 1 (pullCount a t h), rewardByCount a m h z = sumRewards a t h := by
-  induction' t with t ht
-  · simp [pullCount, sumRewards]
-  by_cases hta : arm t h = a
-  · rw [← hta] at ht ⊢
-    rw [pullCount_eq_pullCount_add_one, sum_Icc_succ_top (Nat.le_add_left 1 _), ht]
-    unfold sumRewards
-    rw [sum_range_succ, if_pos rfl, rewardByCount_pullCount_add_one_eq_reward]
-  · unfold sumRewards
-    rwa [pullCount_eq_pullCount hta, sum_range_succ, if_neg hta, add_zero]
+  induction t with
+  | zero => simp [pullCount, sumRewards]
+  | succ t ht =>
+    by_cases hta : arm t h = a
+    · rw [← hta] at ht ⊢
+      rw [pullCount_eq_pullCount_add_one, sum_Icc_succ_top (Nat.le_add_left 1 _), ht]
+      unfold sumRewards
+      rw [sum_range_succ, if_pos rfl, rewardByCount_pullCount_add_one_eq_reward]
+    · unfold sumRewards
+      rwa [pullCount_eq_pullCount hta, sum_range_succ, if_neg hta, add_zero]
 
 lemma sum_pullCount_mul [Fintype α] (h : ℕ → α × ℝ) (f : α → ℝ) (t : ℕ) :
     ∑ a, pullCount a t h * f a = ∑ s ∈ range t, f (arm s h) := by
diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean
index 7c482f1c..ae52fc59 100644
--- a/LeanBandits/RewardByCountMeasure.lean
+++ b/LeanBandits/RewardByCountMeasure.lean
@@ -119,7 +119,7 @@ lemma condDistrib_reward'' [StandardBorelSpace α] [Nonempty α] (n : ℕ) :
   rw [h_law]
   have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ]
       =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] :=
-    condDistrib_fst_prod (by fun_prop) (by fun_prop) _
+    condDistrib_fst_prod _ (by fun_prop) _
   filter_upwards [h_ra', h_prod] with ω h_eq h_prod
   rw [h_prod, h_eq]
 
@@ -193,7 +193,7 @@ lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α]
     by_cases hm1 : m = 1
     · simp only [hm1, true_and]
       have h_indep := condIndepFun_self_right (X := reward 0) (Z := arm 0)
-        (mβ := inferInstance) (mδ := inferInstance) (μ := Bandit.trajMeasure alg ν)
+        (mβ := inferInstance) (mβ' := inferInstance) (μ := Bandit.trajMeasure alg ν)
         (by fun_prop) (by fun_prop)
       have : {ω : ℕ → α × ℝ | arm 0 ω = a}.indicator (fun x ↦ 1)
           = {b | b = a}.indicator (fun _ ↦ 1) ∘ arm 0 := by ext; simp [Set.indicator]
@@ -247,18 +247,22 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α
     congr with ω
     simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and]
     exact arm_eq_of_stepsUntil_eq_coe hm
-  _ = (μ[|{ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) | stepsUntil a m ω.1 = ↑n}.indicator 1 ⁻¹' {1}
-      ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map (fun ω ↦ reward n ω.1) := by
-    congr 3 with ω
-    simp [Set.indicator_apply]
+  _ = (μ[|(fun ω ↦ arm n ω.1) ⁻¹' {a}
+      ∩ {ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) | stepsUntil a m ω.1 = ↑n}.indicator 1 ⁻¹' {1} ]).map
+      (fun ω ↦ reward n ω.1) := by
+    congr 2 with ω
+    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, Set.indicator_apply,
+      Set.mem_setOf_eq, Pi.one_apply, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
+    rw [and_comm]
   _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by
     rw [cond_of_condIndepFun (by fun_prop)]
     · exact condIndepFun_reward_stepsUntil_arm a m n hm
     · refine measurable_one.indicator ?_
       exact measurableSet_eq_fun' (by fun_prop) (by fun_prop)
     · fun_prop
-    · convert hμna
-      ext ω
+    · convert hμna using 2
+      rw [Set.inter_comm]
+      congr 1 with ω
       simp [Set.indicator_apply]
   _ = ν a := reward_cond_arm a n hμa
 
@@ -315,7 +319,7 @@ lemma hasLaw_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α]
     _ = ν a := by
       have : IsProbabilityMeasure
           ((Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)) :=
-        isProbabilityMeasure_map (by fun_prop)
+        Measure.isProbabilityMeasure_map (by fun_prop)
       simp
 
 lemma identDistrib_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α] (a : α) (n m : ℕ)
diff --git a/lake-manifest.json b/lake-manifest.json
index bb1980fe..eeaccc54 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b0be57cc5ec46a829c6afaf7b9c5c5d61b8dbffb",
+   "rev": "f07bd0325121718862be33645a23c4e55791271a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
+   "rev": "7607162f5a1c1eb23c23027629a418b3a160670e",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
+   "rev": "e5c37730d22634ee0169c164f25dac49918ed951",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
+   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.71",
+   "inputRev": "v0.0.77",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
+   "rev": "cbe864cd5177966c9e005418cfdc1fb36db62e13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
+   "rev": "593aa51c4aa07ee81e9233b53e1f61a5b4d9f761",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a67fc66cd1ebc0855dc064a4be727798771c0f89",
+   "rev": "5bd478197f2e5d2a4fde527cf3581d83f49baa9b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
+   "rev": "f75f4926aff7ba19949e16c19094d7298806b1a6",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanBandits",
diff --git a/lean-toolchain b/lean-toolchain
index 27770b57..2264e7fe 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.23.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.25.0-rc1
\ No newline at end of file