awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify 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))
M_1 N P : SheafOfModules R
inst_4 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_5 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
inst_6 :
  ∀ (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))
M : SheafOfModules R
q : LocalGeneratorsData.{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.LocalGeneratorsData.coversTop
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify 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))
M_1 N P : SheafOfModules R
inst_4 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_5 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
inst_6 :
  ∀ (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))
M : SheafOfModules R
q : LocalGeneratorsData.{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.LocalGeneratorsData.coversTop
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify 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))
M_1 N P : SheafOfModules R
inst_4 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_5 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
inst_6 :
  ∀ (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))
M : SheafOfModules R
q : LocalGeneratorsData.{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.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify 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))
M_1 N P : SheafOfModules R
inst_4 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_5 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
inst_6 :
  ∀ (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))
M : SheafOfModules R
q : LocalGeneratorsData.{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.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify 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))
M_1 N P : SheafOfModules R
inst_4 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_5 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
inst_6 :
  ∀ (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))
M : SheafOfModules R
q : LocalGeneratorsData.{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.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
F : D ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ (X : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              forget (ModuleCat.{v, u} (↑(R.obj X) : Type u)) (FC :=
                fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier)).sections :
        Type (max u₂ v))
c : Cone F
inst_3 : HasLimitsOfShape.{v₂, u₂, v, v + 1} D AddCommGrpCat
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
G : D ⥤ Sheaf J AddCommGrpCat :=
  { obj := fun (j : D) ↦ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) (F.obj j).presheaf ⋯,
    map := fun {X Y : D} (φ : X ⟶ Y) ↦ { hom := (toPresheaf R).map (F.map φ) }, map_id := ⋯, map_comp := ⋯ }
⊢ Presheaf.IsSheaf J c.pt.presheaf

Tactic:
Sheaf.isSheaf_of_isLimit G _ (isLimitOfPreserves (toPresheaf R) hc)

Premises used: CategoryTheory.Sheaf.isSheaf_of_isLimit, PresheafOfModules.toPresheaf, CategoryTheory.Limits.isLimitOfPreserves, PresheafOfModules.presheaf
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
F : D ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ (X : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              forget (ModuleCat.{v, u} (↑(R.obj X) : Type u)) (FC :=
                fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier)).sections :
        Type (max u₂ v))
c : Cone F
inst_3 : HasLimitsOfShape.{v₂, u₂, v, v + 1} D AddCommGrpCat
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
G : D ⥤ Sheaf J AddCommGrpCat :=
  { obj := fun (j : D) ↦ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) (F.obj j).presheaf ⋯,
    map := fun {X Y : D} (φ : X ⟶ Y) ↦ { hom := (toPresheaf R).map (F.map φ) }, map_id := ⋯, map_comp := ⋯ }
⊢ Presheaf.IsSheaf J c.pt.presheaf

Tactic:
exact Sheaf.isSheaf_of_isLimit G _ (isLimitOfPreserves (toPresheaf R) hc)

