∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [LawfulMonad m] [Std.Iterators.Finite α m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : β → m (ULift.{w, 0} Bool)},
  it.findM? f = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← f out
        if __do_lift.down = true then pure (some out) else it'.findM? f
      | Std.IterStep.skip it' => it'.findM? f
      | Std.IterStep.done => pure none