-- 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 : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[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)
H :
  ∀ (a : (i : Fin na) → M) (b : (i : Fin nb) → M) (c : (i : Fin nc) → M),
    Eq (α := ⨂[R]^(na + (nb + nc)) M)
      ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin nc) ↦ M)
              ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin nb) ↦ M)
                    ((lhs.compMultilinearMap (M₁ := fun (i : Fin na) ↦ M) (tprod R (s := fun (i : Fin na) ↦ M)) :
                        (a : (i : Fin na) → M) → ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                      a)
                    (tprod R (s := fun (i : Fin nb) ↦ M)) :
                  (a : (i : Fin nb) → M) → ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                b)
              (tprod R (s := fun (i : Fin nc) ↦ M)) :
            (a : (i : Fin nc) → M) → ⨂[R]^(na + (nb + nc)) M)
          c :
        ⨂[R]^(na + (nb + nc)) M)
      ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin nc) ↦ M)
              ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin nb) ↦ M)
                    ((rhs.compMultilinearMap (M₁ := fun (i : Fin na) ↦ M) (tprod R (s := fun (i : Fin na) ↦ M)) :
                        (a : (i : Fin na) → M) → ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                      a)
                    (tprod R (s := fun (i : Fin nb) ↦ M)) :
                  (a : (i : Fin nb) → M) → ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                b)
              (tprod R (s := fun (i : Fin nc) ↦ M)) :
            (a : (i : Fin nc) → M) → ⨂[R]^(na + (nb + nc)) M)
          c :
        ⨂[R]^(na + (nb + nc)) M)
⊢ lhs = rhs

Tactic:
ext a b c