-- 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
⊢ 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)))
have 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)))
Tactic: ext x y z