fix batch 1

Mathlib/Algebra/Algebra/RestrictScalars.lean

@@ -7,9 +7,7 @@ module
 
 public import Mathlib.Algebra.Algebra.Tower
 public import Mathlib.Algebra.Algebra.TransferInstance
-public import Mathlib.Algebra.Group.TransferInstance
 public import Mathlib.Algebra.Module.TransferInstance
-public import Mathlib.Algebra.Ring.TransferInstance
 
 /-!
 
@@ -155,25 +153,29 @@ def toMSemilinearMap [AddCommMonoid M] [Module S M] :
   map_add' := by simp
   map_smul' := by simp [smul_toM]
 
-@[simps]
-def ofAddHom [AddCommMonoid M] [Module S M] :
-    M →+ RestrictScalars f M where
-  toFun := RestrictScalars.of f
-  map_add' := by simp
-  map_zero' := rfl
+instance {R : Type*} [NonUnitalRing R] : NonUnitalRing (RestrictScalars f R) :=
+  fast_instance% (RestrictScalars.toMEquiv f R).nonUnitalRing
 
 instance {R : Type*} [Semiring R] : Semiring (RestrictScalars f R) :=
   fast_instance% (RestrictScalars.toMEquiv f R).semiring
 
 instance {R : Type*} [Ring R] : Ring (RestrictScalars f R) :=
   fast_instance% (RestrictScalars.toMEquiv f R).ring
 
+instance {R : Type*} [NonUnitalCommRing R] : NonUnitalCommRing (RestrictScalars f R) :=
+  fast_instance% (RestrictScalars.toMEquiv f R).nonUnitalCommRing
+
 instance {R : Type*} [CommSemiring R] : CommSemiring (RestrictScalars f R) :=
   fast_instance% (RestrictScalars.toMEquiv f R).commSemiring
 
 instance {R : Type*} [CommRing R] : CommRing (RestrictScalars f R) :=
   fast_instance% (RestrictScalars.toMEquiv f R).commRing
 
+def nonUnitalRingEquiv {A : Type*} [NonUnitalRing A] : RestrictScalars f A ≃+* A where
+  __ := toMEquiv f A
+  map_mul' _ _ := rfl
+  map_add' _ _ := rfl
+
 /-- Tautological ring isomorphism `RestrictScalars R S A ≃+* A`. -/
 def ringEquiv {A : Type*} [Semiring A] : RestrictScalars f A ≃+* A where
   __ := toMAddEquiv f A

Mathlib/Algebra/Category/ModuleCat/Algebra.lean

@@ -45,19 +45,19 @@ variable {A : Type w} [Ring A] [Algebra k A]
 /-- Type synonym for considering a module over a `k`-algebra as a `k`-module. -/
 @[instance_reducible]
 def moduleOfAlgebraModule (M : ModuleCat.{v} A) : Module k M :=
-  Module.restrictScalars k A M
+  Module.compHom _ (algebraMap k A)
 
 attribute [scoped instance] ModuleCat.moduleOfAlgebraModule
 
 theorem isScalarTower_of_algebra_moduleCat (M : ModuleCat.{v} A) : IsScalarTower k A M :=
-  IsScalarTower.restrictScalars k A M
+  IsScalarTower.of_compHom _ _ _
 
 attribute [scoped instance] ModuleCat.isScalarTower_of_algebra_moduleCat
 
 -- We verify that the morphism spaces become `k`-modules.
 example (M N : ModuleCat.{v} A) : Module k (M ⟶ N) := inferInstance
 
 instance linearOverField : Linear k (ModuleCat.{v} A) where
-  homModule _ _ := inferInstance
+  homModule M N := inferInstance
 
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -701,9 +701,8 @@ def HomEquiv.toRestrictScalars {X : ModuleCat R} {Y : ModuleCat S}
     map_add' := fun _ _ => by dsimp; rw [tmul_add, map_add]
     map_smul' := fun r s => by
       dsimp
-      rw [RestrictScalars.smul_def, ← LinearMap.map_smul]
-      erw [tmul_smul]
-      congr }
+      rw [tmul_smul, ← LinearMap.map_smul]
+      rfl }
 
 set_option backward.isDefEq.respectTransparency false in
 -- Porting note: forced to break apart fromExtendScalars due to timeouts

Mathlib/Algebra/Lie/BaseChange.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Algebra.RestrictScalars
 public import Mathlib.Algebra.Lie.TensorProduct
+public import Mathlib.Algebra.Lie.TransferInstance
 
 /-!
 # Extension and restriction of scalars for Lie algebras and Lie modules
@@ -143,17 +144,18 @@ end ExtendScalars
 namespace RestrictScalars
 
 
-variable [h : LieRing L]
+variable [LieRing L]
 
-instance : LieRing (RestrictScalars R A L) :=
-  h
+instance [Semiring R] [Semiring A] (f : R →+* A) : LieRing (RestrictScalars f L) :=
+  fast_instance% (RestrictScalars.toMAddEquiv _ _).lieRing
 
 variable [CommRing A] [LieAlgebra A L]
 
-set_option backward.isDefEq.respectTransparency false in
-instance lieAlgebra [CommRing R] [Algebra R A] : LieAlgebra R (RestrictScalars R A L) where
-  lie_smul t x y := (lie_smul (algebraMap R A t) (RestrictScalars.addEquiv R A L x)
-    (RestrictScalars.addEquiv R A L y) :)
+instance lieAlgebra [CommRing R] [Algebra R A] : LieAlgebra R (RestrictScalars' R A L) where
+  lie_smul t x y := by rw [RestrictScalars.smul_def, RestrictScalars.smul_def,
+    AddEquiv.eq_symm_apply, (RestrictScalars.toMAddEquiv (algebraMap R A) L).bracket_def x y,
+    AddEquiv.apply_symm_apply, ← lie_smul, (RestrictScalars.toMAddEquiv
+    (algebraMap R A) L).bracket_def, AddEquiv.apply_symm_apply, AddEquiv.apply_symm_apply]
 
 end RestrictScalars
 

Mathlib/Analysis/Complex/Basic.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Analysis.Complex.Order
+public import Mathlib.Analysis.Normed.Module.RestrictScalars
 public import Mathlib.Analysis.RCLike.Basic
 public import Mathlib.Basic.Complex.BigOperators
 public import Mathlib.LinearAlgebra.Complex.Module

Mathlib/Analysis/Normed/Module/Basic.lean

@@ -420,133 +420,6 @@ instance (priority := 75) SubalgebraClass.toNormedAlgebra : NormedAlgebra 𝕜 s
 
 end SubalgebraClass
 
-section RestrictScalars
-
-section NormInstances
-
-instance [I : SeminormedAddCommGroup E] :
-    SeminormedAddCommGroup (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : NormedAddCommGroup E] :
-    NormedAddCommGroup (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : NonUnitalSeminormedRing E] :
-    NonUnitalSeminormedRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : NonUnitalNormedRing E] :
-    NonUnitalNormedRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : SeminormedRing E] :
-    SeminormedRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : NormedRing E] :
-    NormedRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : NonUnitalSeminormedCommRing E] :
-    NonUnitalSeminormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : NonUnitalNormedCommRing E] :
-    NonUnitalNormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : SeminormedCommRing E] :
-    SeminormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-instance [I : NormedCommRing E] :
-    NormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-end NormInstances
-
-section NormedSpace
-
-variable (𝕜 𝕜' E)
-variable [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
-  [SeminormedAddCommGroup E] [NormedSpace 𝕜' E]
-
-/-- Warning: This declaration should be used judiciously.
-Please consider using `IsScalarTower` instead.
-
-This definition allows the `RestrictScalars.normedSpace` instance to be put directly on `E`
-rather on `RestrictScalars 𝕜 𝕜' E`. This would be a very bad instance; both because `𝕜'` cannot be
-inferred, and because it is likely to create instance diamonds.
-
-See Note [reducible non-instances].
--/
-@[instance_reducible]
-def NormedSpace.restrictScalars : NormedSpace 𝕜 E :=
-  { Module.restrictScalars 𝕜 𝕜' E with
-    norm_smul_le := fun c x =>
-      (norm_smul_le (algebraMap 𝕜 𝕜' c) (_ : E)).trans_eq <| by rw [norm_algebraMap'] }
-
-theorem NormedSpace.restrictScalars_eq {E : Type*} [SeminormedAddCommGroup E]
-    [h : NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
-    NormedSpace.restrictScalars 𝕜 𝕜' E = h := by
-  ext
-  apply algebraMap_smul
-
-/-- If `E` is a normed space over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
-`RestrictScalars.module` is additionally a `NormedSpace`. -/
-instance RestrictScalars.normedSpace : NormedSpace 𝕜 (RestrictScalars 𝕜 𝕜' E) :=
-  fast_instance% NormedSpace.restrictScalars 𝕜 𝕜' E
-
--- If you think you need this, consider instead reproducing `RestrictScalars.lsmul`
--- appropriately modified here.
-/-- The action of the original `NormedField` on `RestrictScalars 𝕜 𝕜' E`.
-This is not an instance as it would be contrary to the purpose of `RestrictScalars`.
--/
-@[instance_reducible]
-def Module.RestrictScalars.normedSpaceOrig {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [NormedField 𝕜']
-    [SeminormedAddCommGroup E] [I : NormedSpace 𝕜' E] : NormedSpace 𝕜' (RestrictScalars 𝕜 𝕜' E) :=
-  I
-
-end NormedSpace
-
-section NormedAlgebra
-
-variable (𝕜 𝕜' E)
-variable [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
-  [SeminormedRing E] [NormedAlgebra 𝕜' E]
-
-/-- Warning: This declaration should be used judiciously.
-Please consider using `IsScalarTower` instead.
-
-This definition allows the `RestrictScalars.normedAlgebra` instance to be put directly on `E`
-rather on `RestrictScalars 𝕜 𝕜' E`. This would be a very bad instance; both because `𝕜'` cannot be
-inferred, and because it is likely to create instance diamonds.
-
-See Note [reducible non-instances].
--/
-@[instance_reducible]
-def NormedAlgebra.restrictScalars : NormedAlgebra 𝕜 E :=
-  { NormedSpace.restrictScalars 𝕜 𝕜' E, Algebra.restrictScalars 𝕜 𝕜' E with }
-
-/-- If `E` is a normed algebra over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
-`RestrictScalars.module` is additionally a `NormedAlgebra`. -/
-instance RestrictScalars.normedAlgebra : NormedAlgebra 𝕜 (RestrictScalars 𝕜 𝕜' E) :=
-  fast_instance% NormedAlgebra.restrictScalars 𝕜 𝕜' E
-
--- If you think you need this, consider instead reproducing `RestrictScalars.lsmul`
--- appropriately modified here.
-/-- The action of the original `NormedField` on `RestrictScalars 𝕜 𝕜' E`.
-This is not an instance as it would be contrary to the purpose of `RestrictScalars`.
--/
-@[instance_reducible]
-def Module.RestrictScalars.normedAlgebraOrig {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [NormedField 𝕜']
-    [SeminormedRing E] [I : NormedAlgebra 𝕜' E] : NormedAlgebra 𝕜' (RestrictScalars 𝕜 𝕜' E) :=
-  I
-end NormedAlgebra
-
-end RestrictScalars
-
 section Core
 /-!
 ### Structures for constructing new normed spaces

Mathlib/Analysis/Normed/Module/RestrictScalars.lean

@@ -0,0 +1,138 @@
+module
+
+public import Mathlib.Analysis.Normed.Module.TransferInstance
+public import Mathlib.Analysis.Normed.Ring.TransferInstance
+
+/-!
+-/
+
+@[expose] public section
+
+section RestrictScalars
+
+section NormInstances
+
+variable {𝕜 𝕜' E : Type*} [Semiring 𝕜] [Semiring 𝕜'] (f : 𝕜 →+* 𝕜')
+
+instance [SeminormedAddCommGroup E] :
+    SeminormedAddCommGroup (RestrictScalars f E) :=
+  fast_instance% (RestrictScalars.toMEquiv _ _).seminormedAddCommGroup
+
+instance [NormedAddCommGroup E] :
+    NormedAddCommGroup (RestrictScalars f E) :=
+  fast_instance% (RestrictScalars.toMEquiv _ _).normedAddCommGroup
+
+instance [NonUnitalSeminormedRing E] : NonUnitalSeminormedRing (RestrictScalars f E) :=
+  fast_instance% NonUnitalSeminormedRing.induced _ _ (RestrictScalars.nonUnitalRingEquiv f)
+
+instance [NonUnitalNormedRing E] : NonUnitalNormedRing (RestrictScalars f E) :=
+  fast_instance%NonUnitalNormedRing.induced _ _ _ (RestrictScalars.nonUnitalRingEquiv f).injective
+
+instance [SeminormedRing E] : SeminormedRing (RestrictScalars f E) :=
+  fast_instance% (RestrictScalars.toMEquiv _ _).seminormedRing
+
+instance [NormedRing E] : NormedRing (RestrictScalars f E) :=
+  fast_instance% (RestrictScalars.toMEquiv _ _).normedRing
+
+instance [NonUnitalSeminormedCommRing E] : NonUnitalSeminormedCommRing (RestrictScalars f E) :=
+  fast_instance% NonUnitalSeminormedCommRing.induced _ _ (RestrictScalars.nonUnitalRingEquiv f)
+
+instance [NonUnitalNormedCommRing E] : NonUnitalNormedCommRing (RestrictScalars f E) :=
+  fast_instance% NonUnitalNormedCommRing.induced _ _ _
+    (RestrictScalars.nonUnitalRingEquiv f).injective
+
+instance [SeminormedCommRing E] : SeminormedCommRing (RestrictScalars f E) :=
+  fast_instance% (RestrictScalars.toMEquiv _ _).seminormedCommRing
+
+instance [NormedCommRing E] : NormedCommRing (RestrictScalars f E) :=
+  fast_instance% (RestrictScalars.toMEquiv _ _).normedCommRing
+
+end NormInstances
+
+section NormedSpace
+
+variable (𝕜 𝕜' E : Type*)
+variable [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+  [SeminormedAddCommGroup E] [NormedSpace 𝕜' E]
+
+/-- Warning: This declaration should be used judiciously.
+Please consider using `IsScalarTower` instead.
+
+This definition allows the `RestrictScalars.normedSpace` instance to be put directly on `E`
+rather on `RestrictScalars 𝕜 𝕜' E`. This would be a very bad instance; both because `𝕜'` cannot be
+inferred, and because it is likely to create instance diamonds.
+
+See Note [reducible non-instances].
+-/
+@[instance_reducible]
+def NormedSpace.restrictScalars : NormedSpace 𝕜 E :=
+  { Module.compHom E (algebraMap 𝕜 𝕜') with
+    norm_smul_le := fun c x =>
+      (norm_smul_le (algebraMap 𝕜 𝕜' c) (_ : E)).trans_eq <| by rw [norm_algebraMap'] }
+
+theorem NormedSpace.restrictScalars_eq {E : Type*} [SeminormedAddCommGroup E]
+    [h : NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
+    NormedSpace.restrictScalars 𝕜 𝕜' E = h := by
+  ext
+  apply algebraMap_smul
+
+/-- If `E` is a normed space over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
+`RestrictScalars.module` is additionally a `NormedSpace`. -/
+instance RestrictScalars.normedSpace : NormedSpace 𝕜 (RestrictScalars' 𝕜 𝕜' E) where
+  norm_smul_le c x :=
+    (norm_smul_le (algebraMap 𝕜 𝕜' c) x.toM).trans_eq (by rw [norm_algebraMap']; rfl)
+
+-- If you think you need this, consider instead reproducing `RestrictScalars.lsmul`
+-- appropriately modified here.
+variable {𝕜 𝕜' E} in
+/-- The action of the original `NormedField` on `RestrictScalars 𝕜 𝕜' E`.
+This is not an instance as it would be contrary to the purpose of `RestrictScalars`.
+-/
+@[instance_reducible]
+def Module.RestrictScalars.normedSpaceOrig : NormedSpace 𝕜' (RestrictScalars' 𝕜 𝕜' E) :=
+  { RestrictScalars.moduleOrig (algebraMap 𝕜 𝕜') E with
+    norm_smul_le c x:= norm_smul_le c x.toM }
+
+end NormedSpace
+
+section NormedAlgebra
+
+variable (𝕜 𝕜' E)
+variable [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+  [SeminormedRing E] [NormedAlgebra 𝕜' E]
+
+/-- Warning: This declaration should be used judiciously.
+Please consider using `IsScalarTower` instead.
+
+This definition allows the `RestrictScalars.normedAlgebra` instance to be put directly on `E`
+rather on `RestrictScalars 𝕜 𝕜' E`. This would be a very bad instance; both because `𝕜'` cannot be
+inferred, and because it is likely to create instance diamonds.
+
+See Note [reducible non-instances].
+-/
+@[instance_reducible]
+def NormedAlgebra.restrictScalars : NormedAlgebra 𝕜 E :=
+  { NormedSpace.restrictScalars 𝕜 𝕜' E with
+    algebraMap := (algebraMap 𝕜' E).comp (algebraMap 𝕜 𝕜')
+    commutes' _ _ := by simp [Algebra.commute_algebraMap_left _ _|>.eq]
+    smul_def' r x := show (algebraMap 𝕜 𝕜' r) • x = _ from Algebra.smul_def _ _}
+
+/-- If `E` is a normed algebra over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
+`RestrictScalars.module` is additionally a `NormedAlgebra`. -/
+instance RestrictScalars.normedAlgebra : NormedAlgebra 𝕜 (RestrictScalars' 𝕜 𝕜' E) where
+  norm_smul_le c x := (norm_smul_le (algebraMap 𝕜 𝕜' c) x.toM).trans_eq <| by
+    rw [norm_algebraMap']; rfl
+
+-- If you think you need this, consider instead reproducing `RestrictScalars.lsmul`
+-- appropriately modified here.
+variable {𝕜 𝕜' E} in
+/-- The action of the original `NormedField` on `RestrictScalars 𝕜 𝕜' E`.
+This is not an instance as it would be contrary to the purpose of `RestrictScalars`.
+-/
+@[instance_reducible]
+def Module.RestrictScalars.normedAlgebraOrig : NormedAlgebra 𝕜' (RestrictScalars' 𝕜 𝕜' E) :=
+  { Module.RestrictScalars.normedSpaceOrig, RestrictScalars.algebraOrig 𝕜 𝕜' E with}
+
+end NormedAlgebra
+
+end RestrictScalars