by
  let R' := reward alg (n + 1)
  let H := (hist alg · n)
  let A := action alg (n + 1)
  let P := fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω
  have hP : Measurable P := measurable_pullCount_action_add_one alg n
  change HasCondDistrib R' (fun ω ↦ (H ω, A ω)) (ν.prodMkLeft _) _
  suffices HasCondDistrib R' (fun ω ↦ (A ω, H ω)) (ν.prodMkRight _) (arrayMeasure ν) by
    have h_eq : (fun ω ↦ (H ω, A ω)) = MeasurableEquiv.prodComm ∘ (fun ω ↦ (A ω, H ω)) := rfl
    rw [h_eq]
    exact this.measurableEquiv_comp_right (κ := ν.prodMkRight _) _
  suffices HasCondDistrib R' (fun ω ↦ ((A ω, H ω), P ω))
      ((ν.prodMkRight _).prodMkRight _) (arrayMeasure ν) by
    -- use that `P` is measurable wrt `(A, H)` to drop it from the conditioning
    have hP_meas :
        Measurable[MeasurableSpace.comap (fun ω ↦ (A ω, H ω)) inferInstance] P :=
      measurable_pullCount_action_add_one_hist alg n
    obtain ⟨f, hf_meas, hf_eq⟩ := hP_meas.exists_eq_measurable_comp
    simp only [hf_eq, Function.comp_apply] at this
    rwa [hasCondDistrib_prod_right_iff _ _ hf_meas] at this
  suffices HasCondDistrib R' (fun ω ↦ ((A ω, P ω), H ω))
      ((ν.prodMkRight _).prodMkRight _) (arrayMeasure ν) by
    let e : ((𝓐 × ℕ) × (Iic n → 𝓐 × R)) ≃ᵐ ((𝓐 × (Iic n → 𝓐 × R)) × ℕ) :=
    { toFun := fun x ↦ ((x.1.1, x.2), x.1.2)
      invFun := fun x ↦ ((x.1.1, x.2), x.1.2)
      measurable_toFun := by simp only [Equiv.coe_fn_mk]; fun_prop
      measurable_invFun := by simp only [Equiv.symm_mk, Equiv.coe_fn_mk]; fun_prop }
    exact this.measurableEquiv_comp_right e
  suffices HasCondDistrib R' (fun ω ↦ (A ω, P ω)) (ν.prodMkRight _) (arrayMeasure ν) by
    have h_indep : H ⟂ᵢ[(fun ω ↦ (A ω, P ω)), (by fun_prop); arrayMeasure ν] R' :=
      (condIndepFun_reward_hist alg ν n).symm
    have h_condDistrib := this.condDistrib_eq
    rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (by fun_prop) (by fun_prop)
      (by fun_prop)] at h_indep
    refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_
    refine h_indep.trans ?_
    rw [Filter.EventuallyEq, ae_map_iff] at h_condDistrib ⊢
    · simpa only [Kernel.prodMkRight_apply]
    · fun_prop
    · exact Kernel.measurableSet_eq _ _
    · fun_prop
    · exact Kernel.measurableSet_eq _ _
  exact hasCondDistrib_reward_pullCount_action alg ν n