by
  classical
  have h_union : {h' : Ω | ∃ s, pullCount A a (s + 1) h' = m}
      = ⋃ s : ℕ, {h' | pullCount A a (s + 1) h' = m} := by ext; simp
  have h_meas_set : MeasurableSet {h' : Ω | ∃ s, pullCount A a (s + 1) h' = m} := by
    rw [h_union]
    refine MeasurableSet.iUnion fun s ↦ (measurableSet_singleton _).preimage ?_
    exact measurable_pullCount hA a (s + 1)
  suffices Measurable fun k ↦ if h : k ∈ {k' | ∃ s, pullCount A a (s + 1) k' = m}
      then (Nat.find h : ℕ∞) else ⊤ by
    convert this with ω
    rw [stepsUntil_eq_dite a m ω]
    rfl
  refine Measurable.dite (s := {k' : Ω | ∃ s, pullCount A a (s + 1) k' = m})
    (f := fun x ↦ (Nat.find x.2 : ℕ∞)) (g := fun _ ↦ ⊤) ?_ (by fun_prop) h_meas_set
  refine Measurable.coe_nat_enat ?_
  refine measurable_find _ fun k ↦ ?_
  suffices MeasurableSet {x : Ω | pullCount A a (k + 1) x = m} by
    have : Subtype.val '' {x : {k' : Ω |
          ∃ s, pullCount A a (s + 1) k' = m} | pullCount A a (k + 1) (x : Ω) = m}
        = {x : Ω | pullCount A a (k + 1) x = m} := by
      ext x
      simp only [Set.mem_ofPred_eq, Set.coe_ofPred, Set.mem_image, Subtype.exists, exists_and_left,
        exists_prop, exists_eq_right_right, and_iff_left_iff_imp]
      exact fun h ↦ ⟨_, h⟩
    refine (MeasurableEmbedding.subtype_coe h_meas_set).measurableSet_image.mp ?_
    rw [this]
    exact (measurableSet_singleton _).preimage (by fun_prop)
  exact (measurableSet_singleton _).preimage (by fun_prop)