feat: simproc for functions out of Subtype

[kim-em]

Adds a simproc that will replace l.map f, where l : {x // p x} and f syntactically only depends on the value, with l.map (f' ∘Subtype.val).

In combination with

@[simp] theorem map_attach_comp_subtype_val {l : List α} :
    l.attach.map (f ∘ Subtype.val) = l.map f := by
  simp [map_attach]

this allows us to automatically clear attach:

inductive Tree where | node : List Tree → Tree

def Tree.rev : Tree → Tree
  | node ts => .node (ts.attach.reverse.map (fun ⟨t, _⟩ => t.rev))

@[simp] theorem Tree.rev_def (ts : List Tree) :
    Tree.rev (.node ts) = .node (ts.reverse.map rev) := by
  simp [Tree.rev]

(Credit to David and Joachim for suggesting this!)

---

TODO: add simprocs and simp lemmas for other higher order operations besides map.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 90cb6e5da857f8d8c361dbef910206bb7c1cfe6d --onto 7845a05cf1094f24a5c4a51c32dd84bf4ff31a54. (2024-09-26 02:38:54)

[kim-em]

Closing in favour of #5479