mathlib3

52b64a6b - Fix `ring_theory/derivation.lean` (simp normal form, help the elaborator)