-- 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
x₁ x₂ : M
y₁ y₂ : N
⊢ 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))
              (x₁ ⊗ₜ[S] x₂ ⊗ₜ[S] (y₁ ⊗ₜ[S] 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)))
        (x₁ ⊗ₜ[S] 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))
            (y₁ ⊗ₜ[S] y₂ ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) z)) :
      M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
have a : ∀ (z₁ z₂ : P),
  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))
              (x₁ ⊗ₜ[S] x₂ ⊗ₜ[S] (y₁ ⊗ₜ[S] y₂)) ⊗ₜ[R]
            (z₁ ⊗ₜ[R] 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)))
        (x₁ ⊗ₜ[S] 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))
            (y₁ ⊗ₜ[S] y₂ ⊗ₜ[R] (z₁ ⊗ₜ[R] z₂))) :
      M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
Tactic: hopf_tensor_induction comul (R := R) z with z₁ z₂