-- 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 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))
⊢ 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 : ModuleCat.{v, u} (↑(R₀.obj (Opposite.op Y)) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R₀.obj (Opposite.op Y)) : Type u))
                  (RingHom.id (↑(R₀.obj (Opposite.op Y)) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M₀.map g.op) :
              (a : (↑(M₀.obj (Opposite.op Y)) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.obj (Opposite.op Z))) : Type v))
            (r₀ • m₀) :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.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))
        (r₀' • m₀') :
      (↑(A.obj (Opposite.op Z)) : Type v))
have 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))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R₀.obj (Opposite.op Y)) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R₀.obj (Opposite.op Y)) : Type u))
                (RingHom.id (↑(R₀.obj (Opposite.op Y)) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M₀.map g.op) :
            (a : (↑(M₀.obj (Opposite.op Y)) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.obj (Opposite.op Z))) : Type v))
          m₀ :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g.op))).obj (M₀.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))
      m₀' :
    (↑(A.obj (Opposite.op Z)) : Type v))
Tactic: rw [← PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective α φ hA (R₀.map g.op r₀) r₀'
    (M₀.map g.op m₀) m₀', M₀.map_smul]