oops

src/Init/Data/Bool.lean

@@ -547,7 +547,7 @@ theorem apply_cond (f : α → β) {b : Bool} {a a' : α} :
     f (bif b then a else a') = bif b then f a else f a' := by
   cases b <;> simp
 
-/-# decidability -/
+/-! # decidability -/
 
 protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true
 

src/Init/Data/List/Find.lean

@@ -257,8 +257,7 @@ theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
   simp
 
 @[simp] theorem find?_filterMap (xs : List α) (f : α → Option β) (p : β → Bool) :
-    List.find? p (List.filterMap f xs) =
-      (xs.find? (fun a => match f a with | none => false | some b => p b)).bind f := by
+    (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
   induction xs with
   | nil => simp
   | cons x xs ih =>