mathlib3

[Merged by Bors] - fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument

#19228

Closed