diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean
index a3f69ec0d98aa1..7b8c9cbf236c55 100644
--- a/Mathlib/RingTheory/TensorProduct.lean
+++ b/Mathlib/RingTheory/TensorProduct.lean
@@ -158,41 +158,16 @@ variable {B : Type v₂} [Semiring B] [Algebra R B]
 ### The `R`-algebra structure on `A ⊗[R] B`
 -/
 
-
-/-- (Implementation detail)
-The multiplication map on `A ⊗[R] B`,
-for a fixed pure tensor in the first argument,
-as an `R`-linear map.
--/
-def mulAux (a₁ : A) (b₁ : B) : A ⊗[R] B →ₗ[R] A ⊗[R] B :=
-  TensorProduct.map (LinearMap.mulLeft R a₁) (LinearMap.mulLeft R b₁)
-#align algebra.tensor_product.mul_aux Algebra.TensorProduct.mulAux
-
-@[simp]
-theorem mulAux_apply (a₁ a₂ : A) (b₁ b₂ : B) :
-    (mulAux a₁ b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) :=
-  rfl
-#align algebra.tensor_product.mul_aux_apply Algebra.TensorProduct.mulAux_apply
+#noalign algebra.tensor_product.mul_aux
+#noalign algebra.tensor_product.mul_aux_apply
 
 /-- (Implementation detail)
 The multiplication map on `A ⊗[R] B`,
 as an `R`-bilinear map.
 -/
 def mul : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B :=
-  TensorProduct.lift <|
-    LinearMap.mk₂ R mulAux
-      (fun x₁ x₂ y =>
-        TensorProduct.ext' fun x' y' => by
-          simp only [mulAux_apply, LinearMap.add_apply, add_mul, add_tmul])
-      (fun c x y =>
-        TensorProduct.ext' fun x' y' => by
-          simp only [mulAux_apply, LinearMap.smul_apply, smul_tmul', smul_mul_assoc])
-      (fun x y₁ y₂ =>
-        TensorProduct.ext' fun x' y' => by
-          simp only [mulAux_apply, LinearMap.add_apply, add_mul, tmul_add])
-      fun c x y =>
-      TensorProduct.ext' fun x' y' => by
-        simp only [mulAux_apply, LinearMap.smul_apply, smul_tmul, smul_tmul', smul_mul_assoc]
+  TensorProduct.homTensorHomMap R A B A B
+    ∘ₗ TensorProduct.map (LinearMap.mul R A) (LinearMap.mul R B)
 #align algebra.tensor_product.mul Algebra.TensorProduct.mul
 
 @[simp]