-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification (goal)
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R₀ : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj (P := Presheaf.IsSheaf J)
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
inst_2 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_4 : HasWeakSheafify J AddCommGrpCat
P : PresheafOfModules.{v, v', u', u} R₀
F : SheafOfModules.{v, v', u', u} R
f : (sheafification α).obj P ⟶ F
⊢ Eq (α := (SheafOfModules.toSheaf R).obj ((sheafification α).obj P) ⟶ (SheafOfModules.toSheaf R).obj F)
    ((SheafOfModules.toSheaf R).map
      ((Equiv.symm (sheafificationHomEquiv α) :
          (a : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F)) → (sheafification α).obj P ⟶ F)
        ((sheafificationHomEquiv α :
            (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
          f)))
    ((Equiv.symm
          (Adjunction.homEquiv (sheafificationAdjunction J AddCommGrpCat) P.presheaf
            ((SheafOfModules.toSheaf R).obj F)) :
        (a : P.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj F)) →
          (presheafToSheaf J AddCommGrpCat).obj P.presheaf ⟶ (SheafOfModules.toSheaf R).obj F)
      ((toPresheaf R₀).map
        ((sheafificationHomEquiv α :
            (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
          f)))
have a : Eq (α := P.presheaf ⟶ Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj F))
  ((Adjunction.homEquiv (sheafificationAdjunction J AddCommGrpCat) P.presheaf ((SheafOfModules.toSheaf R).obj F) :
        (a : (presheafToSheaf J AddCommGrpCat).obj P.presheaf ⟶ (SheafOfModules.toSheaf R).obj F) →
          P.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map
        ((Equiv.symm (sheafificationHomEquiv α) :
            (a : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F)) → (sheafification α).obj P ⟶ F)
          ((sheafificationHomEquiv α :
              (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
            f))) :
    P.presheaf ⟶ Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj F))
  ((Adjunction.homEquiv (sheafificationAdjunction J AddCommGrpCat) P.presheaf ((SheafOfModules.toSheaf R).obj F) :
        (a : (presheafToSheaf J AddCommGrpCat).obj P.presheaf ⟶ (SheafOfModules.toSheaf R).obj F) →
          P.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj F))
      ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J AddCommGrpCat) P.presheaf
              ((SheafOfModules.toSheaf R).obj F)) :
          (a : P.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj F)) →
            (presheafToSheaf J AddCommGrpCat).obj P.presheaf ⟶ (SheafOfModules.toSheaf R).obj F)
        ((toPresheaf R₀).map
          ((sheafificationHomEquiv α :
              (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
            f))) :
    P.presheaf ⟶ Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj F))
Tactic: apply ((sheafificationAdjunction J AddCommGrpCat).homEquiv _ _).injective