-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
rw :
  Eq (α :=
    ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
      M)
    (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
        (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
          ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))) :
      ⨂[R] (x :
        Fin
          (Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))),
        M)
    ((LinearEquiv.symm (cast R M ⋯) :
          (a :
              ⨂[R]^(GradedMonoid.mk (0 + 0)
                      (GradedMonoid.GMul.mul (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)
                        (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) s))).fst
                M) →
            ⨂[R]^(GradedMonoid.mk 0
                    (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) (r * s))).fst
              M)
        (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
            (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s)))) :
      ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
        M)
⊢ Eq (α :=
    ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
            (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s))))
      M)
    ((cast R M ⋯ :
          (a :
              ⨂[R]^(GradedMonoid.mk 0
                      (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) (r * s))).fst
                M) →
            ⨂[R]^(GradedMonoid.mk (0 + 0)
                    (GradedMonoid.GMul.mul (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)
                      (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) s))).fst
              M)
        (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s)))) :
      ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
              (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
                ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
                ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s))))
        M)
    (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
        (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s))) :
      ⨂[R] (x :
        Fin
          (Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
              (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
                ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
                ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s))))),
        M)

Tactic:
rw [← LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply