-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R₀ R : Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
α : R₀ ⟶ R
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
M₀ : PresheafOfModules.{v, v₁, u₁, u} R₀
A : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst_2 :
  Presheaf.IsLocallyInjective (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier) J φ
hA :
  Presheaf.IsSeparated J A (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CA :=
    AddCommGrpCat.carrier)
Y : C
r₀ r₀' : (↑(R₀.obj (Opposite.op Y)) : Type u)
m₀ m₀' : (↑(M₀.obj (Opposite.op Y)) : Type v)
hr₀ :
  Eq (α := (↑(R.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 (Opposite.op Y)) : Type u))
        r₀ :
      (↑(R.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 (Opposite.op Y)) : Type u))
        r₀' :
      (↑(R.obj (Opposite.op Y)) : Type u))
hm₀ :
  Eq (α := (↑(A.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 (Opposite.op Y)) : Type v))
        m₀ :
      (↑(A.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 (Opposite.op Y)) : Type v))
        m₀' :
      (↑(A.obj (Opposite.op Y)) : Type v))
Z : C
g : Z ⟶ Opposite.unop (Opposite.op Y)
hg :
  (Presheaf.equalizerSieve (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier) r₀
          r₀' ⊓
        Presheaf.equalizerSieve (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
          AddCommGrpCat.carrier) (F := M₀.presheaf) m₀ m₀').arrows
    g
a :
  Eq (α := (↑(A.obj (Opposite.op Z)) : 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 Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M₀.presheaf.map g.op) :
              (a : (↑(M₀.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) →
                (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))
            (r₀ • m₀) :
          (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) :
      (↑(A.obj (Opposite.op Z)) : 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 Z)) (φ.app (Opposite.op Z)) :
          (a : (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M₀.presheaf.map g.op) :
              (a : (↑(M₀.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) →
                (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v))
            (r₀' • m₀') :
          (↑(M₀.presheaf.obj (Opposite.op Z)) : Type v)) :
      (↑(A.obj (Opposite.op Z)) : Type v))
⊢ Eq (α := (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.map g.op) :
          (a : (↑(A.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) → (↑(A.obj (Opposite.op Z)) : 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 (Opposite.op Y)) : Type v))
            (r₀ • m₀) :
          (↑(A.obj (Opposite.op Y)) : Type v)) :
      (↑(A.obj (Opposite.op Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (A.map g.op) :
          (a : (↑(A.obj (Opposite.op (Opposite.unop (Opposite.op Y)))) : Type v)) → (↑(A.obj (Opposite.op Z)) : 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 (Opposite.op Y)) : Type v))
            (r₀' • m₀') :
          (↑(A.obj (Opposite.op Y)) : Type v)) :
      (↑(A.obj (Opposite.op Z)) : Type v))

Tactic:
rw [← NatTrans.naturality_apply (D := Ab), ← NatTrans.naturality_apply (D := Ab)]

Premises used: CategoryTheory.NatTrans.naturality_apply