With less bundling and more implicits, it looks like we can get somew…

…here!

TODO: do we really need to remove all that bundling or are implicits enough?

Mathlib/Algebra/Algebra/Equiv.lean

@@ -59,9 +59,7 @@ namespace AlgEquivClass
 instance (priority := 100) toAlgHomClass (F R A B : Type*) [CommSemiring R] [Semiring A]
     [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B] [h : AlgEquivClass F R A B] :
     AlgHomClass F R A B :=
-  { h with
-    map_zero := map_zero
-    map_one := map_one }
+  { h with }
 #align alg_equiv_class.to_alg_hom_class AlgEquivClass.toAlgHomClass
 
 instance (priority := 100) toLinearEquivClass (F R A B : Type*) [CommSemiring R]

Mathlib/Algebra/Algebra/Hom.lean

@@ -50,7 +50,7 @@ notation:25 A " →ₐ[" R "] " B => AlgHom R A B
 from `A` to `B`.  -/
 class AlgHomClass (F : Type*) (R : outParam (Type*)) (A : outParam (Type*))
   (B : outParam (Type*)) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
-  [Algebra R B] [NDFunLike F A B] extends RingHomClass F A B : Prop where
+  [Algebra R B] [NDFunLike F A B] [RingHomClass F A B] : Prop where
   commutes : ∀ (f : F) (r : R), f (algebraMap R A r) = algebraMap R B r
 #align alg_hom_class AlgHomClass
 
