-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
x y z : (↑(of R (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(of R (↑A : Type u)) : Type u))
    (((((((compr₂ₛₗ (R₄ := R) (M := (↑(of R (↑A : Type u)) : Type u)) (N := (↑(of R (↑A : Type u)) : Type u)) (P :=
                          (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(of R (↑A : Type u)) : Type u)) (Q :=
                          (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) (σ₁₄ := RingHom.id R)
                          (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
                          (TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u) (↑(of R (↑A : Type u)) : Type u))
                          (compr₂ₛₗ (R₄ := R) (M :=
                            (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                  (of R (↑A : Type u))) :
                              Type u))
                            (N := (↑(of R (↑A : Type u)) : Type u)) (P :=
                            (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                    (of R (↑A : Type u))) :
                                Type u) ⊗[R]
                              (↑(of R (↑A : Type u)) : Type u))
                            (Q := (↑(of R (↑A : Type u)) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ :=
                            RingHom.id R)
                            (TensorProduct.mk R
                              (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                    (of R (↑A : Type u))) :
                                Type u)
                              (↑(of R (↑A : Type u)) : Type u))
                            (Hom.hom
                              (CategoryStruct.comp (Y :=
                                MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                  (of R (↑A : Type u)))
                                (MonoidalCategoryStruct.whiskerRight (↟(mul' R (↑A : Type u))) (of R (↑A : Type u)))
                                (↟(mul' R (↑A : Type u)))))) :
                        (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                          (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                            (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
                      (a : (↑(of R (↑A : Type u)) : Type u)) →
                        (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                          (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
                    x :
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                    (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
                (a : (↑(of R (↑A : Type u)) : Type u)) →
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
              y :
            (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
          (a : (↑(of R (↑A : Type u)) : Type u)) → (↑(of R (↑A : Type u)) : Type u))
        z :
      (↑(of R (↑A : Type u)) : Type u))
    (((((((compr₂ₛₗ (R₄ := R) (M := (↑(of R (↑A : Type u)) : Type u)) (N := (↑(of R (↑A : Type u)) : Type u)) (P :=
                          (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(of R (↑A : Type u)) : Type u)) (Q :=
                          (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) (σ₁₄ := RingHom.id R)
                          (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
                          (TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u) (↑(of R (↑A : Type u)) : Type u))
                          (compr₂ₛₗ (R₄ := R) (M :=
                            (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                  (of R (↑A : Type u))) :
                              Type u))
                            (N := (↑(of R (↑A : Type u)) : Type u)) (P :=
                            (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                    (of R (↑A : Type u))) :
                                Type u) ⊗[R]
                              (↑(of R (↑A : Type u)) : Type u))
                            (Q := (↑(of R (↑A : Type u)) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ :=
                            RingHom.id R)
                            (TensorProduct.mk R
                              (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                    (of R (↑A : Type u))) :
                                Type u)
                              (↑(of R (↑A : Type u)) : Type u))
                            (Hom.hom
                              (Iso.hom
                                  (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u))
                                    (of R (↑A : Type u))) ≫
                                CategoryStruct.comp (Y :=
                                  MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                                    (of R (↑A : Type u)))
                                  (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u))))
                                  (↟(mul' R (↑A : Type u)))))) :
                        (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                          (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                            (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
                      (a : (↑(of R (↑A : Type u)) : Type u)) →
                        (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                          (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
                    x :
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                    (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
                (a : (↑(of R (↑A : Type u)) : Type u)) →
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
              y :
            (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
          (a : (↑(of R (↑A : Type u)) : Type u)) → (↑(of R (↑A : Type u)) : Type u))
        z :
      (↑(of R (↑A : Type u)) : Type u))
have hf : Eq (α := (↑A : Type u))
  (((Hom.hom
            (CategoryStruct.comp (Y :=
              MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
              (MonoidalCategoryStruct.whiskerRight (↟(mul' R (↑A : Type u))) (of R (↑A : Type u)))
              (↟(mul' R (↑A : Type u)))) :
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
                  (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
                  (of R (↑A : Type u))) :
              Type u) →ₗ[R]
            (↑(of R (↑A : Type u)) : Type u)) :
        (a :
            (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
              (↑A : Type u)) →
          (↑A : Type u))
      ((((TensorProduct.mk R
                    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                          (of R (↑A : Type u))) :
                      Type u)
                    (↑A : Type u) :
                  (a : (↑A : Type u) ⊗[R] (↑A : Type u)) →
                    (↑A : Type u) →ₗ[R]
                      (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                        (↑A : Type u))
                (x ⊗ₜ[R] y) :
              (↑A : Type u) →ₗ[R]
                (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
                    Type u) ⊗[R]
                  (↑A : Type u)) :
            (a : (↑A : Type u)) →
              (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                (↑A : Type u))
          z :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
            Type u) ⊗[R]
          (↑A : Type u)) :
    (↑A : Type u))
  (((Hom.hom
            (Iso.hom
                (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u)) (of R (↑A : Type u))) ≫
              CategoryStruct.comp (Y :=
                MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
                (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u))))
                (↟(mul' R (↑A : Type u)))) :
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
                  (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
                  (of R (↑A : Type u))) :
              Type u) →ₗ[R]
            (↑(of R (↑A : Type u)) : Type u)) :
        (a :
            (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
              (↑A : Type u)) →
          (↑A : Type u))
      ((((TensorProduct.mk R
                    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                          (of R (↑A : Type u))) :
                      Type u)
                    (↑A : Type u) :
                  (a : (↑A : Type u) ⊗[R] (↑A : Type u)) →
                    (↑A : Type u) →ₗ[R]
                      (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                        (↑A : Type u))
                (x ⊗ₜ[R] y) :
              (↑A : Type u) →ₗ[R]
                (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
                    Type u) ⊗[R]
                  (↑A : Type u)) :
            (a : (↑A : Type u)) →
              (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                (↑A : Type u))
          z :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
            Type u) ⊗[R]
          (↑A : Type u)) :
    (↑A : Type u))
Tactic: dsimp only [compr₂ₛₗ_apply, TensorProduct.mk_apply]