mathlib

e4607f8f - chore(data/sym/basic): golf and add missing simp lemmas (#11160)

chore(data/sym/basic): golf and add missing simp lemmas (#11160) By changing `cons` to not use pattern matching, `(a :: s).1 = a ::ₘ s.1` is true by `rfl`, which is convenient here and there for golfing.