-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₁.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
            m :
          (↑(M₂.presheaf.obj X) : Type v))
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M₁.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        (ModuleCat.ofHom
          {
            toFun :=
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                    AddCommGrpCat.carrier) (φ.app Y)) :
                (a : (↑(M₁.presheaf.obj Y) : Type v)) → (↑(M₂.presheaf.obj Y) : Type v)),
            map_add' := ⋯, map_smul' := ⋯ }) =
    ModuleCat.ofHom
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                  AddCommGrpCat.carrier) (φ.app X)) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v)),
          map_add' := ⋯, map_smul' := ⋯ :
          LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑(M₁.1 X) : Type v)
            (↑(M₂.1 X) : Type v) } ≫
      M₂.map f
have hf : ∀ (x : (↑(M₁.obj X) : Type v)),
  Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            (M₁.map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                (ModuleCat.ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                            (CC := AddCommGrpCat.carrier) (φ.app Y)) :
                        (a : (↑(M₁.presheaf.obj Y) : Type v)) → (↑(M₂.presheaf.obj Y) : Type v)),
                    map_add' := sorry, map_smul' := sorry })) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                          (CC := AddCommGrpCat.carrier) (φ.app X)) :
                      (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v)),
                  map_add' := sorry, map_smul' := sorry } ≫
              M₂.map f) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
Tactic: ext x