Premises used: CategoryTheory.Sheaf.isSheaf_of_isLimit, PresheafOfModules.toPresheaf, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Sheaf J RingCat
F : D ⥤ SheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ (X : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              CategoryTheory.forget (ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (FC :=
                fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u))
                  (RingHom.id (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
                (CC := ModuleCat.carrier)).sections :
        Type (max u₂ v))
inst_3 : HasLimitsOfShape.{v₂, u₂, v, v + 1} D AddCommGrpCat
X : Cᵒᵖ
⊢ Small.{v, max u₂ v}
    (↑(((F ⋙ forget R) ⋙ PresheafOfModules.evaluation (R.obj (P := Presheaf.IsSheaf J)) X) ⋙
            CategoryTheory.forget (ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (FC :=
              fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u))
                (RingHom.id (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
              (CC := ModuleCat.carrier)).sections :
      Type (max u₂ v))

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Sheaf J RingCat
F : D ⥤ SheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ (X : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              CategoryTheory.forget (ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (FC :=
                fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u))
                  (RingHom.id (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
                (CC := ModuleCat.carrier)).sections :
        Type (max u₂ v))
inst_3 : HasLimitsOfShape.{v₂, u₂, v, v + 1} D AddCommGrpCat
⊢ HasLimit F

Tactic:
hasLimit_of_created F (forget _)

Premises used: CategoryTheory.hasLimit_of_created, SheafOfModules.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Sheaf J RingCat
F : D ⥤ SheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ (X : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              CategoryTheory.forget (ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (FC :=
                fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u))
                  (RingHom.id (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (↑x1 : Type v) (↑x2 : Type v))
                (CC := ModuleCat.carrier)).sections :
        Type (max u₂ v))
inst_3 : HasLimitsOfShape.{v₂, u₂, v, v + 1} D AddCommGrpCat
X : Cᵒᵖ
⊢ PreservesLimit F (forget R ⋙ PresheafOfModules.evaluation (R.obj (P := Presheaf.IsSheaf J)) X)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Sheaf J RingCat
⊢ HasFiniteLimits (SheafOfModules.{v, v₁, u₁, u} R)

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Sheaf J RingCat
⊢ PreservesFiniteLimits (toSheaf R ⋙ sheafToPresheaf J AddCommGrpCat)

Tactic:
comp_preservesFiniteLimits (SheafOfModules.forget.{v} R) (PresheafOfModules.toPresheaf R.obj)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.FullSubcategory.obj, SheafOfModules.toSheaf, PresheafOfModules.toPresheaf, CategoryTheory.Limits.comp_preservesFiniteLimits, PresheafOfModules.presheaf, SheafOfModules.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Sheaf J RingCat
⊢ PreservesFiniteLimits (toSheaf R)

Tactic:
preservesFiniteLimits_of_reflects_of_preserves _ (sheafToPresheaf _ _)

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
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 :
  inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) =
    inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α)
⊢ inverseImage J.W (toPresheaf R₀) = inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α)

Tactic:
rw [J.W_eq_inverseImage_isomorphisms]

Premises used: CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
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
h :
  ∀ ⦃P Q : PresheafOfModules.{v, v', u', u} R₀⦄ (f : P ⟶ Q),
    inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) f ↔
      inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α) f
⊢ inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) =
    inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α)

Tactic:
ext P Q f

Premises used: CategoryTheory.MorphismProperty.Q
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
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₀
f : P ⟶ Q
h :
  IsIso (X := Functor.obj (presheafToSheaf J Ab) ((toPresheaf R₀).obj P))
      (CategoryTheory.Functor.map (presheafToSheaf J Ab) ((toPresheaf R₀).map f)) ↔
    IsIso ((SheafOfModules.toSheaf R).map ((sheafification α).map f))
⊢ inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) f ↔
    inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α) f

Tactic:
simp only [inverseImage_iff, isomorphisms.iff,
    ← isIso_iff_of_reflects_iso _ (SheafOfModules.toSheaf.{v} R)]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.MorphismProperty.inverseImage_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
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₀
f : P ⟶ Q
⊢ IsIso (X := Functor.obj (presheafToSheaf J Ab) ((toPresheaf R₀).obj P))
      (CategoryTheory.Functor.map (presheafToSheaf J Ab) ((toPresheaf R₀).map f)) ↔
    IsIso ((SheafOfModules.toSheaf R).map ((sheafification α).map f))

Tactic:
(isomorphisms _).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso (sheafificationCompToSheaf.{v} α)).app (Arrow.mk f))

Premises used: PresheafOfModules.sheafificationCompToSheaf, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
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₀
f : P ⟶ Q
⊢ IsIso (X := Functor.obj (presheafToSheaf J Ab) ((toPresheaf R₀).obj P))
      (CategoryTheory.Functor.map (presheafToSheaf J Ab) ((toPresheaf R₀).map f)) ↔
    IsIso ((SheafOfModules.toSheaf R).map ((sheafification α).map f))

Tactic:
exact (isomorphisms _).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso (sheafificationCompToSheaf.{v} α)).app (Arrow.mk f))
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
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 :
  (sheafification α).IsLocalization
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α))
⊢ (sheafification α).IsLocalization (MorphismProperty.inverseImage J.W (toPresheaf R₀))

Tactic:
rw [inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms α]

Premises used: PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms