chore: fix diamonds around R and C structures

Mathlib/Algebra/Algebra/Defs.lean

@@ -88,24 +88,17 @@ assert_not_exists Field Finset Module.End
 
 universe u v w u₁ v₁
 
-section Prio
-
 /-- An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.
 
 See the implementation notes in this file for discussion of the details of this definition.
 -/
 class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A where
-  /-- Embedding `R →+* A` given by `Algebra` structure.
-  Use `algebraMap` from the root namespace instead. -/
-  protected algebraMap : R →+* A
+  /-- Embedding `R →+* A` given by `Algebra` structure. -/
+  algebraMap (R) (A) : R →+* A
   commutes' : ∀ r x, algebraMap r * x = x * algebraMap r
   smul_def' : ∀ r x, r • x = algebraMap r * x
 
-end Prio
-
-/-- Embedding `R →+* A` given by `Algebra` structure. -/
-def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* A :=
-  Algebra.algebraMap
+export Algebra (algebraMap)
 
 theorem Algebra.subsingleton (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A]
     [Subsingleton R] : Subsingleton A :=

Mathlib/Algebra/Algebra/Pi.lean

@@ -252,6 +252,6 @@ end AlgEquiv
 /-- Apply an algebra map component-wise along a vector. -/
 def Pi.algebraMap (ι R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
     (ι → R) →ₗ[R] (ι → A) where
-  toFun v := _root_.algebraMap R A ∘ v
+  toFun v := Algebra.algebraMap R A ∘ v
   map_add' v w := by simp
   map_smul' t v := by ext; simp [Algebra.smul_def]

Mathlib/Algebra/Ring/Hom/Defs.lean

@@ -534,8 +534,10 @@ theorem coe_monoidHom_id : (id α : α →* α) = MonoidHom.id α :=
 variable {_ : NonAssocSemiring γ}
 
 /-- Composition of ring homomorphisms is a ring homomorphism. -/
+@[implicit_reducible]
 def comp (g : β →+* γ) (f : α →+* β) : α →+* γ :=
-  { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with toFun := g ∘ f, map_one' := by simp }
+  { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with
+    toFun := fun x ↦ g (f x), map_one' := by simp }
 
 /-- Composition of semiring homomorphisms is associative. -/
 theorem comp_assoc {δ} {_ : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) :

Mathlib/Algebra/Star/Subalgebra.lean

@@ -515,7 +515,7 @@ theorem _root_.Subalgebra.starClosure_eq_adjoin (S : Subalgebra R A) :
 @[elab_as_elim]
 theorem adjoin_induction {s : Set A} {p : (x : A) → x ∈ adjoin R s → Prop}
     (mem : ∀ (x) (h : x ∈ s), p x (subset_adjoin R s h))
-    (algebraMap : ∀ r, p (_root_.algebraMap R _ r) (_root_.algebraMap_mem _ r))
+    (algebraMap : ∀ r, p (Algebra.algebraMap R _ r) (algebraMap_mem _ r))
     (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
     (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
     (star : ∀ x hx, p x hx → p (star x) (star_mem hx))
@@ -531,11 +531,11 @@ theorem adjoin_induction₂ {s : Set A} {p : (x y : A) → x ∈ adjoin R s →
     (mem_mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_adjoin R s hx)
       (subset_adjoin R s hy))
     (algebraMap_both : ∀ r₁ r₂, p (algebraMap R A r₁) (algebraMap R A r₂)
-      (_root_.algebraMap_mem _ r₁) (_root_.algebraMap_mem _ r₂))
-    (algebraMap_left : ∀ (r) (x) (hx : x ∈ s), p (algebraMap R A r) x (_root_.algebraMap_mem _ r)
+      (algebraMap_mem _ r₁) (algebraMap_mem _ r₂))
+    (algebraMap_left : ∀ (r) (x) (hx : x ∈ s), p (algebraMap R A r) x (algebraMap_mem _ r)
       (subset_adjoin R s hx))
     (algebraMap_right : ∀ (r) (x) (hx : x ∈ s), p x (algebraMap R A r) (subset_adjoin R s hx)
-      (_root_.algebraMap_mem _ r))
+      (algebraMap_mem _ r))
     (add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz)
     (add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz))
     (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)

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/Analysis/Normed/Algebra/GelfandMazur.lean

@@ -262,7 +262,7 @@ variable {F : Type*} [NormedRing F] [NormedAlgebra ℝ F]
 
 /- A (private) abbreviation introduced for conciseness below.
 We will show that for every `x : F`, `φ x` takes the value zero. -/
-private abbrev φ (x : F) (u : ℝ × ℝ) : F := x ^ 2 - u.1 • x + algebraMap ℝ F u.2
+private noncomputable abbrev φ (x : F) (u : ℝ × ℝ) : F := x ^ 2 - u.1 • x + algebraMap ℝ F u.2
 
 private lemma continuous_φ (x : F) : Continuous (φ x) := by fun_prop
 

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/FieldTheory/IntermediateField/Adjoin/Defs.lean

@@ -484,7 +484,7 @@ theorem adjoin_induction {s : Set E} {p : ∀ x ∈ adjoin F s, Prop}
     {x} (h : x ∈ adjoin F s) : p x h :=
   Subfield.closure_induction
     (fun x hx ↦ Or.casesOn hx (fun ⟨x, hx⟩ ↦ hx ▸ algebraMap x) (mem x))
-    (by simp_rw [← (_root_.algebraMap F E).map_one]; exact algebraMap 1) add
+    (by simp_rw [← (Algebra.algebraMap F E).map_one]; exact algebraMap 1) add
     (fun x _ h ↦ by
       simp_rw [← neg_one_smul F x, Algebra.smul_def]; exact mul _ _ _ _ (algebraMap _) h) inv mul h
 

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -191,7 +191,7 @@ theorem induction {C : CliffordAlgebra Q → Prop}
       mul_mem' := @mul
       add_mem' := @add
       algebraMap_mem' := algebraMap }
-  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = _root_.algebraMap _ _ (Q m) } :=
+  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = Algebra.algebraMap _ _ (Q m) } :=
     ⟨(CliffordAlgebra.ι Q).codRestrict (Subalgebra.toSubmodule s) ι,
       fun m => Subtype.ext <| ι_sq_scalar Q m⟩
   -- the mapping through the subalgebra is the identity

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]

