-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
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)))
have a : Eq (α := 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))) :
        (a : M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P)) → M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
      (((AlgebraTensorModule.tensorTensorTensorComm R S R S (M ⊗[S] N) (M ⊗[S] N) P P :
            M ⊗[S] N ⊗[S] (M ⊗[S] N) ⊗[R] (P ⊗[R] P) ≃ₗ[S] M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P)) :
          (a : M ⊗[S] N ⊗[S] (M ⊗[S] N) ⊗[R] (P ⊗[R] P)) → M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P))
        (((AlgebraTensorModule.tensorTensorTensorComm S S S S M M N N :
                TensorProduct.{u_6, u_7, u_8} S (M ⊗[S] M) (N ⊗[S] N) ≃ₗ[S] M ⊗[S] N ⊗[S] (M ⊗[S] N)) :
              (a : M ⊗[S] M ⊗[S] (N ⊗[S] N)) → M ⊗[S] N ⊗[S] (M ⊗[S] N))
            ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[S] (comul : (a : N) → N ⊗[S] N) y) ⊗ₜ[R]
          (comul : (a : P) → P ⊗[R] P) z)) :
    M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
  (((AlgebraTensorModule.tensorTensorTensorComm S S S S M M (N ⊗[R] P) (N ⊗[R] P) :
          M ⊗[S] M ⊗[S] (N ⊗[R] P ⊗[S] (N ⊗[R] P)) ≃ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
        (a : M ⊗[S] M ⊗[S] (N ⊗[R] P ⊗[S] (N ⊗[R] P))) → M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
      ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[S]
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S N N P P :
              TensorProduct.{u_5, u_8, u_9} R (N ⊗[S] N) (P ⊗[R] P) ≃ₗ[S] N ⊗[R] P ⊗[S] (N ⊗[R] P)) :
            (a : N ⊗[S] N ⊗[R] (P ⊗[R] P)) → N ⊗[R] P ⊗[S] (N ⊗[R] P))
          ((comul : (a : N) → N ⊗[S] N) y ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) z)) :
    M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
Tactic: dsimp