-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R_1 : Sheaf J RingCat
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
N : PresheafOfModules.{v, v₁, u₁, u} R
hN : Presheaf.IsSheaf J N.presheaf
inst_1 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_2 : IsLocallySurjective J f
inst_3 : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  ∀ (Z : Cᵒᵖ) (x : (↑(M₁.obj Z) : Type v)),
    Eq (α := (↑(N.presheaf.obj Z) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (φ.app Z) :
            (a : (↑(((toPresheaf R).obj M₂).obj Z) : Type v)) → (↑(N.presheaf.obj Z) : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (f.app Z) :
                (a : (↑(M₁.obj Z) : Type v)) → (↑(M₂.obj Z) : Type v))
              x :
            (↑(M₂.obj Z) : Type v)) :
        (↑(N.presheaf.obj Z) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (ψ.app Z) :
            (a : (↑(M₁.obj Z) : Type v)) → (↑(N.obj Z) : Type v))
          x :
        (↑(N.obj Z) : Type v))
X : Cᵒᵖ
r : (↑(R.obj X) : Type u)
y : (↑(M₂.obj X) : Type v)
Y : C
p : Y ⟶ Opposite.unop X
x : (↑(M₁.obj (Opposite.op Y)) : Type v)
hx :
  Eq (α := (↑(M₂.obj (Opposite.op Y)) : 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) (f.app (Opposite.op Y)) :
          (a : (↑(M₁.obj (Opposite.op Y)) : Type v)) → (↑(M₂.obj (Opposite.op Y)) : Type v))
        x :
      (↑(M₂.obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u))
              (RingHom.id (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M₂.map p.op) :
          (a : (↑(M₂.obj (Opposite.op (Opposite.unop X))) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v))
        y :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v))
⊢ Eq (α := (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (N.presheaf.map p.op) :
          (a : (↑(N.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v)) →
            (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
            (r • y) :
          (↑(N.presheaf.obj X) : Type v)) :
      (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (N.presheaf.map p.op) :
          (a : (↑(N.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v)) →
            (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
        (HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                  AddCommGrpCat.carrier) (φ.app X) :
                (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
              y :
            (↑(N.presheaf.obj X) : Type v))) :
      (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
have hφ' : ∀ (z : (↑(M₂.obj X) : Type v)),
  Eq (α := (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := ((toPresheaf R).obj M₂).obj (Opposite.op Y)) (φ.app (Opposite.op Y)) :
          (a : (↑(((toPresheaf R).obj M₂).obj (Opposite.op Y)) : Type v)) →
            (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
        ((ConcreteCategory.hom (FC :=
                fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u))
                  (RingHom.id (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M₂.map p.op) :
              (a : (↑(M₂.obj (Opposite.op (Opposite.unop X))) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v))
            z :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map p.op))).obj (M₂.obj (Opposite.op Y))) : Type v)) :
      (↑(N.presheaf.obj (Opposite.op Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u))
              (RingHom.id (↑(R.obj (Opposite.op (Opposite.unop X))) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (N.map p.op) :
          (a : (↑(N.obj (Opposite.op (Opposite.unop X))) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map p.op))).obj (N.obj (Opposite.op Y))) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (X := ((toPresheaf R).obj M₂).obj (Opposite.op (Opposite.unop X)))
                (φ.app (Opposite.op (Opposite.unop X))) :
              (a : (↑(((toPresheaf R).obj M₂).obj (Opposite.op (Opposite.unop X))) : Type v)) →
                (↑(N.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v))
            z :
          (↑(N.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v)) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map p.op))).obj (N.obj (Opposite.op Y))) : Type v))
Tactic: have hφ' : ∀ (z : M₂.obj X), φ.app _ (M₂.map p.op z) =
            N.map p.op (φ.app _ z) := CategoryTheory.congr_fun (φ.naturality p.op)