-- 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
f : M →ₗc[S] N
g : P →ₗc[R] Q
x : M
y : P
⊢ Eq (α := N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    (((_root_.TensorProduct.map
              (AlgebraTensorModule.map
                (↑f :
                  [inst : FunLike (M →ₗc[S] N) M N] → [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N)
                (↑g :
                  [inst : FunLike (P →ₗc[R] Q) P Q] → [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q))
              (AlgebraTensorModule.map
                (↑f :
                  [inst : FunLike (M →ₗc[S] N) M N] → [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N)
                (↑g :
                  [inst : FunLike (P →ₗc[R] Q) P Q] →
                    [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q)) :
            M ⊗[R] P ⊗[S] (M ⊗[R] P) →ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
          (a : M ⊗[R] P ⊗[S] (M ⊗[R] P)) → N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M P P :
              TensorProduct.{u_5, u_7, u_9} R (M ⊗[S] M) (P ⊗[R] P) ≃ₗ[S] M ⊗[R] P ⊗[S] (M ⊗[R] P)) :
            (a : M ⊗[S] M ⊗[R] (P ⊗[R] P)) → M ⊗[R] P ⊗[S] (M ⊗[R] P))
          ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) y)) :
      N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    (((AlgebraTensorModule.tensorTensorTensorComm R S R S N N Q Q :
            TensorProduct.{u_5, u_8, u_10} R (N ⊗[S] N) (Q ⊗[R] Q) ≃ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
          (a : N ⊗[S] N ⊗[R] (Q ⊗[R] Q)) → N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
        (((_root_.TensorProduct.map
                  (↑f :
                    [inst : FunLike (M →ₗc[S] N) M N] →
                      [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N)
                  (↑f :
                    [inst : FunLike (M →ₗc[S] N) M N] →
                      [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N) :
                LinearMap.{u_6, u_6, u_7, u_8} (RingHom.id S) (M ⊗[S] M) (N ⊗[S] N)) :
              (a : M ⊗[S] M) → N ⊗[S] N)
            ((comul : (a : M) → M ⊗[S] M) x) ⊗ₜ[R]
          ((_root_.TensorProduct.map
                  (↑g :
                    [inst : FunLike (P →ₗc[R] Q) P Q] →
                      [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q)
                  (↑g :
                    [inst : FunLike (P →ₗc[R] Q) P Q] →
                      [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q) :
                LinearMap.{u_5, u_5, u_9, u_10} (RingHom.id R) (P ⊗[R] P) (Q ⊗[R] Q)) :
              (a : P ⊗[R] P) → Q ⊗[R] Q)
            ((comul : (a : P) → P ⊗[R] P) y)) :
      N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
have a : ∀ (x₁ x₂ : M),
  Eq (α := N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    (((_root_.TensorProduct.map
              (AlgebraTensorModule.map
                (↑f :
                  [inst : FunLike (M →ₗc[S] N) M N] → [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N)
                (↑g :
                  [inst : FunLike (P →ₗc[R] Q) P Q] → [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q))
              (AlgebraTensorModule.map
                (↑f :
                  [inst : FunLike (M →ₗc[S] N) M N] → [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N)
                (↑g :
                  [inst : FunLike (P →ₗc[R] Q) P Q] →
                    [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q)) :
            M ⊗[R] P ⊗[S] (M ⊗[R] P) →ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
          (a : M ⊗[R] P ⊗[S] (M ⊗[R] P)) → N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M P P :
              TensorProduct.{u_5, u_7, u_9} R (M ⊗[S] M) (P ⊗[R] P) ≃ₗ[S] M ⊗[R] P ⊗[S] (M ⊗[R] P)) :
            (a : M ⊗[S] M ⊗[R] (P ⊗[R] P)) → M ⊗[R] P ⊗[S] (M ⊗[R] P))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) y)) :
      N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    (((AlgebraTensorModule.tensorTensorTensorComm R S R S N N Q Q :
            TensorProduct.{u_5, u_8, u_10} R (N ⊗[S] N) (Q ⊗[R] Q) ≃ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
          (a : N ⊗[S] N ⊗[R] (Q ⊗[R] Q)) → N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
        (((_root_.TensorProduct.map
                  (↑f :
                    [inst : FunLike (M →ₗc[S] N) M N] →
                      [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N)
                  (↑f :
                    [inst : FunLike (M →ₗc[S] N) M N] →
                      [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N) :
                LinearMap.{u_6, u_6, u_7, u_8} (RingHom.id S) (M ⊗[S] M) (N ⊗[S] N)) :
              (a : M ⊗[S] M) → N ⊗[S] N)
            (x₁ ⊗ₜ[S] x₂) ⊗ₜ[R]
          ((_root_.TensorProduct.map
                  (↑g :
                    [inst : FunLike (P →ₗc[R] Q) P Q] →
                      [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q)
                  (↑g :
                    [inst : FunLike (P →ₗc[R] Q) P Q] →
                      [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q) :
                LinearMap.{u_5, u_5, u_9, u_10} (RingHom.id R) (P ⊗[R] P) (Q ⊗[R] Q)) :
              (a : P ⊗[R] P) → Q ⊗[R] Q)
            ((comul : (a : P) → P ⊗[R] P) y)) :
      N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
Tactic: hopf_tensor_induction comul (R := S) x with x₁ x₂