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
P₀ Q₀ : PresheafOfModules.{v, v', u', u} R₀
N : SheafOfModules.{v, v', u', u} R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
a :
  Eq (α := (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)
    ((SheafOfModules.toSheaf R).map
      ((Equiv.symm (sheafificationHomEquiv α) :
          (a : P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N) → (sheafification α).obj P₀ ⟶ N)
        (f ≫ g)))
    ((SheafOfModules.toSheaf R).map
      ((sheafification α).map f ≫
        (Equiv.symm (sheafificationHomEquiv α) :
            (a : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N) → (sheafification α).obj Q₀ ⟶ N)
          g))
⊢ Eq (α := (sheafification α).obj P₀ ⟶ N)
    ((Equiv.symm (sheafificationHomEquiv α) :
          (a : P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N) → (sheafification α).obj P₀ ⟶ N)
        (f ≫ g) :
      (sheafification α).obj P₀ ⟶ N)
    ((sheafification α).map f ≫
        (Equiv.symm (sheafificationHomEquiv α) :
            (a : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N) → (sheafification α).obj Q₀ ⟶ N)
          g :
      (sheafification α).obj P₀ ⟶ N)

Tactic:
apply (SheafOfModules.toSheaf _).map_injective

Premises used: SheafOfModules.toSheaf, 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
P₀ Q₀ : PresheafOfModules.{v, v', u', u} R₀
N : SheafOfModules.{v, v', u', u} R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
a :
  Eq (α := (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)
    ((SheafOfModules.toSheaf R).map
      ((Equiv.symm (sheafificationHomEquiv α) :
          (a : P₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj N)) → (sheafification α).obj P₀ ⟶ N)
        (f ≫ g)))
    ((SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      (SheafOfModules.toSheaf R).map
        ((Equiv.symm (sheafificationHomEquiv α) :
            (a : Q₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj N)) → (sheafification α).obj Q₀ ⟶ N)
          g))
⊢ Eq (α := (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)
    ((SheafOfModules.toSheaf R).map
      ((Equiv.symm (sheafificationHomEquiv α) :
          (a : P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N) → (sheafification α).obj P₀ ⟶ N)
        (f ≫ g)))
    ((SheafOfModules.toSheaf R).map
      ((sheafification α).map f ≫
        (Equiv.symm (sheafificationHomEquiv α) :
            (a : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N) → (sheafification α).obj Q₀ ⟶ N)
          g))

Tactic:
simp only [Functor.comp_obj, Functor.map_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp
-- 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₀ Q₀ : PresheafOfModules.{v, v', u', u} R₀
N : SheafOfModules.{v, v', u', u} R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
a :
  Eq (α := (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)
    ((Equiv.symm
            (Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat) P₀.presheaf
              ((SheafOfModules.toSheaf R).obj N)) :
          (a : P₀.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj N)) →
            (presheafToSheaf J AddCommGrpCat).obj P₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N)
        ((toPresheaf R₀).map f ≫ (toPresheaf R₀).map g) :
      Functor.obj (presheafToSheaf J AddCommGrpCat) P₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N)
    ((SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
        (Equiv.symm
              (Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat) Q₀.presheaf
                ((SheafOfModules.toSheaf R).obj N)) :
            (a : Q₀.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj N)) →
              (presheafToSheaf J AddCommGrpCat).obj Q₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N)
          ((toPresheaf R₀).map g) :
      (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)
⊢ Eq (α := (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)
    ((SheafOfModules.toSheaf R).map
      ((Equiv.symm (sheafificationHomEquiv α) :
          (a : P₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj N)) → (sheafification α).obj P₀ ⟶ N)
        (f ≫ g)))
    ((SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      (SheafOfModules.toSheaf R).map
        ((Equiv.symm (sheafificationHomEquiv α) :
            (a : Q₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj N)) → (sheafification α).obj Q₀ ⟶ N)
          g))

Tactic:
rw [toSheaf_map_sheafificationHomEquiv_symm α (f ≫ g),
          toSheaf_map_sheafificationHomEquiv_symm α g, Functor.map_comp]

Premises used: PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp
-- 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₀ Q₀ : PresheafOfModules.{v, v', u', u} R₀
N : SheafOfModules.{v, v', u', u} R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
⊢ Eq (α := (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)
    ((Equiv.symm
            (Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat) P₀.presheaf
              ((SheafOfModules.toSheaf R).obj N)) :
          (a : P₀.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj N)) →
            (presheafToSheaf J AddCommGrpCat).obj P₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N)
        ((toPresheaf R₀).map f ≫ (toPresheaf R₀).map g) :
      Functor.obj (presheafToSheaf J AddCommGrpCat) P₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N)
    ((SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
        (Equiv.symm
              (Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat) Q₀.presheaf
                ((SheafOfModules.toSheaf R).obj N)) :
            (a : Q₀.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj N)) →
              (presheafToSheaf J AddCommGrpCat).obj Q₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N)
          ((toPresheaf R₀).map g) :
      (SheafOfModules.toSheaf R).obj ((sheafification α).obj P₀) ⟶ (SheafOfModules.toSheaf R).obj N)

