induction L with
| nil => simp_all [pure, Except.pure]
| cons hd tl ih =>
  simp [bind, Except.bind]
  by_cases f hd = true <;> simp_all
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
no goals