-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
⊢ 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)
have 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 sorry) :
        (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)
Tactic: rw [← LinearEquiv.eq_symm_apply]