From 4624c4e7773ad9bdebbe9942e1a86d6a2d37b64f Mon Sep 17 00:00:00 2001
From: Whysoserioushah <yx3021@ic.ac.uk>
Date: Sun, 25 Oct 2026 10:05:51 +0000
Subject: [PATCH 1/2] fix batch 1

---
 Mathlib/Algebra/Algebra/RestrictScalars.lean  |  18 ++-
 .../Algebra/Category/ModuleCat/Algebra.lean   |   6 +-
 .../Category/ModuleCat/ChangeOfRings.lean     |   5 +-
 Mathlib/Algebra/Lie/BaseChange.lean           |  16 +-
 Mathlib/Analysis/Complex/Basic.lean           |   1 +
 Mathlib/Analysis/Normed/Module/Basic.lean     | 127 ----------------
 .../Normed/Module/RestrictScalars.lean        | 138 ++++++++++++++++++
 .../Normed/Ring/TransferInstance.lean         |  10 ++
 Mathlib/LinearAlgebra/Complex/Module.lean     |   6 +-
 Mathlib/RepresentationTheory/Basic.lean       |  16 +-
 .../Subrepresentation.lean                    |  23 +--
 Mathlib/RingTheory/Flat/Basic.lean            |  22 ++-
 Mathlib/RingTheory/IsTensorProduct.lean       |   4 +-
 Mathlib/RingTheory/TensorProduct/Maps.lean    |   4 +-
 14 files changed, 215 insertions(+), 181 deletions(-)
 create mode 100644 Mathlib/Analysis/Normed/Module/RestrictScalars.lean

diff --git a/Mathlib/Algebra/Algebra/RestrictScalars.lean b/Mathlib/Algebra/Algebra/RestrictScalars.lean
index 5b288612acc2b2..7f23f41c0a5384 100644
--- a/Mathlib/Algebra/Algebra/RestrictScalars.lean
+++ b/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,12 +153,8 @@ 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
@@ -168,12 +162,20 @@ instance {R : Type*} [Semiring R] : Semiring (RestrictScalars f R) :=
 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
diff --git a/Mathlib/Algebra/Category/ModuleCat/Algebra.lean b/Mathlib/Algebra/Category/ModuleCat/Algebra.lean
index 0de46ddcccc707..c2fada600beea4 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Algebra.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Algebra.lean
@@ -45,12 +45,12 @@ 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
 
@@ -58,6 +58,6 @@ attribute [scoped instance] ModuleCat.isScalarTower_of_algebra_moduleCat
 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
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index 60286c158b2d89..b3f9293b730a41 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/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
diff --git a/Mathlib/Algebra/Lie/BaseChange.lean b/Mathlib/Algebra/Lie/BaseChange.lean
index ad444d30364f5c..91d17820d2e1c1 100644
--- a/Mathlib/Algebra/Lie/BaseChange.lean
+++ b/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
 
diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean
index 007723b2bd5cb8..3bf16d3c51af7e 100644
--- a/Mathlib/Analysis/Complex/Basic.lean
+++ b/Mathlib/Analysis/Complex/Basic.lean
@@ -13,6 +13,7 @@ public import Mathlib.Topology.Algebra.Algebra.Equiv
 public import Mathlib.Topology.Algebra.InfiniteSum.Module
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
 public import Mathlib.Topology.Instances.RealVectorSpace
+public import Mathlib.Analysis.Normed.Module.RestrictScalars
 
 /-!
 
diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean
index 54ce650fb8ea64..e2e21ea0365d2b 100644
--- a/Mathlib/Analysis/Normed/Module/Basic.lean
+++ b/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
diff --git a/Mathlib/Analysis/Normed/Module/RestrictScalars.lean b/Mathlib/Analysis/Normed/Module/RestrictScalars.lean
new file mode 100644
index 00000000000000..9aaddf3886d5bc
--- /dev/null
+++ b/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
diff --git a/Mathlib/Analysis/Normed/Ring/TransferInstance.lean b/Mathlib/Analysis/Normed/Ring/TransferInstance.lean
index 6517496129a953..a4a3b579fcfb03 100644
--- a/Mathlib/Analysis/Normed/Ring/TransferInstance.lean
+++ b/Mathlib/Analysis/Normed/Ring/TransferInstance.lean
@@ -34,4 +34,14 @@ protected abbrev normedRing [NormedRing β] (e : α ≃ β) : NormedRing α :=
   letI := e.ring
   .induced α β e.ringEquiv e.injective
 
