-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean
lemma toSheaf_map_sheafificationHomEquiv_symm
    {P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
    (g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F)) :
    (SheafOfModules.toSheaf _).map ((sheafificationHomEquiv α).symm g) =
      (((sheafificationAdjunction J AddCommGrp).homEquiv
        P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm ((toPresheaf R₀).map g))

Proof state:
case intro.a
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (sheafificationAdjunction J AddCommGrp).unit.app P.presheaf ≫
      (sheafToPresheaf J AddCommGrp).map ((SheafOfModules.toSheaf R).map f) =
    (toPresheaf R₀).map ((sheafificationHomEquiv α) f)

Tactic:
rfl

Result:
no goals

Proof state:
case intro
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f)) =
    ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
      ((toPresheaf R₀).map ((sheafificationHomEquiv α) f))

Tactic:
apply ((sheafificationAdjunction J AddCommGrp).homEquiv _ _).injective

Result:
case intro.a
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f))) =
    ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      (((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
        ((toPresheaf R₀).map ((sheafificationHomEquiv α) f)))

Proof state:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F)
⊢ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm g) =
    ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
      ((toPresheaf R₀).map g)

Tactic:
obtain ⟨f, rfl⟩ := (sheafificationHomEquiv α).surjective g

Result:
case intro
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f)) =
    ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
      ((toPresheaf R₀).map ((sheafificationHomEquiv α) f))

Proof state:
case intro.a
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f))) =
    ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      (((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
        ((toPresheaf R₀).map ((sheafificationHomEquiv α) f)))

Tactic:
rw [Equiv.apply_symm_apply, Adjunction.homEquiv_unit, Equiv.symm_apply_apply]

Result:
case intro.a
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (sheafificationAdjunction J AddCommGrp).unit.app P.presheaf ≫
      (sheafToPresheaf J AddCommGrp).map ((SheafOfModules.toSheaf R).map f) =
    (toPresheaf R₀).map ((sheafificationHomEquiv α) f)