-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
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
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀
    (a b :
      (↑((forget₂ (ModuleCat.{v, u} (↑(R.obj X) : Type u)) (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                  (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier) :
                ModuleCat.{v, u} (↑(R.obj X) : Type u) ⥤ Ab).1
            (M.obj X)) :
        Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
        (a + b) =
      HAdd.hAdd (α :=
        (↑((forget₂ (ModuleCat.{v, u} (↑(R.obj Y) : Type u)) (FC :=
                    fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                    LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u))
                      (↑x1 : Type v) (↑x2 : Type v))
                    (CC := ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier) :
                  ModuleCat.{v, u} (↑(R.obj Y) : Type u) ⥤ Ab).1
              (M.obj Y)) :
          Type v))
        (β :=
        (↑((forget₂ (ModuleCat.{v, u} (↑(R.obj Y) : Type u)) (FC :=
                    fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                    LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u))
                      (↑x1 : Type v) (↑x2 : Type v))
                    (CC := ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier) :
                  ModuleCat.{v, u} (↑(R.obj Y) : Type u) ⥤ Ab).1
              (M.obj Y)) :
          Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M.map f) :
              (a : (↑(M.obj X) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
            a :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M.map f) :
              (a : (↑(M.obj X) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
            b :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))

Tactic:
simp