From 0bb21f22eb318816f6b13ef99c6059a2b966536e Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 22 May 2026 12:22:40 +0000
Subject: [PATCH 1/3] some api

---
 Mathlib/LinearAlgebra/TensorProduct/Tower.lean |  3 +++
 Mathlib/RingTheory/TensorProduct/Basic.lean    | 18 ++++++++++--------
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
index 7607ff2d6e0b81..c71de9452136f5 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@@ -176,6 +176,9 @@ nonrec def mk (A M N : Type*) [Semiring A]
 
 variable {R A B M N P Q}
 
+/-- The heterobasic version of `mk` coincides with the regular version. -/
+lemma mk_eq : mk R R M N = TensorProduct.mk R M N := rfl
+
 /-- Heterobasic version of `TensorProduct.map` -/
 def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q :=
   lift <|
diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean
index e7ec44de33ee7f..0f1d5cc41adee0 100644
--- a/Mathlib/RingTheory/TensorProduct/Basic.lean
+++ b/Mathlib/RingTheory/TensorProduct/Basic.lean
@@ -269,11 +269,9 @@ theorem tmul_pow (a : A) (b : B) (k : ℕ) : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[
   | succ k ih => simp [pow_succ, ih]
 
 /-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/
-@[simps]
+@[simps!]
 def includeLeftRingHom : A →+* A ⊗[R] B where
-  toFun a := a ⊗ₜ 1
-  map_zero' := by simp
-  map_add' := by simp [add_tmul]
+  __ := (AlgebraTensorModule.mk R R A B).flip 1 |>.toAddMonoidHom
   map_one' := rfl
   map_mul' := by simp
 
@@ -317,19 +315,23 @@ theorem includeLeft_apply [SMulCommClass R S A] (a : A) :
     (includeLeft : A →ₐ[S] A ⊗[R] B) a = a ⊗ₜ 1 :=
   rfl
 
+@[simp] theorem toLinearMap_includeLeft [SMulCommClass R S A] :
+    (includeLeft : A →ₐ[S] A ⊗[R] B).toLinearMap = (AlgebraTensorModule.mk R S A B).flip 1 := rfl
+
 /-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`. -/
 def includeRight : B →ₐ[R] A ⊗[R] B where
-  toFun b := 1 ⊗ₜ b
-  map_zero' := by simp
-  map_add' := by simp [tmul_add]
+  __ := AlgebraTensorModule.mk R R A B 1 |>.toAddMonoidHom
   map_one' := rfl
   map_mul' := by simp
-  commutes' r := by simp only [algebraMap_apply']
+  commutes' r := by simp [algebraMap_eq_smul_one', smul_tmul]
 
 @[simp]
 theorem includeRight_apply (b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b :=
   rfl
 
+@[simp] theorem toLinearMap_includeRight :
+    (includeRight : B →ₐ[R] A ⊗[R] B).toLinearMap = AlgebraTensorModule.mk R R A B 1 := rfl
+
 theorem includeLeftRingHom_comp_algebraMap :
     (includeLeftRingHom.comp (algebraMap R A) : R →+* A ⊗[R] B) =
       includeRight.toRingHom.comp (algebraMap R B) := by

From 03e39e9b58b86f64d2d8e51922944bf6bc362c10 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 22 May 2026 13:51:51 +0000
Subject: [PATCH 2/3] fix

---
 Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
index a4ca029c1952f5..26e9a4cdaf9855 100644
--- a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
+++ b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
@@ -54,7 +54,7 @@ lemma includeLeftSubRight_apply (s : S) : includeLeftSubRight R S s = s ⊗ₜ[R
 lemma includeLeftSubRight_zero_of_mem_range {s : S} (hs : s ∈ Set.range ⇑(algebraMap R S)) :
     includeLeftSubRight R S s = 0 := by
   obtain ⟨_, hr⟩ := Set.mem_range.mp hs
-  simp [includeLeftSubRight, ← hr]
+  simp [includeLeftSubRight, ← hr, algebraMap_eq_smul_one]
 
 /-- `includeLeftSubRight R S` vanishes at `algebraMap R S r`. -/
 lemma includeLeftSubRight_algebraMap_zero (r : R) :

From 6363bbf8cfa6f16af6878665c682d018de999924 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 22 May 2026 13:58:47 +0000
Subject: [PATCH 3/3] tiny change

---
 Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
index 26e9a4cdaf9855..781cd5e014c7d1 100644
--- a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
+++ b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
@@ -54,7 +54,7 @@ lemma includeLeftSubRight_apply (s : S) : includeLeftSubRight R S s = s ⊗ₜ[R
 lemma includeLeftSubRight_zero_of_mem_range {s : S} (hs : s ∈ Set.range ⇑(algebraMap R S)) :
     includeLeftSubRight R S s = 0 := by
   obtain ⟨_, hr⟩ := Set.mem_range.mp hs
-  simp [includeLeftSubRight, ← hr, algebraMap_eq_smul_one]
+  simp [← hr, algebraMap_eq_smul_one]
 
 /-- `includeLeftSubRight R S` vanishes at `algebraMap R S r`. -/
 lemma includeLeftSubRight_algebraMap_zero (r : R) :