mathlib3

6efc3e91 - fix(data/polynomial): Resolve a has_scalar instance diamond (#8392)

fix(data/polynomial): Resolve a has_scalar instance diamond (#8392) Without this change, the following fails to close the diamond between `units.distrib_mul_action` and`polynomial.distrib_mul_action`: ```lean example (R α : Type*) (β : α → Type*) [monoid R] [semiring α] [distrib_mul_action R α] : (units.distrib_mul_action : distrib_mul_action (units R) (polynomial α)) = polynomial.distrib_mul_action := rfl ``` This was because both used `polynomial.smul`, which was: * `@[irreducible]`, which means that typeclass search is unable to unfold it to see there is no diamond * Defined using a pattern match, which means that even if it were not reducible, it does not unfold as needed. This adds a new test file with this diamond and some other diamonds to verify they are defeq. Unfortunately this means `simps` now aggressively unfolds `•` on polynomials into `finsupp`s, so we need to tell `simps` precisely what lemma we actually want. This only happens in one place though. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/units.2Ehas_scalar.20and.20polynomial.2Ehas_scalar.20diamond/near/246800881) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>