-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify (goal)
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)
X : C
r : (↑(R.obj (Opposite.op X)) : Type u)
m : (↑(A.obj (Opposite.op X)) : Type v)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : (↑(R₀.obj (Opposite.op Y)) : Type u)
r₀' : (↑(R₀.obj (Opposite.op Z)) : Type u)
m₀ : (↑(M₀.obj (Opposite.op Y)) : Type v)
m₀' : (↑(M₀.obj (Opposite.op Z)) : 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)
            (R.map f.op) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Y)) : Type u))
        r :
      (↑(R.obj (Opposite.op Y)) : Type u))
hr₀' :
  Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        r₀' :
      (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R.obj (Opposite.op X)) (Y := R.obj (Opposite.op Z)) (R.map (f.op ≫ g.op)) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        r :
      (↑(R.obj (Opposite.op Z)) : 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) (A.map f.op) :
          (a : (↑(A.obj (Opposite.op X)) : Type v)) → (↑(A.obj (Opposite.op Y)) : Type v))
        m :
      (↑(A.obj (Opposite.op Y)) : Type v))
hm₀' :
  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))
        m₀' :
      (↑(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 := A.obj (Opposite.op X)) (Y := A.obj (Opposite.op Z)) (A.map (f.op ≫ g.op)) :
          (a : (↑(A.obj (Opposite.op X)) : Type v)) → (↑(A.obj (Opposite.op Z)) : Type v))
        m :
      (↑(A.obj (Opposite.op Z)) : Type v))
hr₁ :
  Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
                (R₀.map g.op) :
              (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R₀.obj (Opposite.op Z)) : Type u))
            r₀ :
          (↑(R₀.obj (Opposite.op Z)) : Type u)) :
      (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R.obj (Opposite.op X)) (Y := R.obj (Opposite.op Z)) (R.map (f.op ≫ g.op)) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        r :
      (↑(R.obj (Opposite.op Z)) : Type u))
hr₂ :
  Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
                (R₀.map g.op) :
              (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R₀.obj (Opposite.op Z)) : Type u))
            r₀ :
          (↑(R₀.obj (Opposite.op Z)) : Type u)) :
      (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (R.map f.op ≫ R.map g.op) :
          (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        r :
      (↑(R.obj (Opposite.op Z)) : Type u))
hr₃ :
  Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
                (R₀.map g.op) :
              (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R₀.obj (Opposite.op Z)) : Type u))
            r₀ :
          (↑(R₀.obj (Opposite.op Z)) : Type u)) :
      (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (R.map g.op) :
          (a : (↑(R.obj (Opposite.op Y)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
                (R.map f.op) :
              (a : (↑(R.obj (Opposite.op X)) : Type u)) → (↑(R.obj (Opposite.op Y)) : Type u))
            r :
          (↑(R.obj (Opposite.op Y)) : Type u)) :
      (↑(R.obj (Opposite.op Z)) : Type u))
⊢ Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
                (R₀.map g.op) :
              (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R₀.obj (Opposite.op Z)) : Type u))
            r₀ :
          (↑(R₀.obj (Opposite.op Z)) : Type u)) :
      (↑(R.obj (Opposite.op Z)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (X := R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
          (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
        r₀' :
      (↑(R.obj (Opposite.op Z)) : Type u))
have hr₄ : Eq (α := (↑(R.obj (Opposite.op Z)) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier) (X :=
          R₀.obj (Opposite.op Z)) (α.app (Opposite.op Z)) :
        (a : (↑(R₀.obj (Opposite.op Z)) : Type u)) → (↑(R.obj (Opposite.op Z)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              (R₀.map g.op) :
            (a : (↑(R₀.obj (Opposite.op Y)) : Type u)) → (↑(R₀.obj (Opposite.op Z)) : Type u))
          r₀ :
        (↑(R₀.obj (Opposite.op Z)) : Type u)) :
    (↑(R.obj (Opposite.op Z)) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
          (R.map g.op) :
        (a : (↑(R.obj (Opposite.op Y)) : Type u)) → (↑(R.obj (Opposite.op Z)) : 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)) :
    (↑(R.obj (Opposite.op Z)) : Type u))
Tactic: rw [hr₀', R.map_comp, RingCat.comp_apply, ← hr₀, ← RingCat.comp_apply, NatTrans.naturality,
      RingCat.comp_apply]