chore: fix diamonds around R and C structures (#38451)

The following examples fail on master, work with the PR:
```lean
example : (Semiring.toNatAlgebra : Algebra ℕ ℂ) = Complex.instAlgebraOfReal := by
  with_reducible_and_instances rfl

example : (Ring.toIntAlgebra ℂ : Algebra ℤ ℂ) = Complex.instAlgebraOfReal := by
  with_reducible_and_instances rfl

example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by
  with_reducible_and_instances rfl

example : (instInnerProductSpaceRealComplex.toSMul : SMul ℝ ℂ) = Complex.instRCLike.toSMul := by
  with_reducible_and_instances rfl

example {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] : SMulCommClass ℂ ℝ F :=
  inferInstance
```

The PR makes a few algebra maps implicit-reducible. This is necessary to get rid of the diamonds as these maps show up in the instances. This has no noticeable performance impact: implicit-reducible only matters for instances, and there it tends to help unification.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -521,7 +521,7 @@ lemma convexOn_cfcₙ_of_convexOn_cfc {f : ℝ → ℝ} {s : Set A}
   refine convexOn_of_convexOn_inr_comp (fun _ => IsSelfAdjoint.cfcₙ) ?_
   have h₁ : inr (R := ℂ) ∘ (cfcₙ f) = fun x : A => ((cfcₙ f x : A) : A⁺¹) := rfl
   have h₂ : (fun x : A => ((cfcₙ f x : A) : A⁺¹))
-      = fun x : A => cfc f (x : A⁺¹) := by ext1; rw [real_cfcₙ_eq_cfc_inr ..]; rfl
+      = fun x : A => cfc f (x : A⁺¹) := by ext1; rw [real_cfcₙ_eq_cfc_inr ..]
   rw [h₁, h₂]
   have h₃ : ConvexOn ℝ (inrl ⁻¹' inrl '' s) ((cfc f) ∘ inrl) :=
     ConvexOn.comp_linearMap (g := inrl) hf

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -996,3 +996,7 @@ lemma isPosSemidef_inner : LinearMap.IsPosSemidef (innerₗ E) where
   isNonneg := isNonneg_inner
 
 end IsPosSemidef
+
+example : (instInnerProductSpaceRealComplex.toSMul : SMul ℝ ℂ) =
+    Complex.instRCLike.toSMul := by
+  with_reducible_and_instances rfl

Mathlib/Data/Complex/Basic.lean

@@ -77,7 +77,7 @@ theorem range_im : range im = univ :=
   im_surjective.range_eq
 
 /-- The natural inclusion of the real numbers into the complex numbers. -/
-@[coe]
+@[coe, implicit_reducible]
 def ofReal (r : ℝ) : ℂ :=
   ⟨r, 0⟩
 instance : Coe ℝ ℂ :=
@@ -197,7 +197,7 @@ instance : Sub ℂ :=
 /--
 `mulAux` is an auxiliary definition for defining multiplication and scalar multiplication on `ℂ`
 in such a way that `real_smul {x : ℝ} {z : ℂ} : x • z = x * z` holds definitionally.
-This makes sure that `Module.restrictScalars ℝ ℂ ℂ = Complex.module` definitionally.
+This makes sure that `Module.restrictScalars ℝ ℂ ℂ = Complex.instModule` definitionally.
 -/
 @[no_expose]
 def mulAux {R : Type*} [SMul R ℝ] (re : R) (im : ℝ) (z : ℂ) : ℂ :=
@@ -568,6 +568,7 @@ theorem add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ) :=
   Complex.ext_iff.2 <| by simp [two_mul, ofReal]
 
 /-- The coercion `ℝ → ℂ` as a `RingHom`. -/
+@[implicit_reducible]
 def ofRealHom : ℝ →+* ℂ where
   toFun x := (x : ℂ)
   map_one' := ofReal_one

Mathlib/Data/Int/Cast/Lemmas.lean

@@ -81,6 +81,7 @@ variable [NonAssocRing α]
 
 variable (α) in
 /-- `coe : ℤ → α` as a `RingHom`. -/
+@[implicit_reducible]
 def castRingHom : ℤ →+* α where
   toFun := Int.cast
   map_zero' := cast_zero

Mathlib/Data/Nat/Cast/Basic.lean

@@ -58,6 +58,7 @@ variable [NonAssocSemiring α]
 
 variable (α) in
 /-- `Nat.cast : ℕ → α` as a `RingHom` -/
+@[implicit_reducible]
 def castRingHom : ℕ →+* α :=
   { castAddMonoidHom α with toFun := Nat.cast, map_one' := cast_one, map_mul' := cast_mul }
 

Mathlib/LinearAlgebra/Complex/Module.lean

@@ -109,6 +109,15 @@ instance : StarModule ℝ ℂ :=
 theorem coe_algebraMap : (algebraMap ℝ ℂ : ℝ → ℂ) = ((↑) : ℝ → ℂ) :=
   rfl
 
+example : (Semiring.toNatAlgebra : Algebra ℕ ℂ) = Complex.instAlgebraOfReal := by
+  with_reducible_and_instances rfl
+
+example : (Ring.toIntAlgebra ℂ : Algebra ℤ ℂ) = Complex.instAlgebraOfReal := by
+  with_reducible_and_instances rfl
+
+example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by
+  with_reducible_and_instances rfl
+
 section
 
 variable {A : Type*} [Semiring A] [Algebra ℝ A]