-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
a :
  ∀ (x : M) (y : N) (z : P),
    Eq (α := M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              ((_root_.TensorProduct.map
                                      (↑(AlgebraTensorModule.assoc R S S M N P) :
                                        M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P))
                                      (↑(AlgebraTensorModule.assoc R S S M N P) :
                                        M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
                                    M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P) →ₗ[S]
                                      M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) ∘ₗ
                                  (comul : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P)) :
                                M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))) :
                          M →ₗ[S] N →ₗ[S] P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
                        (a : M) → N →ₗ[S] P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
                      x :
                    N →ₗ[S] P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
                  (a : N) → P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
                y :
              P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
            (a : P) → M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
          z :
        M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              (comul ∘ₗ
                                  (↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
                                M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))) :
                          M →ₗ[S] N →ₗ[S] P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
                        (a : M) → N →ₗ[S] P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
                      x :
                    N →ₗ[S] P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
                  (a : N) → P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
                y :
              P →ₗ[R] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
            (a : P) → M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
          z :
        M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
⊢ Eq (α := M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
    ((_root_.TensorProduct.map (↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P))
            (↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
          M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P) →ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) ∘ₗ
        (comul : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P)) :
      M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
    (comul ∘ₗ (↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
      M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))

Tactic:
ext x y z