chore: avoid unbracketed by within suffices (#32342)

This is a preparatory PR which will allow us to increase the precedence of the `by` notation.

The issue is that the `suffices A by ...`/`suffices A from ...` notation can get confused, if `A` contains an unbracketed `by`.

Author: JovanGerb

Mathlib/SetTheory/Lists.lean

@@ -99,7 +99,7 @@ theorem to_ofList (l : List (Lists α)) : toList (ofList l) = l := by induction
 theorem of_toList : ∀ l : Lists' α true, ofList (toList l) = l :=
   suffices
     ∀ (b) (h : true = b) (l : Lists' α b),
-      let l' : Lists' α true := by rw [h]; exact l
+      let l' : Lists' α true := h ▸ l
       ofList (toList l') = l'
     from this _ rfl
   fun b h l => by