diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
index bc98cbfd4fae12..d0595a460fb70d 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
@@ -133,12 +133,7 @@ noncomputable def tensorQuotientEquiv (n : Submodule R N) :
     (M ⊗[R] N) ⧸ (LinearMap.range (map (LinearMap.id : M →ₗ[R] M) n.subtype)) :=
   congr ((Submodule.quotEquivOfEqBot _ rfl).symm) (LinearEquiv.refl _ _) ≪≫ₗ
   quotientTensorQuotientEquiv (⊥ : Submodule R M) n ≪≫ₗ
-  Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _) (by
-    simp only [Submodule.map_sup]
-    erw [Submodule.map_id, Submodule.map_id]
-    simp only [sup_eq_right]
-    rw [range_map_eq_span_tmul, range_map_eq_span_tmul]
-    simp)
+  Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _) (by simp [range_map_eq_span_tmul])
 
 @[simp]
 lemma tensorQuotientEquiv_apply_mk_tmul (n : Submodule R N) (x : M) (y : N) :