Tactic:
apply (CategoryTheory.sheafificationAdjunction J
          AddCommGrpCat.{v}).homEquiv_naturality_left_symm
-- 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₀
M N : SheafOfModules.{v, v', u', u} R
f : (sheafification α).obj P₀ ⟶ M
g : M ⟶ N
a :
  Eq (α := (toPresheaf R₀).obj P₀ ⟶ (toPresheaf R₀).obj ((SheafOfModules.forget R ⋙ restrictScalars α).obj N))
    ((toPresheaf R₀).map
      ((sheafificationHomEquiv α :
          (a : (sheafification α).obj P₀ ⟶ N) → P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N)
        (f ≫ g)))
    ((toPresheaf R₀).map
      ((sheafificationHomEquiv α :
            (a : (sheafification α).obj P₀ ⟶ M) → P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj M)
          f ≫
        (SheafOfModules.forget R ⋙ restrictScalars α).map g))
⊢ Eq (α := P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N)
    ((sheafificationHomEquiv α :
          (a : (sheafification α).obj P₀ ⟶ N) → P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N)
        (f ≫ g) :
      P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N)
    ((sheafificationHomEquiv α :
            (a : (sheafification α).obj P₀ ⟶ M) → P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj M)
          f ≫
        (SheafOfModules.forget R ⋙ restrictScalars α).map g :
      P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N)

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
P₀ : PresheafOfModules.{v, v', u', u} R₀
M N : SheafOfModules.{v, v', u', u} R
f : (sheafification α).obj P₀ ⟶ M
g : M ⟶ N
a a₁ :
  Eq (α := (toPresheaf R₀).obj P₀ ⟶ (toPresheaf R₀).obj ((SheafOfModules.forget R ⋙ restrictScalars α).obj N))
    ((Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat) P₀.presheaf
            ((SheafOfModules.toSheaf R).obj N) :
          (a : (presheafToSheaf J AddCommGrpCat).obj P₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N) →
            P₀.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj N))
        ((SheafOfModules.toSheaf R).map (f ≫ g)) :
      P₀.presheaf ⟶ Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj N))
    ((Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat) P₀.presheaf
            ((SheafOfModules.toSheaf R).obj N) :
          (a : (presheafToSheaf J AddCommGrpCat).obj P₀.presheaf ⟶ (SheafOfModules.toSheaf R).obj N) →
            P₀.presheaf ⟶ (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj N))
        ((SheafOfModules.toSheaf R).map (f ≫ g)) :
      P₀.presheaf ⟶ Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj N))
⊢ Eq (α := (toPresheaf R₀).obj P₀ ⟶ (toPresheaf R₀).obj ((SheafOfModules.forget R ⋙ restrictScalars α).obj N))
    ((toPresheaf R₀).map
      ((sheafificationHomEquiv α :
          (a : (sheafification α).obj P₀ ⟶ N) → P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N)
        (f ≫ g)))
    ((toPresheaf R₀).map
      ((sheafificationHomEquiv α :
            (a : (sheafification α).obj P₀ ⟶ M) → P₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj M)
          f ≫
        (SheafOfModules.forget R ⋙ restrictScalars α).map g))

Tactic:
erw [toPresheaf_map_sheafificationHomEquiv]

