-- 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
na nb nc : ℕ
a_1 : ⨂[R]^na M
b_1 : ⨂[R]^nb M
c_1 : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun (n m : ℕ) ↦
    LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M))
      (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M)
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
        (a : ⨂[R]^(na + nb) M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →
          (⨂[R]^nb M →ₗ[R] ⨂[R]^(na + nb) M) →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
      (LinearMap.compr₂ (mul (na + nb) nc) (↑e : ⨂[R]^(na + nb + nc) M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    Eq (α := ⨂[R]^(na + (nb + nc)) M)
      ((((((lhs : (a : ⨂[R]^na M) → ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) a :
                    ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
                  (a : ⨂[R]^nb M) → ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                b :
              ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
            (a : ⨂[R]^nc M) → ⨂[R]^(na + (nb + nc)) M)
          c :
        ⨂[R]^(na + (nb + nc)) M)
      ((e : (a : ⨂[R]^(na + nb + nc) M) → ⨂[R]^(na + (nb + nc)) M)
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (na + nb) _
            (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ a b) c) :
        ⨂[R]^(na + (nb + nc)) M)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  LinearMap.flip
    ((((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
              (a :
                  (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →ₗ[R]
                    ⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →
                (⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →ₗ[R]
                  ⨂[R]^nb M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
            (↑LinearMap.lflip :
              (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →ₗ[R]
                ⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
          (⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →ₗ[R]
            ⨂[R]^nb M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
        (a : ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →
          ⨂[R]^nb M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
            (a : ⨂[R]^(nb + nc) M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →
              (⨂[R]^nc M →ₗ[R] ⨂[R]^(nb + nc) M) →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (LinearMap.flip (mul na (nb + nc))) ∘ₗ
        mul nb nc))
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    Eq (α := ⨂[R]^(na + (nb + nc)) M)
      ((((((rhs : (a : ⨂[R]^na M) → ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) a :
                    ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
                  (a : ⨂[R]^nb M) → ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                b :
              ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
            (a : ⨂[R]^nc M) → ⨂[R]^(na + (nb + nc)) M)
          c :
        ⨂[R]^(na + (nb + nc)) M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ (nb + nc) a
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ b c) :
        ⨂[R]^(na + (nb + nc)) M)
a : (i : Fin na) → M
b : (i : Fin nb) → M
c : (i : Fin nc) → M
H : ∀ (j : Fin (na + (nb + nc))), (Fin.append (Fin.append a b) c ∘ Fin.cast ⋯) j = Fin.append a (Fin.append b c) j
⊢ Eq (α := ⨂[R]^(na + (nb + nc)) M)
    ((tprod R (s := fun (a : Fin (na + (nb + nc))) ↦ M) :
          (a : (i : Fin (na + (nb + nc))) → M) → ⨂[R] (i : Fin (na + (nb + nc))), M)
        (Fin.append (Fin.append a b) c ∘ Fin.cast ⋯) :
      ⨂[R] (i : Fin (na + (nb + nc))), M)
    ((tprod R (s := fun (a : Fin (na + (nb + nc))) ↦ M) :
          (a : (i : Fin (na + (nb + nc))) → M) → ⨂[R] (i : Fin (na + (nb + nc))), M)
        (Fin.append a (Fin.append b c)) :
      ⨂[R] (i : Fin (na + (nb + nc))), M)

Tactic:
congr 1 with j