-- 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))
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)
⊢ 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 :
    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)
Tactic: rwa [MonoidalCategory.leftUnitor_hom_apply, ← η[A].hom.map_smul] at h
Cleared hypotheses: h