-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
x : (↑(of R (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(of R (↑A : Type u)) : Type u))
    ((((compr₂ₛₗ (R₄ := R) (M := (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u))
                  (N := (↑(of R (↑A : Type u)) : Type u)) (P :=
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : 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.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : 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 (↟(Algebra.linearMap R (↑A : Type u))) (of R (↑A : Type u)))
                      (↟(mul' R (↑A : Type u))))) :
                (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
              (a : R) → (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
            1 :
          (a : (↑(of R (↑A : Type u)) : Type u)) → (↑(of R (↑A : Type u)) : Type u))
        x :
      (↑(of R (↑A : Type u)) : Type u))
    ((((compr₂ₛₗ (R₄ := R) (M := (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u))
                  (N := (↑(of R (↑A : Type u)) : Type u)) (P :=
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : 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.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)
                    (↑(of R (↑A : Type u)) : Type u))
                  (Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor (of R (↑A : Type u))))) :
                (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u)) :
              (a : R) → (↑(of R (↑A : Type u)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
            1 :
          (a : (↑(of R (↑A : Type u)) : Type u)) → (↑(of R (↑A : Type u)) : Type u))
        x :
      (↑(of R (↑A : Type u)) : Type u))
have hf : Eq (α := (↑(of R (↑A : Type u)) : Type u))
  ((Hom.hom (↟(mul' R (↑A : Type u))) :
        (a : (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u)) →
          (↑(of R (↑A : Type u)) : Type u))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R (↑A : Type u))) (of R (↑A : Type u))) :
            (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) ⊗[R] (↑(of R (↑A : Type u)) : Type u)) →
              (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u))
          (((TensorProduct.mk R (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)
                    (↑(of R (↑A : Type u)) : Type u) :
                  (a : R) →
                    (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) ⊗[R]
                        (↑(of R (↑A : Type u)) : Type u))
                1 :
              (a : (↑(of R (↑A : Type u)) : Type u)) →
                (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) ⊗[R] (↑(of R (↑A : Type u)) : Type u))
            x) :
        (↑(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.leftUnitor (of R (↑A : Type u)))) :
        (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) ⊗[R] (↑(of R (↑A : Type u)) : Type u)) →
          (↑(of R (↑A : Type u)) : Type u))
      (((TensorProduct.mk R (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)
                  (↑(of R (↑A : Type u)) : Type u) :
                (a : R) →
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) ⊗[R] (↑(of R (↑A : Type u)) : Type u))
              1 :
            (a : (↑(of R (↑A : Type u)) : Type u)) →
              (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) ⊗[R] (↑(of R (↑A : Type u)) : Type u))
          x :
        (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) ⊗[R]
          (↑(of R (↑A : Type u)) : Type u)) :
    (↑(of R (↑A : Type u)) : Type u))
Tactic: rw [compr₂ₛₗ_apply, compr₂ₛₗ_apply, hom_comp, LinearMap.comp_apply]