∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Monad m] [LawfulMonad m] [inst_5 : Monad n]
  [inst_6 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] {it : Std.IterM m β}
  {f : β → n (Option β')} {p : β' → n (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.IterM.filterMapM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => p fx
          | none => pure { down := true })
      (Std.IterM.mapM pure it)