-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
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))
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)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (h :
      Eq (α := (↑A : Type u))
        ((Hom.hom η : (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u)) (x • 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)) :
          (↑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)
⊢ 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

Premises used: ModuleCat.MonoidalCategory.leftUnitor_hom_apply, CategoryTheory.MonObj.one, LinearMap.map_smul, ModuleCat.Hom.hom