Commit 2025-01-07 07:29 1327df05

chore: smile more often (#20436) This replaces : _) with the shorter and otherwise almost identical :). The former is a Lean 3 ism; or at least, the latter is new syntax in Lean 4. More precisely (thanks @kmill):

• (e : _) elaborates e without an expected type, and then it inserts a coercion if the type of e does not match the expected type.
• (e :) elaborates e without an expected type to completion, and then it inserts a coercion if the type of e does not match the expected type. A few places break when switched to :); in many of these cases, the : _)/:) can just be dropped entirely. The remainder are left as is.