chore(algebra/algebra/restrict_scalars): replace `restrict_scalars_sm…

…ul_def` with version that does not commit defeq-abuse. (#18540)

This lemma abuses definitional equality and I think we are better without it. My immediate motivation is the trouble it is causing in the Mathlib4 porting PR: leanprover-community/mathlib4#2563

Note that it was only used in one place and there is a better proof.

src/algebra/algebra/restrict_scalars.lean

@@ -148,19 +148,16 @@ add_equiv.refl M
 
 variables [comm_semiring R] [semiring S] [algebra R S] [module S M]
 
-/--
-Note that this lemma relies on the definitional equality `restrict_scalars R S M = M`,
-so usage may result in instance leakage.
-`restrict_scalars.add_equiv_map_smul` is the "hygienic" version.
--/
-lemma restrict_scalars_smul_def (c : R) (x : restrict_scalars R S M) :
-  c • x = ((algebra_map R S c) • x : M) := rfl
-
 @[simp] lemma restrict_scalars.add_equiv_map_smul (c : R) (x : restrict_scalars R S M) :
   restrict_scalars.add_equiv R S M (c • x)
   = (algebra_map R S c) • restrict_scalars.add_equiv R S M x :=
 rfl
 
+lemma restrict_scalars.smul_def (c : R) (x : restrict_scalars R S M) :
+  c • x = (restrict_scalars.add_equiv R S M).symm
+    (algebra_map R S c • restrict_scalars.add_equiv R S M x) :=
+rfl
+
 lemma restrict_scalars.add_equiv_symm_map_algebra_map_smul (r : R) (x : M) :
   (restrict_scalars.add_equiv R S M).symm (algebra_map R S r • x)
   = r • (restrict_scalars.add_equiv R S M).symm x :=

src/data/complex/module.lean

@@ -211,8 +211,7 @@ by rw [← finite_dimensional.finrank_mul_finrank ℝ ℂ E, complex.finrank_rea
 @[priority 900]
 instance star_module.complex_to_real {E : Type*} [add_comm_group E] [has_star E] [module ℂ E]
   [star_module ℂ E] : star_module ℝ E :=
-⟨λ r a, by rw [star_trivial r, restrict_scalars_smul_def, restrict_scalars_smul_def, star_smul,
-  complex.coe_algebra_map, complex.star_def, complex.conj_of_real]⟩
+⟨λ r a, by rw [←smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]⟩
 
 namespace complex