-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
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))
refine_2 :
  Eq (α := ⨂[R]^(n + 1) M)
    ((TensorPower.cast R M ⋯ : (a : ⨂[R]^(1 + n) M) → ⨂[R]^(n + 1) M)
        ((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]^(n + 1) M)
    ((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] (i : Fin (n + 1)), M)
⊢ 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 ⋯ :
          (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:
dsimp only [GradedMonoid.mk]

Premises used: GradedMonoid.mk