diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
index 9355d09c2992a..f24b144938533 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -288,7 +288,7 @@ theorem ι_ne_one [Nontrivial R] (x : M) : ι R x ≠ 1 := by
 theorem ι_range_disjoint_one :
     Disjoint (LinearMap.range (ι R : M →ₗ[R] TensorAlgebra R M))
       (1 : Submodule R (TensorAlgebra R M)) := by
-  rw [Submodule.disjoint_def]
+  rw [Submodule.disjoint_def, Submodule.one_eq_range]
   rintro _ ⟨x, hx⟩ ⟨r, rfl⟩
   rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx
   rw [hx.2, map_zero]
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
index 838f15025ec00..074c5389f0f01 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
@@ -121,8 +121,9 @@ theorem mulMap'_surjective : Function.Surjective (mulMap' M N) := by
 `i(R) ⊗[R] N →ₗ[R] N` induced by multiplication in `S`, here `i : R → S` is the structure map.
 This is promoted to an isomorphism of `R`-modules as `Submodule.lTensorOne`. Use that instead. -/
 def lTensorOne' : (⊥ : Subalgebra R S) ⊗[R] N →ₗ[R] N :=
-  show (1 : Submodule R S) ⊗[R] N →ₗ[R] N from
-    (LinearEquiv.ofEq _ _ (by rw [mulMap_range, one_mul])).toLinearMap ∘ₗ (mulMap _ N).rangeRestrict
+  show Subalgebra.toSubmodule ⊥ ⊗[R] N →ₗ[R] N from
+    (LinearEquiv.ofEq _ _ (by rw [Algebra.toSubmodule_bot, mulMap_range, one_mul])).toLinearMap ∘ₗ
+      (mulMap _ N).rangeRestrict
 
 variable {N} in
 @[simp]
@@ -130,7 +131,7 @@ theorem lTensorOne'_tmul (y : R) (n : N) :
     N.lTensorOne' (algebraMap R _ y ⊗ₜ[R] n) = y • n := Subtype.val_injective <| by
   simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
     LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def]
-  exact mulMap_tmul 1 N _ _
+  exact mulMap_tmul _ N _ _
 
 variable {N} in
 @[simp]
@@ -163,15 +164,17 @@ variable {N} in
 @[simp]
 theorem lTensorOne_symm_apply (n : N) : N.lTensorOne.symm n = 1 ⊗ₜ[R] n := rfl
 
-theorem mulMap_one_left_eq : mulMap 1 N = N.subtype ∘ₗ N.lTensorOne.toLinearMap :=
+theorem mulMap_one_left_eq :
+    mulMap (Subalgebra.toSubmodule ⊥) N = N.subtype ∘ₗ N.lTensorOne.toLinearMap :=
   TensorProduct.ext' fun _ _ ↦ rfl
 
 /-- If `M` is a submodule in an algebra `S` over `R`, there is the natural `R`-linear map
 `M ⊗[R] i(R) →ₗ[R] M` induced by multiplication in `S`, here `i : R → S` is the structure map.
 This is promoted to an isomorphism of `R`-modules as `Submodule.rTensorOne`. Use that instead. -/
 def rTensorOne' : M ⊗[R] (⊥ : Subalgebra R S) →ₗ[R] M :=
-  show M ⊗[R] (1 : Submodule R S) →ₗ[R] M from
-    (LinearEquiv.ofEq _ _ (by rw [mulMap_range, mul_one])).toLinearMap ∘ₗ (mulMap M _).rangeRestrict
+  show M ⊗[R] Subalgebra.toSubmodule ⊥ →ₗ[R] M from
+    (LinearEquiv.ofEq _ _ (by rw [Algebra.toSubmodule_bot, mulMap_range, mul_one])).toLinearMap ∘ₗ
+      (mulMap M _).rangeRestrict
 
 variable {M} in
 @[simp]
@@ -180,7 +183,7 @@ theorem rTensorOne'_tmul (y : R) (m : M) :
   simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
     LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul]
   rw [Algebra.smul_def, Algebra.commutes]
-  exact mulMap_tmul M 1 _ _
+  exact mulMap_tmul M _ _ _
 
 variable {M} in
 @[simp]
@@ -213,7 +216,8 @@ variable {M} in
 @[simp]
 theorem rTensorOne_symm_apply (m : M) : M.rTensorOne.symm m = m ⊗ₜ[R] 1 := rfl
 
-theorem mulMap_one_right_eq : mulMap M 1 = M.subtype ∘ₗ M.rTensorOne.toLinearMap :=
+theorem mulMap_one_right_eq :
+    mulMap M (Subalgebra.toSubmodule ⊥) = M.subtype ∘ₗ M.rTensorOne.toLinearMap :=
   TensorProduct.ext' fun _ _ ↦ rfl
 
 @[simp]
diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean
index 0039e1437e417..afeae5a28a460 100644
--- a/Mathlib/RingTheory/Finiteness.lean
+++ b/Mathlib/RingTheory/Finiteness.lean
@@ -432,8 +432,8 @@ section Mul
 variable {R : Type*} {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
 variable {M N : Submodule R A}
 
-theorem FG.mul (hm : M.FG) (hn : N.FG) : (M * N).FG :=
-  hm.map₂ _ hn
+theorem FG.mul (hm : M.FG) (hn : N.FG) : (M * N).FG := by
+  rw [mul_eq_map₂]; exact hm.map₂ _ hn
 
 theorem FG.pow (h : M.FG) (n : ℕ) : (M ^ n).FG :=
   Nat.recOn n ⟨{1}, by simp [one_eq_span]⟩ fun n ih => by simpa [pow_succ] using ih.mul h