awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
M₀ : PresheafOfModules.{v, v', u', u} R₀
h :
  (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (SheafOfModules.Hom.val
        (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯)) =
    (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (SheafOfModules.Hom.val
        (𝟙
          (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf))))
⊢ SheafOfModules.Hom.val
      (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯) =
    SheafOfModules.Hom.val
      (𝟙 (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf)))

Tactic:
apply (toPresheaf _).map_injective

Premises used: PresheafOfModules.toPresheaf, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
M₀ : PresheafOfModules.{v, v', u', u} R₀
h :
  (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (homMk
        (𝟙 ((Functor.obj (presheafToSheaf J AddCommGrpCat) ((toPresheaf R₀).obj M₀)).obj (P := Presheaf.IsSheaf J)))
        ⋯) =
    𝟙
      ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
        (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf)
            (CategoryTheory.toSheafify J M₀.presheaf)).val)
⊢ (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (SheafOfModules.Hom.val
        (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯)) =
    (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (SheafOfModules.Hom.val
        (𝟙
          (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf))))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
M₀ : PresheafOfModules.{v, v', u', u} R₀
⊢ (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (homMk
        (𝟙 ((Functor.obj (presheafToSheaf J AddCommGrpCat) ((toPresheaf R₀).obj M₀)).obj (P := Presheaf.IsSheaf J)))
        ⋯) =
    𝟙
      ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
        (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf)
            (CategoryTheory.toSheafify J M₀.presheaf)).val)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
X Y Z : PresheafOfModules.{v, v', u', u} R₀
x : X ⟶ Y
x_1 : Y ⟶ Z
h :
  Eq (α :=
    (sheafify α (A := Functor.obj (presheafToSheaf J Ab) X.presheaf) (CategoryTheory.toSheafify J X.presheaf)).val ⟶
      (sheafify α (A := Functor.obj (presheafToSheaf J Ab) Z.presheaf) (CategoryTheory.toSheafify J Z.presheaf)).val)
    (SheafOfModules.Hom.val
      (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Z.presheaf) (x ≫ x_1)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x ≫ x_1)) ⋯))
    (SheafOfModules.Hom.val
      (CategoryStruct.comp (Y :=
        sheafify α (A := Functor.obj (presheafToSheaf J Ab) Y.presheaf) (CategoryTheory.toSheafify J Y.presheaf))
        (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) x
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x) ⋯)
        (sheafifyMap α (CategoryTheory.toSheafify J Y.presheaf) (CategoryTheory.toSheafify J Z.presheaf) x_1
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x_1) ⋯)))
⊢ Eq (α :=
    sheafify α (A := Functor.obj (presheafToSheaf J Ab) X.presheaf) (CategoryTheory.toSheafify J X.presheaf) ⟶
      sheafify α (A := Functor.obj (presheafToSheaf J Ab) Z.presheaf) (CategoryTheory.toSheafify J Z.presheaf))
    (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Z.presheaf) (x ≫ x_1)
      ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x ≫ x_1)) ⋯)
    (CategoryStruct.comp (Y :=
      sheafify α (A := Functor.obj (presheafToSheaf J Ab) Y.presheaf) (CategoryTheory.toSheafify J Y.presheaf))
      (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) x
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x) ⋯)
      (sheafifyMap α (CategoryTheory.toSheafify J Y.presheaf) (CategoryTheory.toSheafify J Z.presheaf) x_1
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x_1) ⋯))

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
X Y Z : PresheafOfModules.{v, v', u', u} R₀
x : X ⟶ Y
x_1 : Y ⟶ Z
h :
  Eq (α :=
    (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
        (sheafify α (A := Functor.obj (presheafToSheaf J Ab) X.presheaf) (CategoryTheory.toSheafify J X.presheaf)).val ⟶
      (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
        (sheafify α (A := Functor.obj (presheafToSheaf J Ab) Z.presheaf) (CategoryTheory.toSheafify J Z.presheaf)).val)
    ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (SheafOfModules.Hom.val
        (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Z.presheaf) (x ≫ x_1)
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x ≫ x_1)) ⋯)))
    ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (SheafOfModules.Hom.val
        (CategoryStruct.comp (Y :=
          sheafify α (A := Functor.obj (presheafToSheaf J Ab) Y.presheaf) (CategoryTheory.toSheafify J Y.presheaf))
          (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) x
            ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x) ⋯)
          (sheafifyMap α (CategoryTheory.toSheafify J Y.presheaf) (CategoryTheory.toSheafify J Z.presheaf) x_1
            ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x_1) ⋯))))
