-- 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))
    ((((LinearMap.id :
                (a :
                    (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                        (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) →ₗ[R]
                      (↑(of R (↑A : Type u)) : Type u)) →
                  (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) →ₗ[R]
                    (↑(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.whiskerLeft (of R (↑A : Type u)) (↟(Algebra.linearMap R (↑A : Type u))))
                  (↟(mul' R (↑A : Type u))))) :
            (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
              (↑(of R (↑A : Type u)) : Type u)) :
          (a : (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) →
            (↑(of R (↑A : Type u)) : Type u))
        ((((TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u)
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) :
                  (a : (↑(of R (↑A : Type u)) : Type u)) →
                    R →ₗ[R]
                      (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                        (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
                x :
              R →ₗ[R]
                (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) :
            (a : R) →
              (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
          1) :
      (↑(of R (↑A : Type u)) : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor (of R (↑A : Type u)))) :
          (a : (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) →
            (↑(of R (↑A : Type u)) : Type u))
        ((((TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u)
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) :
                  (a : (↑(of R (↑A : Type u)) : Type u)) →
                    R →ₗ[R]
                      (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                        (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
                x :
              R →ₗ[R]
                (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) :
            (a : R) →
              (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
          1) :
      (↑(of R (↑A : Type u)) : Type u))
have hf : Eq (α := (↑A : Type u))
  (((mul' R (↑A : Type u) : (↑A : Type u) ⊗[R] (↑A : Type u) →ₗ[R] (↑A : Type u)) :
        (a : (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u)) → (↑A : Type u))
      (((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(Algebra.linearMap R (↑A : Type u)))) :
              (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                      (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))) :
                  Type u) →ₗ[R]
                (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
                  Type u)) :
            (a : (↑A : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) →
              (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u))
          ((((TensorProduct.mk R (↑A : Type u)
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) :
                    (a : (↑A : Type u)) →
                      R →ₗ[R] (↑A : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
                  x :
                R →ₗ[R]
                  (↑A : Type u) ⊗[R]
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) :
              (a : R) → (↑A : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
            1) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
          Type u)) :
    (↑A : Type u))
  ((Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor (of R (↑A : Type u)))) :
        (a : (↑A : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
      ((((TensorProduct.mk R (↑A : Type u)
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) :
                (a : (↑A : Type u)) →
                  R →ₗ[R] (↑A : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
              x :
            R →ₗ[R]
              (↑A : Type u) ⊗[R]
                (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) :
          (a : R) → (↑A : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
        1) :
    (↑A : Type u))
Tactic: simp only [hom_comp, hom_ofHom, id_coe, id_eq, LinearMap.comp_apply]