Premises used: PresheafOfModules.toPresheaf_map_sheafificationHomEquiv
-- 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 ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj F)
    ((Adjunction.homEquiv (sheafificationAdjunction α) P F :
          (a : (sheafification α).obj P ⟶ F) → P ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj F)
        f :
      P ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj F)
    ((sheafificationHomEquiv α :
          (a : (sheafification α).obj P ⟶ F) → P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))
        f :
      P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))

Tactic:
rfl

Premises used: PresheafOfModules.restrictScalarsObj, 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
M₀ : PresheafOfModules.{v, v', u', u} R₀
⊢ Eq (α :=
    (toPresheaf R₀).obj (Functor.obj (𝟭 (PresheafOfModules.{v, v', u', u} R₀)) M₀) ⟶
      (toPresheaf R₀).obj ((sheafification α ⋙ SheafOfModules.forget R ⋙ restrictScalars α).obj M₀))
    ((toPresheaf R₀).map (NatTrans.app (Adjunction.unit (sheafificationAdjunction α)) M₀))
    (CategoryTheory.toSheafify J M₀.presheaf)

Tactic:
rfl

Premises used: AddMonoidHom.mk', 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
M : SheafOfModules.{v, v', u', u} R
⊢ Eq (α :=
    (SheafOfModules.toSheaf R).obj ((sheafification α).obj ((SheafOfModules.forget R ⋙ restrictScalars α).obj M)) ⟶
      (SheafOfModules.toSheaf R).obj (Functor.obj (𝟭 (SheafOfModules.{v, v', u', u} R)) M))
    ((Equiv.symm
            (Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat)
              ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf
              ((SheafOfModules.toSheaf R).obj (Functor.obj (𝟭 (SheafOfModules.{v, v', u', u} R)) M))) :
          (a :
              ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf ⟶
                (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj ((𝟭 (SheafOfModules R)).obj M))) →
            (presheafToSheaf J AddCommGrpCat).obj ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf ⟶
              (SheafOfModules.toSheaf R).obj ((𝟭 (SheafOfModules R)).obj M))
        ((toPresheaf R₀).map (𝟙 ((SheafOfModules.forget R ⋙ restrictScalars α).obj M))) :
      Functor.obj (presheafToSheaf J AddCommGrpCat) ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf ⟶
        (SheafOfModules.toSheaf R).obj (Functor.obj (𝟭 (SheafOfModules.{v, v', u', u} R)) M))
    ((Equiv.symm
            (Adjunction.homEquiv (CategoryTheory.sheafificationAdjunction J AddCommGrpCat)
              (Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj M))
              ((SheafOfModules.toSheaf R).obj M)) :
          (a :
              (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M) ⟶
                (sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M)) →
            (presheafToSheaf J AddCommGrpCat).obj
                ((sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M)) ⟶
              (SheafOfModules.toSheaf R).obj M)
        (𝟙 (Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj M))) :
      Functor.obj (presheafToSheaf J AddCommGrpCat)
          (Functor.obj (sheafToPresheaf J AddCommGrpCat) ((SheafOfModules.toSheaf R).obj M)) ⟶
        (SheafOfModules.toSheaf R).obj M)

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
⊢ (sheafification α).IsLeftAdjoint

Tactic:
(sheafificationAdjunction α).isLeftAdjoint

Premises used: PresheafOfModules.sheafificationAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- 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
rw :
  ∀ (X : SheafOfModules.{v, v', u', u} R),
    IsIso (X := ((SheafOfModules.forget R ⋙ restrictScalars α) ⋙ sheafification α).obj X)
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction α)) X)
⊢ IsIso (X := (SheafOfModules.forget R ⋙ restrictScalars α) ⋙ sheafification α)
    (Adjunction.counit (sheafificationAdjunction α))

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- 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
F : SheafOfModules.{v, v', u', u} R
rw :
  IsIso (X := (SheafOfModules.toSheaf R).obj (((SheafOfModules.forget R ⋙ restrictScalars α) ⋙ sheafification α).obj F))
    ((SheafOfModules.toSheaf R).map (NatTrans.app (Adjunction.counit (sheafificationAdjunction α)) F))
⊢ IsIso (X := ((SheafOfModules.forget R ⋙ restrictScalars α) ⋙ sheafification α).obj F)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction α)) F)

Tactic:
rw [← isIso_iff_of_reflects_iso _ (SheafOfModules.toSheaf.{v} R)]