diff --git a/Mathlib/LinearAlgebra/TensorProduct/Map.lean b/Mathlib/LinearAlgebra/TensorProduct/Map.lean
index c2f23fa7984d96..ac9e7ae0a5aafc 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Map.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Map.lean
@@ -595,21 +595,29 @@ def rTensor (f : N ≃ₗ[R] P) : N ⊗[R] M ≃ₗ[R] P ⊗[R] M := TensorProdu
 
 variable (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (m : M) (n : N) (p : P) (x : M ⊗[R] N) (y : N ⊗[R] M)
 
+@[simp] theorem symm_lTensor : (f.lTensor M).symm = f.symm.lTensor M := rfl
+
+@[simp] theorem symm_rTensor : (f.rTensor M).symm = f.symm.rTensor M := rfl
+
 @[simp] theorem coe_lTensor : lTensor M f = (f : N →ₗ[R] P).lTensor M := rfl
 
-@[simp] theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl
+@[deprecated "use symm_lTensor and coe_lTensor" (since := "2026-07-04")]
+theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl
 
 @[simp] theorem coe_rTensor : rTensor M f = (f : N →ₗ[R] P).rTensor M := rfl
 
-@[simp] theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl
+@[deprecated "use symm_rTensor and coe_rTensor" (since := "2026-07-04")]
+theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl
 
 @[simp] theorem lTensor_tmul : f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n := rfl
 
-@[simp] theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl
+@[deprecated "use symm_lTensor and lTensor_tmul" (since := "2026-07-04")]
+theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl
 
 @[simp] theorem rTensor_tmul : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m := rfl
 
-@[simp] theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl
+@[deprecated "use symm_rTensor and rTensor_tmul" (since := "2026-07-04")]
+theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl
 
 lemma comm_trans_rTensor_trans_comm_eq (g : N ≃ₗ[R] P) :
     TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g :=
diff --git a/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean b/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
index 433e94131ac863..5b185e6f6f3b53 100644
--- a/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
+++ b/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
@@ -73,8 +73,8 @@ attribute [coassoc_simps] LinearMap.comp_id LinearMap.id_comp TensorProduct.map_
   LinearEquiv.coe_trans LinearEquiv.trans_symm
   LinearEquiv.refl_toLinearMap TensorProduct.toLinearMap_congr
   LinearEquiv.comp_symm LinearEquiv.symm_comp LinearEquiv.symm_symm
-  LinearEquiv.coe_lTensor LinearEquiv.coe_lTensor_symm
-  LinearEquiv.coe_rTensor LinearEquiv.coe_rTensor_symm
+  LinearEquiv.coe_lTensor LinearEquiv.symm_lTensor
+  LinearEquiv.coe_rTensor LinearEquiv.symm_rTensor
   IsCocomm.comm_comp_comul TensorProduct.AlgebraTensorModule.map_eq
   TensorProduct.AlgebraTensorModule.assoc_eq TensorProduct.AlgebraTensorModule.rightComm_eq
   TensorProduct.tensorTensorTensorComm TensorProduct.AlgebraTensorModule.tensorTensorTensorComm