@@ -66,7 +66,8 @@ variable {R : Type*} {A : Type*} {B : Type*} [CommSemiring R] [Semiring A] [Semi
   [Algebra R A] [Algebra R B] [NDFunLike F A B]
 
 -- see Note [lower instance priority]
-instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass F R A B :=
+instance (priority := 100) linearMapClass [RingHomClass F A B] [AlgHomClass F R A B] :
+    LinearMapClass F R A B :=
   { ‹AlgHomClass F R A B› with
     map_smulₛₗ := fun f r x => by
       simp only [Algebra.smul_def, map_mul, commutes, RingHom.id_apply] }
@@ -76,12 +77,14 @@ instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass
 /-- Turn an element of a type `F` satisfying `AlgHomClass F α β` into an actual
 `AlgHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
 @[coe]
-def toAlgHom {F : Type*} [NDFunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B :=
+def toAlgHom {F : Type*} [NDFunLike F A B] [RingHomClass F A B] [AlgHomClass F R A B]
+    (f : F) : A →ₐ[R] B :=
   { (f : A →+* B) with
       toFun := f
       commutes' := AlgHomClass.commutes f }
 
-instance coeTC {F : Type*} [NDFunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
+instance coeTC {F : Type*} [NDFunLike F A B] [RingHomClass F A B] [AlgHomClass F R A B] :
+    CoeTC F (A →ₐ[R] B) :=
   ⟨AlgHomClass.toAlgHom⟩
 #align alg_hom_class.alg_hom.has_coe_t AlgHomClass.coeTC
 
@@ -107,12 +110,14 @@ instance funLike : NDFunLike (A →ₐ[R] B) A B where
     rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
     congr
 
--- Porting note: This instance is moved.
-instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where
+instance ringHomClass : RingHomClass (A →ₐ[R] B) A B where
   map_add f := f.map_add'
   map_zero f := f.map_zero'
   map_mul f := f.map_mul'
   map_one f := f.map_one'
+
+-- Porting note: This instance is moved.
+instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where
   commutes f := f.commutes'
 #align alg_hom.alg_hom_class AlgHom.algHomClass
 
@@ -123,7 +128,8 @@ def Simps.apply {R : Type u} {α : Type v} {β : Type w} [CommSemiring R]
 initialize_simps_projections AlgHom (toFun → apply)
 
 @[simp]
-protected theorem coe_coe {F : Type*} [NDFunLike F A B] [AlgHomClass F R A B] (f : F) :
+protected theorem coe_coe {F : Type*} [NDFunLike F A B] [RingHomClass F A B] [AlgHomClass F R A B]
+    (f : F) :
     ⇑(f : A →ₐ[R] B) = f :=
   rfl
 #align alg_hom.coe_coe AlgHom.coe_coe

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -66,10 +66,12 @@ attribute [nolint docBlame] NonUnitalAlgHom.toMulHom
 
 /-- `NonUnitalAlgHomClass F R A B` asserts `F` is a type of bundled algebra homomorphisms
 from `A` to `B`.  -/
-class NonUnitalAlgHomClass (F : Type*) (R : outParam (Type*)) (A B : Type*)
-  [Monoid R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B]
-  [DistribMulAction R A] [DistribMulAction R B] [NDFunLike F A B]
-  extends DistribMulActionHomClass F R A B, MulHomClass F A B : Prop
+class NonUnitalAlgHomClass (F : Type*) (R A B : outParam Type*)
+  {_ : outParam <| Monoid R} {_ : outParam <| NonUnitalNonAssocSemiring A}
+  {_ : outParam <| NonUnitalNonAssocSemiring B}
+  [DistribMulAction R A] [DistribMulAction R B] [NDFunLike F A B] [AddMonoidHomClass F A B]
+  [MulHomClass F A B]
+  extends DistribMulActionHomClass F R A B : Prop
 #align non_unital_alg_hom_class NonUnitalAlgHomClass
 
 -- Porting note: commented out, not dangerous
@@ -82,6 +84,7 @@ namespace NonUnitalAlgHomClass
 instance (priority := 100) toNonUnitalRingHomClass {F R A B : Type*}
     [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
     [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NDFunLike F A B]
+    [AddMonoidHomClass F A B] [MulHomClass F A B]
     [NonUnitalAlgHomClass F R A B] : NonUnitalRingHomClass F A B :=
   { ‹NonUnitalAlgHomClass F R A B› with }
 #align non_unital_alg_hom_class.non_unital_alg_hom_class.to_non_unital_ring_hom_class NonUnitalAlgHomClass.toNonUnitalRingHomClass
@@ -90,7 +93,11 @@ variable [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A]
   [NonUnitalNonAssocSemiring B] [Module R B]
 
 -- see Note [lower instance priority]
-instance (priority := 100) {F : Type*} [NDFunLike F A B] [NonUnitalAlgHomClass F R A B] :
+instance (priority := 100) {F R A B : Type*}
+    {_ : Semiring R} {_ : NonUnitalSemiring A} {_ : NonUnitalSemiring B}
+    [Module R A] [Module R B]
+    [NDFunLike F A B] [AddMonoidHomClass F A B]
+    [MulHomClass F A B] [NonUnitalAlgHomClass F R A B] :
     LinearMapClass F R A B :=
   { ‹NonUnitalAlgHomClass F R A B› with map_smulₛₗ := map_smul }
 
@@ -99,13 +106,14 @@ instance (priority := 100) {F : Type*} [NDFunLike F A B] [NonUnitalAlgHomClass F
 @[coe]
 def toNonUnitalAlgHom {F R A B : Type*} [Monoid R] [NonUnitalNonAssocSemiring A]
     [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NDFunLike F A B]
-    [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] B :=
+    [AddMonoidHomClass F A B] [MulHomClass F A B] [NonUnitalAlgHomClass F R A B]
+    (f : F) : A →ₙₐ[R] B :=
   { (f : A →ₙ+* B) with
     map_smul' := map_smul f }
 
 instance {F R A B : Type*} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
     [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
-    [NDFunLike F A B] [NonUnitalAlgHomClass F R A B] :
+    [NDFunLike F A B] [AddMonoidHomClass F A B] [MulHomClass F A B] [NonUnitalAlgHomClass F R A B] :
     CoeTC F (A →ₙₐ[R] B) :=
   ⟨toNonUnitalAlgHom⟩
 
@@ -142,7 +150,8 @@ initialize_simps_projections NonUnitalAlgHom
   (toDistribMulActionHom_toMulActionHom_toFun → apply, -toDistribMulActionHom)
 
 @[simp]
-protected theorem coe_coe {F : Type*} [NDFunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) :
+protected theorem coe_coe {F : Type*} [NDFunLike F A B] [AddMonoidHomClass F A B]
+    [MulHomClass F A B] [NonUnitalAlgHomClass F R A B] (f : F) :
     ⇑(f : A →ₙₐ[R] B) = f :=
   rfl
 #align non_unital_alg_hom.coe_coe NonUnitalAlgHom.coe_coe
@@ -156,13 +165,19 @@ instance : NDFunLike (A →ₙₐ[R] B) A B
   coe f := f.toFun
   coe_injective' := coe_injective
 
-instance : NonUnitalAlgHomClass (A →ₙₐ[R] B) R A B
+instance : AddMonoidHomClass (A →ₙₐ[R] B) A B
     where
-  map_smul f := f.map_smul'
   map_add f := f.map_add'
   map_zero f := f.map_zero'
+
+instance : MulHomClass (A →ₙₐ[R] B) A B
+    where
   map_mul f := f.map_mul'
 
+instance : NonUnitalAlgHomClass (A →ₙₐ[R] B) R A B
+    where
+  map_smul f := f.map_smul'
+
 @[ext]
 theorem ext {f g : A →ₙₐ[R] B} (h : ∀ x, f x = g x) : f = g :=
   coe_injective <| funext h
@@ -439,7 +454,7 @@ variable {R A B} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
   [Algebra R B]
 
 -- see Note [lower instance priority]
-instance (priority := 100) [NDFunLike F A B] [AlgHomClass F R A B] :
+instance (priority := 100) [NDFunLike F A B] [RingHomClass F A B] [AlgHomClass F R A B] :
     NonUnitalAlgHomClass F R A B :=
   { ‹AlgHomClass F R A B› with map_smul := map_smul }
 

Mathlib/Algebra/Algebra/Operations.lean

@@ -93,7 +93,7 @@ theorem le_one_toAddSubmonoid : 1 ≤ (1 : Submodule R A).toAddSubmonoid := by
 #align submodule.le_one_to_add_submonoid Submodule.le_one_toAddSubmonoid
 
 theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) :=
-  LinearMap.mem_range_self _ _
+  LinearMap.mem_range_self (Algebra.linearMap R A) _
 #align submodule.algebra_map_mem Submodule.algebraMap_mem
 
 @[simp]