keep both versions

Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

@@ -118,18 +118,23 @@ theorem ofDirectSum_toDirectSum (x : TensorAlgebra R M) :
 #align tensor_algebra.of_direct_sum_to_direct_sum TensorAlgebra.ofDirectSum_toDirectSum
 
 @[simp]
-theorem mk_reindex_cast {n m : ℕ} (h : Fin n = Fin m) (x : (⨂[R]^n) M) :
+theorem mk_reindex_cast' {n m : ℕ} (h : Fin n = Fin m) (x : (⨂[R]^n) M) :
     GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m
     (PiTensorProduct.reindex R M (Equiv.cast h) x) =
     GradedMonoid.mk n x :=
   Eq.symm (PiTensorProduct.gradedMonoid_eq_of_reindex_cast (fin_injective h) rfl)
+
+theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) :
+    GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m
+    (PiTensorProduct.reindex R M (Equiv.cast <| congr_arg Fin h) x) =
+    GradedMonoid.mk n x := by simp
 #align tensor_algebra.mk_reindex_cast TensorAlgebra.mk_reindex_cast
 
 @[simp]
 theorem mk_reindex_fin_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) :
     GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m
     (PiTensorProduct.reindex R M (Fin.castIso h).toEquiv x) = GradedMonoid.mk n x := by
-  rw [Fin.castIso_to_equiv, mk_reindex_cast (h ▸ rfl)]
+  rw [Fin.castIso_to_equiv, mk_reindex_cast h]
 #align tensor_algebra.mk_reindex_fin_cast TensorAlgebra.mk_reindex_fin_cast
 
 /-- The product of tensor products made of a single vector is the same as a single product of