chore(LinearAlgebra/TensorProduct/Quotient): remove an erw (#38417)

- simplifies the proof passed to `Submodule.Quotient.equiv` in `tensorQuotientEquiv` to a single `simp [range_map_eq_span_tmul]`

Extracted from #38415

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

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) :