mathlib3

0324bd3f - fix(ring_theory/derivation): speed up a slow definition (#18457)

fix(ring_theory/derivation): speed up a slow definition (#18457) 16s to 3s. I don't know which of the changes is responsible for the speedup, but they all seem sensible anyway. With the explicit `to_fun` field, we may as well use `simps` to generate a lemma for us.