-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R₀ : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj (P := Presheaf.IsSheaf J)
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
inst_2 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj (P := Presheaf.IsSheaf J)
inst_3 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
inst_4 :
  Presheaf.IsLocallySurjective J (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier) φ
X : Cᵒᵖ
r : (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)
m m' : (↑(A.obj (P := Presheaf.IsSheaf J).obj X) : Type v)
S : Sieve.{v₁, u₁} (Opposite.unop X) :=
  Presheaf.imageSieve (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA := RingCat.carrier) α r ⊓
      Presheaf.imageSieve (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
        AddCommGrpCat.carrier) φ m ⊓
    Presheaf.imageSieve (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
      AddCommGrpCat.carrier) φ m'
hS : Membership.mem (γ := Set (Sieve.{v₁, u₁} (Opposite.unop X))) ((J : (a : C) → Set (Sieve a)) (Opposite.unop X)) S
Y : C
f : Y ⟶ Opposite.unop X
r₀ :
  ToType (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
    (R₀.obj (Opposite.op Y))
hr₀ :
  Eq (α := (↑(R.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Y)) (α.app (Opposite.op Y)) :
          (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R.obj.obj (Opposite.op Y)) : Type u))
        r₀ :
      (↑(R.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (R.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (↑(R.obj.obj (Opposite.op (Opposite.unop X))) : Type u)) → (↑(R.obj.obj (Opposite.op Y)) : Type u))
        r :
      (↑(R.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type u))
m₀ : (↑(M₀.obj (Opposite.op Y)) : Type v)
hm₀ :
  Eq (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
        m₀ :
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
        m :
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
m₀' : (↑(M₀.obj (Opposite.op Y)) : Type v)
hm₀' :
  Eq (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
        m₀' :
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
        m' :
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
a :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (A.obj (P := Presheaf.IsSheaf J).map f.op) :
        (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
      (smul α φ r (m + m')) =
    HAdd.hAdd (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) (β :=
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((AddCommGrpCat.Hom.hom (A.obj (P := Presheaf.IsSheaf J).map f.op) :
            (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (smul α φ r m) :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((AddCommGrpCat.Hom.hom (A.obj (P := Presheaf.IsSheaf J).map f.op) :
            (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (smul α φ r m') :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
a₁ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (A.obj (P := Presheaf.IsSheaf J).map f.op) :
        (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
      (smul α φ r (m + m')) =
    HAdd.hAdd (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) (β :=
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀) :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((AddCommGrpCat.Hom.hom (A.obj (P := Presheaf.IsSheaf J).map f.op) :
            (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (smul α φ r m') :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
a₂ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (A.obj (P := Presheaf.IsSheaf J).map f.op) :
        (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
      (smul α φ r (m + m')) =
    HAdd.hAdd (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) (β :=
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀) :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀') :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
a₃ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
        (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
      (r₀ • (m₀ + m₀')) =
    HAdd.hAdd (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) (β :=
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀) :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀') :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
a₄ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
        (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
      (r₀ • m₀ + r₀ • m₀') =
    HAdd.hAdd (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) (β :=
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀) :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀') :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
a₅ a₆ :
  HAdd.hAdd (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) (β :=
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀) :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀') :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) =
    HAdd.hAdd (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v)) (β :=
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀) :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (X := M₀.presheaf.obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
            (a : (↑(M₀.presheaf.obj (Opposite.op Y)) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
          (r₀ • m₀') :
        (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
⊢ Eq (α := (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
        (smul α φ r (m + m')) :
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (↑(A.obj.obj (Opposite.op (Opposite.unop X))) : Type v)) → (↑(A.obj.obj (Opposite.op Y)) : Type v))
        (smul α φ r m + smul α φ r m') :
      (↑(A.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)) : Type v))

Tactic:
rw [(A.obj.map f.op).hom.map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
    map_smul_eq α φ r m' f.op r₀ hr₀ m₀' hm₀',
    map_smul_eq α φ r (m + m') f.op r₀ hr₀ (m₀ + m₀')
      (by rw [_root_.map_add, _root_.map_add, hm₀, hm₀']),
    smul_add, _root_.map_add]

Premises used: Quiver.Hom.op, PresheafOfModules.Sheafify.map_smul_eq, map_add, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, HAdd.hAdd, AddCommGrpCat.Hom.hom, AddMonoidHom.map_add, smul_add