awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
⊢ pushforwardComp φ (𝟙 R) = isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor
have w : ∀ (x : PresheafOfModules.{v, v₂, u₂, u} R) (X : Cᵒᵖ)
  (x_1 : (↑((Functor.obj (pushforward (F := 𝟭 D) (𝟙 R) ⋙ pushforward φ) x).obj X) : Type v)),
  Eq (α := (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
    ((ModuleCat.Hom.hom (Hom.app (NatTrans.app (Iso.hom (pushforwardComp φ (𝟙 R))) x) X) :
          (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).obj X) : Type v)) →
            (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
        x_1 :
      (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
    ((ModuleCat.Hom.hom
            (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x).app X) :
          (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).obj X) : Type v)) →
            (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
        x_1 :
      (↑(((pushforward (φ ≫ F.op.whiskerLeft (𝟙 R))).obj x).obj X) : Type v))
Tactic: ext
-- 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
M₀ : PresheafOfModules.{v, v', u', u} R₀
⊢ sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
      ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯ =
    𝟙 (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf))
have h : SheafOfModules.Hom.val
    (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
      ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) sorry) =
  SheafOfModules.Hom.val
    (𝟙 (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf)))
Tactic: ext1
-- 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
M₀ : PresheafOfModules.{v, v', u', u} R₀
⊢ 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)))
have 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₀)) sorry)) =
  (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: apply (toPresheaf _).map_injective
-- 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
M₀ : PresheafOfModules.{v, v', u', u} R₀
⊢ (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))))
have h : (toPresheaf (R.obj (P := Presheaf.IsSheaf J))).map
    (homMk (𝟙 ((Functor.obj (presheafToSheaf J AddCommGrpCat) ((toPresheaf R₀).obj M₀)).obj (P := Presheaf.IsSheaf J)))
      sorry) =
  𝟙
    ((toPresheaf (R.obj (P := Presheaf.IsSheaf J))).obj
      (sheafify α (A := Functor.obj (presheafToSheaf J Ab) M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf)).val)
Tactic: simp
-- 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
X Y Z : PresheafOfModules.{v, v', u', u} R₀
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ 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) ⋯))
have 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)) sorry))
  (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) sorry)
      (sheafifyMap α (CategoryTheory.toSheafify J Y.presheaf) (CategoryTheory.toSheafify J Z.presheaf) x_1
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x_1) sorry)))
Tactic: ext1
-- 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
X Y Z : PresheafOfModules.{v, v', u', u} R₀
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ 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) ⋯)))
have 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)) sorry)))
  ((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) sorry)
        (sheafifyMap α (CategoryTheory.toSheafify J Y.presheaf) (CategoryTheory.toSheafify J Z.presheaf) x_1
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x_1) sorry))))
Tactic: apply (toPresheaf _).map_injective
-- 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 (α := (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))
have 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))
Tactic: rw [toPresheaf_map_sheafificationHomEquiv_def, Adjunction.homEquiv_unit]
-- 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
g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj 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))
have 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)))
Tactic: obtain ⟨f, rfl⟩ := (sheafificationHomEquiv α).surjective g
Cleared hypotheses: g
-- 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₀ 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 (α := (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)
have 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))
Tactic: apply (SheafOfModules.toSheaf _).map_injective
-- 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₀ 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)
    ((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))
have 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))
Tactic: simp only [Functor.comp_obj, Functor.map_comp]
-- 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₀ 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)
    ((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))
have 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)
Tactic: rw [toSheaf_map_sheafificationHomEquiv_symm α (f ≫ g),
          toSheaf_map_sheafificationHomEquiv_symm α g, Functor.map_comp]