awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := Iso.symm (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)))
h' : Abelian.image f ≅
  kernel (X := free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)))
    (GeneratingSections.π (generatorsOfIsCokernelFree f g H H') :
      free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M) :=
  kernel.mapIso (cokernel.π f) (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) (Iso.refl (free σ)) h ⋯
⊢ Eq (α := free ι ⟶ M) (f ≫ GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) 0

Tactic:
simp [H]
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := Iso.symm (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)))
h' : Abelian.image f ≅
  kernel (X := free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)))
    (GeneratingSections.π (generatorsOfIsCokernelFree f g H H') :
      free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M) :=
  kernel.mapIso (cokernel.π f) (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) (Iso.refl (free σ)) h ⋯
⊢ Abelian.factorThruImage f ≫ h'.hom = kernel.lift (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) f ⋯

Tactic:
have comp_aux : Abelian.factorThruImage f ≫ h'.hom =
      (kernel.lift (generatorsOfIsCokernelFree f g H H').π f (by simp [H])) :=
        equalizer.hom_ext <| by simp [h']
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := Iso.symm (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)))
h' : Abelian.image f ≅
  kernel (X := free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)))
    (GeneratingSections.π (generatorsOfIsCokernelFree f g H H') :
      free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M) :=
  kernel.mapIso (cokernel.π f) (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) (Iso.refl (free σ)) h ⋯
comp_aux :
  Abelian.factorThruImage f ≫ h'.hom = kernel.lift (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) f ⋯
⊢ Epi (Abelian.factorThruImage f ≫ h'.hom)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
P : M.Presentation
⊢ Eq (α := free P.relations.I ⟶ M)
    (CategoryStruct.comp (Y := kernel P.generators.π)
          ((Equiv.symm (kernel P.generators.π).freeHomEquiv :
              (a : P.relations.I → (kernel P.generators.π).sections) → free P.relations.I ⟶ kernel P.generators.π)
            P.relations.s)
          (kernel.ι P.generators.π) ≫
        P.generators.π :
      free P.relations.I ⟶ M)
    (0 : free P.relations.I ⟶ M)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ_1 : Type u
M N : SheafOfModules R
f : M ⟶ N
inst_5 : IsIso f
σ : M.Presentation
⊢ kernel (σ.generators.π ≫ f) = kernel (σ.generators.ofEpi f).π

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
C' : Type u₂
inst_5 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_6 : HasSheafify J' AddCommGrpCat
inst_7 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.184806}) ↦
    (↑x1 : Type ?u.184806) →+ (↑x2 : Type ?u.184806)) (CA := AddCommGrpCat.carrier)
inst_8 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst_9 : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ PreservesColimitsOfSize.{0, 0, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F

Tactic:
preservesColimitsOfSize_shrink _

Premises used: CategoryTheory.Limits.preservesColimitsOfSize_shrink
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
C' : Type u₂
inst_4 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_5 : HasSheafify J' AddCommGrpCat
inst_6 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_7 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst_8 : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ Eq (α := free P.relations.I ⟶ F.obj M)
    (CategoryStruct.comp (Y := free P.generators.I)
        (P.mapRelations F η : Quiver.Hom (V := SheafOfModules S) (free P.relations.I) (free P.generators.I))
        (P.mapGenerators F η : free P.generators.I ⟶ F.obj M) :
      free P.relations.I ⟶ F.obj M)
    (0 : free P.relations.I ⟶ F.obj M)

Tactic:
simp only [mapRelations, mapGenerators, Category.assoc, Iso.inv_hom_id_assoc,
    ← Functor.map_comp, kernel.condition, Functor.map_zero, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, SheafOfModules.Presentation.mapGenerators, CategoryTheory.Limits.kernel.condition, CategoryTheory.Iso.inv_hom_id_assoc, SheafOfModules.Presentation.mapRelations, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
C' : Type u₂
inst_5 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_6 : HasSheafify J' AddCommGrpCat
inst_7 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_8 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst_9 : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [Presentation.mapRelations, Presentation.mapGenerators, ← Functor.map_comp]

Premises used: SheafOfModules.Presentation.mapGenerators, SheafOfModules.Presentation.mapRelations, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
C' : Type u₂
inst_4 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_5 : HasSheafify J' AddCommGrpCat
inst_6 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_7 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst_8 : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ Eq (α := free (GeneratingSections.I (generators (P.map F η) : (F.obj M).GeneratingSections)) ⟶ F.obj M)
    (GeneratingSections.π (generators (P.map F η)) :
      free (GeneratingSections.I (generators (P.map F η) : (F.obj M).GeneratingSections)) ⟶ F.obj M)
    (Iso.hom (mapFreeIso F P.generators.I η) ≫ F.map P.generators.π : free P.generators.I ⟶ F.obj M)

Tactic:
(F.obj M).freeHomEquiv.symm_apply_eq.mpr rfl

Premises used: Iff.mpr, Equiv.symm_apply_eq, SheafOfModules.freeHomEquiv, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
X : C
⊢ Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X ∈
    (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering (fun Y hY H ↦ ?_) (q.coversTop X)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, SheafOfModules.QuasicoherentData.coversTop
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
X : C
refine :
  ∀ (Y : C) (hY : Y ⟶ X) (H : Sieve.arrows (Sieve.ofObjects q.X X) hY),
    Sieve.arrows
      (Sieve.ofObjects
        (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X)
      hY
⊢ Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X ∈
    (J : (a : C) → Set (Sieve a)) X

Tactic:
refine J.superset_covering (fun Y hY H ↦ ?_) (q.coversTop X)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, SheafOfModules.QuasicoherentData.coversTop
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
X Y : C
hY : Y ⟶ X
H : Sieve.arrows (Sieve.ofObjects q.X X) hY
obtain :
  ∀ (i : q.I) (hi : Y ⟶ q.X i),
    Sieve.arrows
      (Sieve.ofObjects
        (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X)
      hY
⊢ Sieve.arrows
    (Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X)
    hY

Tactic:
obtain ⟨i, ⟨hi⟩⟩ := (Sieve.mem_ofObjects_iff ..).mp H

Premises used: CategoryTheory.Sieve.mem_ofObjects_iff, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
X Y : C
hY : Y ⟶ X
H : Sieve.arrows (Sieve.ofObjects q.X X) hY
i : q.I
hi : Y ⟶ q.X i
⊢ q.X i =
    (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯))
      (Subtype.mk (p := fun (x : C) ↦ x ∈ Set.range q.X) (q.X i) ⋯)

Tactic:
grind
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
X Y : C
hY : Y ⟶ X
H : Sieve.arrows (Sieve.ofObjects q.X X) hY
i : q.I
hi : Y ⟶ q.X i
⊢ Sieve.arrows
    (Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X)
    hY

Tactic:
exact ⟨⟨_, i, rfl⟩, ⟨hi ≫ eqToHom (by grind)⟩⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
inst_4 : q.IsFinitePresentation
dsimp : ∀ (i : q.I), (q.presentation i).generators.IsFiniteType
⊢ ∀ (i : q.localGeneratorsData.I), (q.localGeneratorsData.generators i).IsFiniteType

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
inst_4 : q.IsFinitePresentation
⊢ ∀ (i : q.I), (q.presentation i).generators.IsFiniteType

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).HasSheafCompose
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
inst_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
q : QuasicoherentData.{u_1, u, v₁, u₁} M
⊢ M.IsQuasicoherent

Tactic:
⟨⟨q.shrink⟩⟩

Premises used: Nonempty.intro, SheafOfModules.IsQuasicoherent.mk, SheafOfModules.QuasicoherentData.shrink