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>

src/data/polynomial/basic.lean

@@ -35,9 +35,11 @@ the polynomials. For instance,
 
 Polynomials are defined using `add_monoid_algebra R ℕ`, where `R` is a commutative semiring, but
 through a structure to make them irreducible from the point of view of the kernel. Most operations
-are irreducible since Lean can not compute anyway with `add_monoid_algebra`. An exception is the
-zero polynomial, that we make semireducible so that its coefficients are definitionally
-equal to `0`.
+are irreducible since Lean can not compute anyway with `add_monoid_algebra`. There are two
+exceptions that we make semireducible:
+* The zero polynomial, so that its coefficients are definitionally equal to `0`.
+* The scalar action, to permit typeclass search to unfold it to resolve potential instance
+  diamonds.
 
 The raw implementation of the equivalence between `polynomial R` and `add_monoid_algebra R ℕ` is
 done through `of_finsupp` and `to_finsupp` (or, equivalently, `rcases p` when `p` is a polynomial
@@ -81,16 +83,14 @@ lemma exists_iff_exists_finsupp (P : polynomial R → Prop) :
 | ⟨a⟩ := ⟨-a⟩
 @[irreducible] private def mul : polynomial R → polynomial R → polynomial R
 | ⟨a⟩ ⟨b⟩ := ⟨a * b⟩
-@[irreducible] private def smul {S : Type*} [monoid S] [distrib_mul_action S R] :
-  S → polynomial R → polynomial R
-| a ⟨b⟩ := ⟨a • b⟩
 
 instance : has_zero (polynomial R) := ⟨⟨0⟩⟩
 instance : has_one (polynomial R) := ⟨monomial_fun 0 (1 : R)⟩
 instance : has_add (polynomial R) := ⟨add⟩
 instance {R : Type u} [ring R] : has_neg (polynomial R) := ⟨neg⟩
 instance : has_mul (polynomial R) := ⟨mul⟩
-instance {S : Type*} [monoid S] [distrib_mul_action S R] : has_scalar S (polynomial R) := ⟨smul⟩
+instance {S : Type*} [monoid S] [distrib_mul_action S R] : has_scalar S (polynomial R) :=
+⟨λ r p, ⟨r • p.to_finsupp⟩⟩
 
 lemma zero_to_finsupp : (⟨0⟩ : polynomial R) = 0 :=
 rfl
@@ -107,7 +107,7 @@ lemma neg_to_finsupp {R : Type u} [ring R] {a} : (-⟨a⟩ : polynomial R) = ⟨
 show neg _ = _, by rw neg
 lemma mul_to_finsupp {a b} : (⟨a⟩ * ⟨b⟩ : polynomial R) = ⟨a * b⟩ := show mul _ _ = _, by rw mul
 lemma smul_to_finsupp {S : Type*} [monoid S] [distrib_mul_action S R] {a : S} {b} :
-  (a • ⟨b⟩ : polynomial R) = ⟨a • b⟩ := show smul _ _ = _, by rw smul
+  (a • ⟨b⟩ : polynomial R) = ⟨a • b⟩ := rfl
 
 instance : inhabited (polynomial R) := ⟨0⟩
 

src/ring_theory/polynomial_algebra.lean

@@ -46,7 +46,7 @@ namespace poly_equiv_tensor
 The function underlying `A ⊗[R] polynomial R →ₐ[R] polynomial A`,
 as a bilinear function of two arguments.
 -/
-@[simps]
+@[simps apply_apply]
 def to_fun_bilinear : A →ₗ[A] polynomial R →ₗ[R] polynomial A :=
 linear_map.to_span_singleton A _ (aeval (polynomial.X : polynomial A)).to_linear_map
 

test/instance_diamonds.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+
+import algebra.module.pi
+import data.polynomial.basic
+import group_theory.group_action.prod
+import group_theory.group_action.units
+
+/-! # Tests that instances do not form diamonds -/
+
+/-! ## Scalar action instances -/
+section has_scalar
+
+section units
+
+example (α : Type*) [monoid α] :
+  (units.mul_action : mul_action (units α) (α × α)) = prod.mul_action := rfl
+
+example (R α : Type*) (β : α → Type*) [monoid R] [Π i, mul_action R (β i)] :
+  (units.mul_action : mul_action (units R) (Π i, β i)) = pi.mul_action _ := rfl
+
+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
+
+/-!
+TODO: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/units.2Emul_action'.20diamond/near/246402813
+```lean
+example {α : Type*} [comm_monoid α] :
+  (units.mul_action' : mul_action (units α) (units α)) = monoid.to_mul_action _ :=
+rfl -- fails
+```
+-/
+
+end units
+
+end has_scalar