⊢ Eq (α :=
    (sheafify α (A := Functor.obj (presheafToSheaf J Ab) X.presheaf) (CategoryTheory.toSheafify J X.presheaf)).val ⟶
      (sheafify α (A := Functor.obj (presheafToSheaf J Ab) Z.presheaf) (CategoryTheory.toSheafify J Z.presheaf)).val)
    (SheafOfModules.Hom.val
      (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Z.presheaf) (x ≫ x_1)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x ≫ x_1)) ⋯))
    (SheafOfModules.Hom.val
      (CategoryStruct.comp (Y :=
        sheafify α (A := Functor.obj (presheafToSheaf J Ab) Y.presheaf) (CategoryTheory.toSheafify J Y.presheaf))
        (sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) x
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x) ⋯)
        (sheafifyMap α (CategoryTheory.toSheafify J Y.presheaf) (CategoryTheory.toSheafify J Z.presheaf) x_1
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x_1) ⋯)))

Tactic:
apply (toPresheaf _).map_injective

Premises used: PresheafOfModules.toPresheaf, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
X Y Z : PresheafOfModules.{v, v', u', u} R₀
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α :=
    (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
        (sheafify α (A := Functor.obj (presheafToSheaf J Ab) X.presheaf) (CategoryTheory.toSheafify J X.presheaf)).val ⟶
      (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
        (sheafify α (A := Functor.obj (presheafToSheaf J Ab) Z.presheaf) (CategoryTheory.toSheafify J Z.presheaf)).val)
    ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
      (homMk
        (InducedCategory.Hom.hom
            (CategoryTheory.Functor.map (presheafToSheaf J AddCommGrpCat) ((toPresheaf R₀).map x)) ≫
          InducedCategory.Hom.hom
            (CategoryTheory.Functor.map (presheafToSheaf J AddCommGrpCat) ((toPresheaf R₀).map x_1)))
        ⋯))
    (CategoryStruct.comp (Y :=
      (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
        (sheafify α (A := Functor.obj (presheafToSheaf J Ab) Y.presheaf) (CategoryTheory.toSheafify J Y.presheaf)).val)
      ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
        (homMk
          (InducedCategory.Hom.hom
            (CategoryTheory.Functor.map (presheafToSheaf J AddCommGrpCat) ((toPresheaf R₀).map x)))
          ⋯))
      ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
        (homMk
          (InducedCategory.Hom.hom
            (CategoryTheory.Functor.map (presheafToSheaf J AddCommGrpCat) ((toPresheaf R₀).map x_1)))
          ⋯)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
⊢ ((sheafification α).obj P ⟶ F) ≃ (P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))

Tactic:
apply sheafifyHomEquiv

Premises used: PresheafOfModules.sheafifyHomEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
⊢ (toPresheaf R₀).map
      ((sheafificationHomEquiv α :
          (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
        f) =
    CategoryTheory.toSheafify J P.presheaf ≫ (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map f.val

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, rfl, PresheafOfModules.presheaf
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
rw :
  CategoryTheory.toSheafify J P.presheaf ≫ (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map f.val =
    CategoryStruct.comp (Y :=
      Functor.obj (presheafToSheaf J AddCommGrpCat ⋙ sheafToPresheaf J AddCommGrpCat) P.presheaf)
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J AddCommGrpCat)) P.presheaf)
      (CategoryTheory.Functor.map (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).map f))
⊢ Eq (α := (toPresheaf R₀).obj P ⟶ (toPresheaf R₀).obj ((restrictScalars α).obj ((SheafOfModules.forget R).obj F)))
    ((toPresheaf R₀).map
      ((sheafificationHomEquiv α :
          (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
        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 f))

Tactic:
rw [toPresheaf_map_sheafificationHomEquiv_def, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
⊢ CategoryTheory.toSheafify J P.presheaf ≫ (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map f.val =
    CategoryStruct.comp (Y :=
      Functor.obj (presheafToSheaf J AddCommGrpCat ⋙ sheafToPresheaf J AddCommGrpCat) P.presheaf)
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J AddCommGrpCat)) P.presheaf)
      (CategoryTheory.Functor.map (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).map f))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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
g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F)
obtain :
  ∀ (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)))
⊢ 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)
        g))
    ((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 g))

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

Premises used: PresheafOfModules.sheafificationHomEquiv, Equiv.surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
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 (α := P.presheaf ⟶ Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj F))
    (CategoryStruct.comp (Y :=
        Functor.obj (presheafToSheaf J AddCommGrpCat ⋙ sheafToPresheaf J AddCommGrpCat) P.presheaf)
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J AddCommGrpCat)) P.presheaf)
        (CategoryTheory.Functor.map (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).map f)) :
      P.presheaf ⟶ Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj F))
    ((toPresheaf R₀).map
        ((sheafificationHomEquiv α :
            (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
          f) :
      (toPresheaf R₀).obj P ⟶ (toPresheaf R₀).obj ((restrictScalars α).obj ((SheafOfModules.forget R).obj F)))

Tactic:
rfl