by_cases f hd = true <;> simp_all
case cons
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
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () tl =
      Except.ok () ↔
    ∀ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.ok () else Except.error () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.ok () else Except.error ()) v tl) =
      Except.ok () ↔
    f hd = true ∧ ∀ a ∈ tl, f a = true
no goals