-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (1 + n)
      ((PiTensorProduct.tprod R (s := fun (a : Fin (1 + n)) ↦ M) :
          (a : (i : Fin (1 + n)) → M) → ⨂[R] (i : Fin (1 + n)), M)
        (Fin.append (fun (x : Fin 1) ↦ x₀) x)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x)))
have refine_2 : Eq (α :=
  ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
        (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
          ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
              (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
            (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))))
    M)
  ((TensorPower.cast R M sorry :
        (a :
            ⨂[R]^(GradedMonoid.mk (1 + n)
                    ((PiTensorProduct.tprod R : (a : (i : Fin (1 + n)) → M) → ⨂[R] (i : Fin (1 + n)), M)
                      (Fin.append (fun (x : Fin 1) ↦ x₀) x))).fst
              M) →
          ⨂[R]^(GradedMonoid.mk (n + 1)
                  ((PiTensorProduct.tprod R : (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
                    (Fin.cons x₀ x))).fst
            M)
      (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
        (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (1 + n)
          ((PiTensorProduct.tprod R (s := fun (a : Fin (1 + n)) ↦ M) :
              (a : (i : Fin (1 + n)) → M) → ⨂[R] (i : Fin (1 + n)), M)
            (Fin.append (fun (x : Fin 1) ↦ x₀) x)))) :
    ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
            ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
                (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
              (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))))
      M)
  (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
      (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
        ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
            (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
          (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))) :
    ⨂[R] (x :
      Fin
        (Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
            ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
                (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
              (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))))),
      M)
Tactic: refine TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) ?_