fix(topology/algebra/module/multilinear): initialize simps projections (

#14495)

* `continuous_multilinear_map.smul_right` has a `simps` attribute, causing the generation of the simps projections for `continuous_multilinear_map`, but without specific support for apply. We now initialize the simps projections correctly.
* This fixes an error in the sphere eversion project

src/topology/algebra/module/multilinear.lean

@@ -66,6 +66,13 @@ variables [semiring R]
 instance : has_coe_to_fun (continuous_multilinear_map R M₁ M₂) (λ _, (Π i, M₁ i) → M₂) :=
 ⟨λ f, f.to_fun⟩
 
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+  because it is a composition of multiple projections. -/
+def simps.apply (L₁ : continuous_multilinear_map R M₁ M₂) (v : Π i, M₁ i) : M₂ := L₁ v
+
+initialize_simps_projections continuous_multilinear_map
+  (-to_multilinear_map, to_multilinear_map_to_fun → apply)
+
 @[continuity] lemma coe_continuous : continuous (f : (Π i, M₁ i) → M₂) := f.cont
 
 @[simp] lemma coe_coe : (f.to_multilinear_map : (Π i, M₁ i) → M₂) = f := rfl
@@ -461,14 +468,10 @@ variables [comm_semiring R] [Π i, add_comm_monoid (M₁ i)] [add_comm_monoid M
 
 /-- Given a continuous `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the
 continuous multilinear map sending `m` to `f m • z`. -/
-@[simps] def smul_right : continuous_multilinear_map R M₁ M₂ :=
+@[simps to_multilinear_map apply] def smul_right : continuous_multilinear_map R M₁ M₂ :=
 { to_multilinear_map := f.to_multilinear_map.smul_right z,
   cont := f.cont.smul continuous_const }
 
-@[simp] lemma smul_right_apply (m : Π i, M₁ i) :
-  f.smul_right z m = (f m) • z :=
-rfl
-
 end smul_right
 
 end continuous_multilinear_map