-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
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
obtain :
  ∀ (φ : (toPresheaf R).obj M₂ ⟶ N.presheaf)
    (hφ :
      (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN :
            (a : (toPresheaf R).obj M₂ ⟶ N.presheaf) → (toPresheaf R).obj M₁ ⟶ N.presheaf)
          φ =
        (toPresheaf R).map ψ)
    (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₂.obj X) : Type v)),
    (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
            (M₂.presheaf.obj X) (N.presheaf.obj X)
            (NatTrans.app
              (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                  (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                ((toPresheaf R).map ψ))
              X) :
          (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
        ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
                (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
                (M₂.presheaf.obj X) (N.presheaf.obj X)
                (NatTrans.app
                  (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                      (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                    ((toPresheaf R).map ψ))
                  X) :
              (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
            m :
          (↑(N.presheaf.obj X) : Type v))
⊢ ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₂.obj X) : Type v)),
    (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
            (M₂.presheaf.obj X) (N.presheaf.obj X)
            (NatTrans.app
              (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                  (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                ((toPresheaf R).map ψ))
              X) :
          (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
        ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
                (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
                (M₂.presheaf.obj X) (N.presheaf.obj X)
                (NatTrans.app
                  (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                      (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                    ((toPresheaf R).map ψ))
                  X) :
              (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
            m :
          (↑(N.presheaf.obj X) : Type v))

Tactic:
obtain ⟨φ, hφ⟩ := ((J.W_of_isLocallyBijective
          ((PresheafOfModules.toPresheaf R).map f)).homEquiv _ hN).surjective
          ((PresheafOfModules.toPresheaf R).map ψ)

Premises used: CategoryTheory.GrothendieckTopology.W_of_isLocallyBijective, CategoryTheory.Functor.map, CategoryTheory.ObjectProperty.isLocal.homEquiv, PresheafOfModules.toPresheaf, Equiv.surjective