Mathlib/RingTheory/Localization/Integral.lean

@@ -257,7 +257,7 @@ theorem IsLocalization.scaleRoots_commonDenom_mem_lifts (p : Rₘ[X])
 theorem IsIntegral.exists_multiple_integral_of_isLocalization [Algebra Rₘ S] [IsScalarTower R Rₘ S]
     (x : S) (hx : IsIntegral Rₘ x) : ∃ m : M, IsIntegral R (m • x) := by
   rcases subsingleton_or_nontrivial Rₘ with _ | nontriv
-  · haveI := (_root_.algebraMap Rₘ S).codomain_trivial
+  · haveI := (algebraMap Rₘ S).codomain_trivial
     exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
   obtain ⟨p, hp₁, hp₂⟩ := hx
   -- Porting note: obtain doesn't support side goals

Mathlib/RingTheory/OrderOfVanishing/Basic.lean

@@ -182,7 +182,7 @@ lemma ord_le_ord_mul (a : R) (x : R) : ord R x ≤ ord R (a * x) := by
     let g : (R ⧸ Ideal.span {a * x}) →ₗ[R] (R ⧸ Ideal.span {x}) := Submodule.factor this
     refine Module.length_le_of_surjective (Submodule.factor this) (Submodule.factor_surjective this)
   rw [Ideal.span_singleton_le_span_singleton]
-  exact Dvd.intro_left (Algebra.algebraMap a) rfl
+  exact Dvd.intro_left (algebraMap R R a) rfl
 
 lemma ord_le_ord_of_dvd {a x : R} (h : a ∣ x) : ord R a ≤ ord R x := by
   obtain ⟨b, rfl⟩ := h

Mathlib/Tactic/Module.lean

@@ -202,7 +202,7 @@ variable (R)
 commutative semiring, by applying to each `S`-component the algebra-map from `S` into a specified
 `S`-algebra `R`. -/
 def algebraMap [CommSemiring S] [Semiring R] [Algebra S R] (l : NF S M) : NF R M :=
-  l.map (fun ⟨s, x⟩ ↦ (_root_.algebraMap S R s, x))
+  l.map (fun ⟨s, x⟩ ↦ (Algebra.algebraMap S R s, x))
 
 theorem eval_algebraMap [CommSemiring S] [Semiring R] [Algebra S R] [AddMonoid M] [SMul S M]
     [MulAction R M] [IsScalarTower S R M] (l : NF S M) :

Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean

@@ -96,6 +96,11 @@ notation:25 E' " →Lᵤ[" R ", " 𝔖 "] " F => UniformConvergenceCLM (RingHom.
 
 namespace UniformConvergenceCLM
 
+/-- Reinterpret `f : E →SL[σ] F` as an element of `E →SLᵤ[σ, 𝔖] F`. -/
+@[implicit_reducible]
+def ofFun [TopologicalSpace F] (𝔖 : Set (Set E)) : (E →SL[σ] F) ≃ (E →SLᵤ[σ, 𝔖] F) :=
+  ⟨fun x => x, fun x => x, fun _ => rfl, fun _ => rfl⟩
+
 instance instFunLike [TopologicalSpace F] (𝔖 : Set (Set E)) :
     FunLike (E →SLᵤ[σ, 𝔖] F) E F :=
   inferInstanceAs <| FunLike (E →SL[σ] F) E F
@@ -215,8 +220,9 @@ theorem t2Space [TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F]
 
 instance instDistribMulAction (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
     [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
-    DistribMulAction M (E →SLᵤ[σ, 𝔖] F) :=
-  inferInstanceAs <| DistribMulAction M (E →SL[σ] F)
+    DistribMulAction M (E →SLᵤ[σ, 𝔖] F) where
+  smul c f := (ofFun σ F 𝔖) (c • (ofFun σ F 𝔖).symm f)
+  __ : DistribMulAction M (E →SLᵤ[σ, 𝔖] F) := inferInstanceAs <| DistribMulAction M (E →SL[σ] F)
 
 @[simp]
 theorem smul_apply {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]

Mathlib/Topology/Algebra/StarSubalgebra.lean

@@ -237,7 +237,7 @@ lemma le_centralizer_centralizer [T2Space A] (x : A) :
 theorem induction_on {x y : A}
     (hy : y ∈ elemental R x) {P : (u : A) → u ∈ elemental R x → Prop}
     (self : P x (self_mem R x)) (star_self : P (star x) (star_self_mem R x))
-    (algebraMap : ∀ r, P (algebraMap R A r) (_root_.algebraMap_mem _ r))
+    (algebraMap : ∀ r, P (Algebra.algebraMap R A r) (algebraMap_mem _ r))
     (add : ∀ u hu v hv, P u hu → P v hv → P (u + v) (add_mem hu hv))
     (mul : ∀ u hu v hv, P u hu → P v hv → P (u * v) (mul_mem hu hv))
     (closure : ∀ s : Set A, (hs : s ⊆ elemental R x) → (∀ u, (hu : u ∈ s) →