+protected abbrev seminormedCommRing [SeminormedCommRing β] (e : α ≃ β) :
+    SeminormedCommRing α :=
+  letI := e.commRing
+  .induced α β e.ringEquiv
+
+protected abbrev normedCommRing [NormedCommRing β] (e : α ≃ β) :
+    NormedCommRing α :=
+  letI := e.commRing
+  .induced α β e.ringEquiv e.injective
+
 end Equiv
diff --git a/Mathlib/LinearAlgebra/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean
index 57b2542a8bb518..69ba08b09968e3 100644
--- a/Mathlib/LinearAlgebra/Complex/Module.lean
+++ b/Mathlib/LinearAlgebra/Complex/Module.lean
@@ -116,7 +116,7 @@ example : (Semiring.toNatAlgebra : Algebra ℕ ℂ) = Complex.instAlgebraOfReal
 example : (Ring.toIntAlgebra ℂ : Algebra ℤ ℂ) = Complex.instAlgebraOfReal := by
   with_reducible_and_instances rfl
 
-example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by
+example : Module.compHom ℂ (algebraMap ℝ ℂ) = Complex.instModule := by
   with_reducible_and_instances rfl
 
 section
@@ -168,13 +168,13 @@ end Complex
 vector space. -/
 instance (priority := 900) Module.complexToReal (E : Type*) [AddCommGroup E] [Module ℂ E] :
     Module ℝ E :=
-  .restrictScalars ℝ ℂ E
+  Module.compHom _ (algebraMap ℝ ℂ)
 
 /-- Register as an instance (with low priority) the fact that a complex algebra is also a real
 algebra. -/
 instance (priority := 900) Algebra.complexToReal {A : Type*} [Semiring A] [Algebra ℂ A] :
     Algebra ℝ A :=
