-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y : R
h :
  Eq (α := (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (x ⊗ₜ[R]
            (@ConcreteCategory.hom _ (moduleCategory R)
                  (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) carrier _ _
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) A η :
                (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
              y :
          (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) ⊗[R] (↑A : Type u)) :
      (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (x ⊗ₜ[R]
            (@ConcreteCategory.hom _ (moduleCategory R)
                  (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) carrier _ _
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) A η :
                (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
              y :
          (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) ⊗[R] (↑A : Type u)) :
      (↑A : Type u))
⊢ AddHom.toFun (toAddHom (Hom.hom η)) (x * y) =
    HMul.hMul (α := (↑A : Type u)) (AddHom.toFun (toAddHom (Hom.hom η)) x) (AddHom.toFun (toAddHom (Hom.hom η)) y)
have rwa : ∀
  (h :
    HSMul.hSMul (β := (↑A : Type u)) x
        ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                carrier _ _ (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) A η :
              (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
            y :
          (↑A : Type u)) =
      (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (x ⊗ₜ[R]
            (@ConcreteCategory.hom _ (moduleCategory R)
                  (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) carrier _ _
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) A η :
                (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
              y :
          (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) ⊗[R] (↑A : Type u))),
  AddHom.toFun (toAddHom (Hom.hom η)) (x * y) =
    HMul.hMul (α := (↑A : Type u)) (AddHom.toFun (toAddHom (Hom.hom η)) x) (AddHom.toFun (toAddHom (Hom.hom η)) y)
Tactic: rwa [MonoidalCategory.leftUnitor_hom_apply, ← η[A].hom.map_smul] at h
Cleared hypotheses: h