-  .restrictScalars ℝ ℂ A
+  Algebra.compHom _ (algebraMap ℝ ℂ)
 
 -- try to make sure we're not introducing diamonds but we will need
 -- `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906
diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean
index 33f106f497af7e..8df46a306108da 100644
--- a/Mathlib/RepresentationTheory/Basic.lean
+++ b/Mathlib/RepresentationTheory/Basic.lean
@@ -201,7 +201,7 @@ variable (M : Type*) [AddCommMonoid M] [Module k[G] M]
 Note that the representation is built on `restrictScalars k k[G] M`,
 rather than on `M` itself.
 -/
-noncomputable def ofModule : Representation k G (RestrictScalars k k[G] M) :=
+noncomputable def ofModule : Representation k G (RestrictScalars' k k[G] M) :=
   (MonoidAlgebra.lift k _ G).symm (RestrictScalars.lsmul k k[G] M)
 
 /-!
@@ -224,9 +224,9 @@ we have `Module k[G] (restrictScalars k k[G] M)`.
 
 @[simp]
 theorem ofModule_asAlgebraHom_apply_apply (r : k[G])
-    (m : RestrictScalars k k[G] M) :
+    (m : RestrictScalars' k k[G] M) :
     ((ofModule M).asAlgebraHom r) m =
-      (RestrictScalars.addEquiv _ _ _).symm (r • RestrictScalars.addEquiv _ _ _ m) := by
+      (RestrictScalars.toMAddEquiv _ _).symm (r • RestrictScalars.toMAddEquiv _ _ m) := by
   apply MonoidAlgebra.induction_on r
   · intro g
     simp only [one_smul, MonoidAlgebra.lift_symm_apply, MonoidAlgebra.of_apply,
@@ -238,16 +238,16 @@ theorem ofModule_asAlgebraHom_apply_apply (r : k[G])
     simp only [w, map_smul, LinearMap.smul_apply, RestrictScalars.addEquiv_symm_map_smul_smul]
 
 @[simp]
-theorem ofModule_asModule_act (g : G) (x : RestrictScalars k k[G] ρ.asModule) :
+theorem ofModule_asModule_act (g : G) (x : RestrictScalars' k k[G] ρ.asModule) :
     ofModule ρ.asModule g x =
-      (RestrictScalars.addEquiv _ _ _).symm
-        (ρ.asModuleEquiv.symm (ρ g (ρ.asModuleEquiv (RestrictScalars.addEquiv _ _ _ x)))) := by
+      (RestrictScalars.toMAddEquiv _ _).symm
+        (ρ.asModuleEquiv.symm (ρ g (ρ.asModuleEquiv (RestrictScalars.toMAddEquiv _ _ x)))) := by
   dsimp [ofModule, RestrictScalars.lsmul_apply_apply]
   simp
 
 theorem smul_ofModule_asModule (r : k[G]) (m : (ofModule M).asModule) :
-    (RestrictScalars.addEquiv k _ _) ((ofModule M).asModuleEquiv (r • m)) =
-      r • (RestrictScalars.addEquiv k _ _) ((ofModule M).asModuleEquiv (G := G) m) := by
+    (RestrictScalars.toMAddEquiv _ _) ((ofModule M).asModuleEquiv (k := k) (r • m)) =
+      r • (RestrictScalars.toMAddEquiv _ _) ((ofModule M).asModuleEquiv (G := G) m) := by
   dsimp
   simp only [AddEquiv.apply_symm_apply, ofModule_asAlgebraHom_apply_apply]
 
diff --git a/Mathlib/RepresentationTheory/Subrepresentation.lean b/Mathlib/RepresentationTheory/Subrepresentation.lean
index 3cacdae7928f40..41d4c2c966baca 100644
--- a/Mathlib/RepresentationTheory/Subrepresentation.lean
+++ b/Mathlib/RepresentationTheory/Subrepresentation.lean
@@ -143,18 +143,21 @@ lemma mem_asSubmodule_iff {σ : Subrepresentation ρ} {v : W} : v ∈ asSubmodul
 
 /-- A subrepresentation of `ofModule M` can be thought of as an `A[G]` submodule of `M`.
 -/
-def asSubmodule' (σ : Subrepresentation (Representation.ofModule (k := A) (G := G) M)) :
-    Submodule A[G] M where
-  __ := σ.toSubmodule
+noncomputable def asSubmodule' (σ : Subrepresentation
+    (Representation.ofModule (k := A) (G := G) M)) : Submodule A[G] M where
+  __ := σ.toSubmodule.toAddSubmonoid.map (RestrictScalars.toMAddEquiv (algebraMap A A[G]) _)
   smul_mem' c m hm := by
     induction c using MonoidAlgebra.induction_linear with
-    | zero => rw [zero_smul]; exact σ.toSubmodule.zero_mem'
-    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
+    | zero => simp [zero_smul]
+    | add x y hx hy => simpa [-AddSubmonoid.mem_map, add_smul] using add_mem hx hy
     | single g a =>
       rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]
-      exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
-        simpa [Representation.ofModule, RestrictScalars.lsmul] using! σ.apply_mem_toSubmodule g hm
+      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup]
+      obtain ⟨x, hx, rfl⟩ := hm
+      exact AddSubmonoid.mem_map.mpr ⟨a • Representation.ofModule M g x,
+        σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hx), rfl⟩
 
+#exit
 @[simp]
 lemma mem_asSubmodule'_iff {σ : Subrepresentation (Representation.ofModule (k := A) (G := G) M)}
     {m : M} : m ∈ asSubmodule' σ ↔ m ∈ σ := by rfl
@@ -206,8 +209,8 @@ def submoduleSubrepresentationOrderIso : Submodule A[G] M ≃o
     Subrepresentation (Representation.ofModule (k := A) (G := G) M) where
   toFun := ofSubmodule
   invFun := asSubmodule'
-  left_inv N := rfl
-  right_inv σ := rfl
-  map_rel_iff' := by rfl
+  left_inv N := sorry
+  right_inv σ := sorry
+  map_rel_iff' := sorry
 
 end Subrepresentation
diff --git a/Mathlib/RingTheory/Flat/Basic.lean b/Mathlib/RingTheory/Flat/Basic.lean
index 6ec99a8bf40d3b..25604a7d9cdf51 100644
--- a/Mathlib/RingTheory/Flat/Basic.lean
+++ b/Mathlib/RingTheory/Flat/Basic.lean
@@ -231,15 +231,21 @@ instance of_projective [Projective R M] : Flat R M :=
 
 instance of_free [Free R M] : Flat R M := inferInstance
 
-instance {S} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M]
+instance {S : Type w} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M]
     [Flat S M] [Flat R N] : Flat S (M ⊗[R] N) :=
-  iff_rTensor_injectiveₛ.mpr fun P _ _ I ↦ by
-    let := RestrictScalars.moduleOrig R S P
-    change Submodule S (RestrictScalars R S P) at I
-    change Function.Injective (rTensor _ I.subtype)
-    simpa [AlgebraTensorModule.rTensor_tensor] using!
-      rTensor_preserves_injective_linearMap (.restrictScalars R <| I.subtype.rTensor M)
-      (rTensor_preserves_injective_linearMap _ I.injective_subtype)
+  iff_rTensor_preserves_injective_linearMapₛ.mpr fun (P P' : Type w) _ _ _ _ f hf ↦ by
+    let := RestrictScalars.moduleOrig (algebraMap R S) P
+    let := RestrictScalars.moduleOrig (algebraMap R S) P'
+    let e := (RestrictScalars.toMAddEquiv (algebraMap R S) P).linearEquiv S
+    let e' := (RestrictScalars.toMAddEquiv (algebraMap R S) P').linearEquiv S
+    let g := e'.symm.toLinearMap ∘ₗ f ∘ₗ e.toLinearMap
+    have : Injective (g.rTensor (M ⊗[R] N)) := by
+      simpa [AlgebraTensorModule.rTensor_tensor] using!
+        rTensor_preserves_injective_linearMap (.restrictScalars R <| g.rTensor M)
+          (rTensor_preserves_injective_linearMap _ (e'.symm.injective.comp (hf.comp e.injective)))
+    have hf' : f = e'.toLinearMap ∘ₗ g ∘ₗ e.symm.toLinearMap := by ext; simp [g]
+    rw [hf', rTensor_comp, rTensor_comp]
+    exact (e'.rTensor _).injective.comp (this.comp (e.symm.rTensor _).injective)
 
 example [Flat R M] [Flat R N] : Flat R (M ⊗[R] N) := inferInstance
 
diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
index b14705894aa57f..cf25047e588154 100644
--- a/Mathlib/RingTheory/IsTensorProduct.lean
+++ b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -557,8 +557,8 @@ lemma IsBaseChange.of_comp {f : M →ₗ[R] N} (hf : IsBaseChange S f) {h : N 
     IsBaseChange T h := by
   apply IsBaseChange.of_lift_unique
   intro Q _ _ _ _ r
-  let : Module R Q := .restrictScalars R S Q
-  have : IsScalarTower R S Q := .restrictScalars R S Q
+  let : Module R Q := Module.compHom Q (algebraMap R S)
+  have : IsScalarTower R S Q := .of_compHom _ _ _
   have : IsScalarTower R T Q := IsScalarTower.of_algebraMap_smul fun r x ↦ by
     simp [IsScalarTower.algebraMap_apply R S T]
   let r' : M →ₗ[R] Q := r ∘ₗ f
diff --git a/Mathlib/RingTheory/TensorProduct/Maps.lean b/Mathlib/RingTheory/TensorProduct/Maps.lean
index 6bf9efc709c37a..9aecd93a24fde5 100644
--- a/Mathlib/RingTheory/TensorProduct/Maps.lean
+++ b/Mathlib/RingTheory/TensorProduct/Maps.lean
@@ -85,8 +85,8 @@ lemma _root_.LinearMap.map_mul_of_map_mul_tmul {f : A ⊗[R] B →ₗ[S] C}
     (x y : A ⊗[R] B) : f (x * y) = f x * f y :=
   f.map_mul_iff.2 (by
     -- these instances are needed by the statement of `ext`, but not by the current definition.
-    let : Algebra R C := .restrictScalars R S C
-    let : IsScalarTower R S C := .restrictScalars R S C
+    let : Algebra R C := Algebra.compHom C (algebraMap R S)
+    let : IsScalarTower R S C := IsScalarTower.of_compHom _ _ _
     ext
     dsimp
     exact hf _ _ _ _) x y

From 4db3c114d3a766638dfd2763ab92d894533d2778 Mon Sep 17 00:00:00 2001
From: Whysoserioushah <yx3021@ic.ac.uk>
Date: Sun, 25 Oct 2026 11:33:02 +0000
Subject: [PATCH 2/2] a bit more

---
 Mathlib/Analysis/Complex/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean
index 3bf16d3c51af7e..6ab2b1a2ce71ca 100644
--- a/Mathlib/Analysis/Complex/Basic.lean
+++ b/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
@@ -13,7 +14,6 @@ public import Mathlib.Topology.Algebra.Algebra.Equiv
 public import Mathlib.Topology.Algebra.InfiniteSum.Module
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
 public import Mathlib.Topology.Instances.RealVectorSpace
-public import Mathlib.Analysis.Normed.Module.RestrictScalars
 
 /-!