awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
⊢ Membership.mem (γ := Set (Sieve (unop (op U)))) ((zariskiTopology : (a : Scheme) → Set (Sieve a)) (unop (op U)))
    (Presheaf.equalizerSieve (FD := TypeCat.Fun) (F :=
      (zariskiTopology.yoneda.obj (glueData hf).glued).obj (P := Presheaf.IsSheaf zariskiTopology)) α β)

Tactic:
GrothendieckTopology.superset_covering _ ?_
      (zariskiTopology.intersection_covering (zariskiTopology.pullback_stable α mem)
        (zariskiTopology.pullback_stable β mem))

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, AlgebraicGeometry.Scheme.zariskiTopology, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.GrothendieckTopology.intersection_covering
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
V : Scheme
γ : V ⟶ U
Y_1 : Scheme
i :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
a : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i
fac₁ : a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i = γ ≫ α
Y : Scheme
j :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
b : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
fac₂ : b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = γ ≫ β
change : γ ≫ α = γ ≫ β
⊢ Sieve.arrows
    (Presheaf.equalizerSieve (FD := TypeCat.Fun) (F :=
      (zariskiTopology.yoneda.obj (glueData hf).glued).obj (P := Presheaf.IsSheaf zariskiTopology)) α β)
    γ

Tactic:
change γ ≫ α = γ ≫ β
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : U ⟶ (glueData hf).glued) → F.obj.obj (op U))
        α :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : U ⟶ (glueData hf).glued) → F.obj.obj (op U))
        β :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U))
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
V : Scheme
γ : V ⟶ U
Y_1 : Scheme
i :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
a : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i
fac₁ : a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i = γ ≫ α
Y : Scheme
j :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
b : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
fac₂ : b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = γ ≫ β
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (γ ≫ α) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (γ ≫ β) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))

Tactic:
simp [h]
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
V : Scheme
γ : V ⟶ U
Y_1 : Scheme
i :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
a : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i
fac₁ : a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i = γ ≫ α
Y : Scheme
j :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
b : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
fac₂ : b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = γ ≫ β
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
h₁ : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
⊢ a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i =
    b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j

Tactic:
apply comp_toGlued_eq

Premises used: AlgebraicGeometry.Scheme.LocalRepresentability.comp_toGlued_eq
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
V : Scheme
γ : V ⟶ U
Y_1 : Scheme
i :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
a : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i
fac₁ : a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i = γ ≫ α
Y : Scheme
j :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
b : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
fac₂ : b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = γ ≫ β
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
⊢ CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j

Tactic:
simpa [Scheme.GlueData.openCover_X, yonedaEquiv_naturality] using h

Premises used: AlgebraicGeometry.Scheme.GlueData.openCover_X, CategoryTheory.yonedaEquiv_naturality
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
rw :
  Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf) ∧
    Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)
⊢ IsIso (yonedaGluedToSheaf hf)

Tactic:
rw [← Sheaf.isLocallyBijective_iff_isIso (yonedaGluedToSheaf hf)]

Premises used: AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf, CategoryTheory.Sheaf.isLocallyBijective_iff_isIso
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
left : Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf)
right : Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)
⊢ Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf) ∧
    Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
⊢ Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
⊢ F.obj (P := Presheaf.IsSheaf zariskiTopology).IsRepresentable

Tactic:
⟨_, ⟨representableBy hf⟩⟩

Premises used: AlgebraicGeometry.Scheme.LocalRepresentability.representableBy, CategoryTheory.Functor.IsRepresentable.mk, Nonempty.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
⊢ Presieve.IsSheaf (propQCTopology P) F ↔
    Presieve.IsSheaf zariskiTopology F ∧
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))

Tactic:
⟨fun hF ↦ ⟨?_, fun {R S} f hf hs ↦ ?_⟩, fun ⟨hzar, hff⟩ ↦ ?_⟩

Premises used: CategoryTheory.Presieve.IsSheaf, AlgebraicGeometry.Scheme.propQCTopology, And.intro, Iff.intro, _private.0.AlgebraicGeometry.isSheaf_type_propQCTopology_iff.match_1
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
refine_1 : ∀ (hF : Presieve.IsSheaf (propQCTopology P) F), Presieve.IsSheaf zariskiTopology F
refine_2 :
  ∀ (hF : Presieve.IsSheaf (propQCTopology P) F) {R S : CommRingCat.{u}} (f : R ⟶ S) (hf : P (Spec.map f))
    (hs : Surjective (Spec.map f)), Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
refine_3 :
  (Presieve.IsSheaf zariskiTopology F ∧
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))) →
    ∀ (hzar : Presieve.IsSheaf zariskiTopology F)
      (hff :
        ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
          P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))),
      Presieve.IsSheaf (propQCTopology P) F
⊢ Presieve.IsSheaf (propQCTopology P) F ↔
    Presieve.IsSheaf zariskiTopology F ∧
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))

Tactic:
refine ⟨fun hF ↦ ⟨?_, fun {R S} f hf hs ↦ ?_⟩, fun ⟨hzar, hff⟩ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
⊢ Presieve.IsSheaf zariskiTopology F

Tactic:
Presieve.isSheaf_of_le _ zariskiTopology_le_propQCTopology hF

Premises used: AlgebraicGeometry.Scheme.zariskiTopology_le_propQCTopology, CategoryTheory.Presieve.isSheaf_of_le
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
⊢ Presieve.IsSheaf zariskiTopology F

Tactic:
exact Presieve.isSheaf_of_le _ zariskiTopology_le_propQCTopology hF

Premises used: AlgebraicGeometry.Scheme.zariskiTopology_le_propQCTopology, CategoryTheory.Presieve.isSheaf_of_le
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
refine_2 :
  Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
    (Sieve.generate (Presieve.singleton (Spec.map f)))
⊢ Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))

Tactic:
apply hF.isSheafFor

Premises used: CategoryTheory.Presieve.IsSheaf.isSheafFor
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
refine_2 :
  Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
    (Sieve.generate (Hom.cover (P := P) (Spec.map f) hf).presieve₀)
⊢ Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
    (Sieve.generate (Presieve.singleton (Spec.map f)))

Tactic:
rw [← Hom.presieve₀_cover _ hf]

Premises used: AlgebraicGeometry.Scheme.Hom.presieve₀_cover
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
⊢ Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
    (Sieve.generate (Hom.cover (P := P) (Spec.map f) hf).presieve₀)

Tactic:
Cover.mem_propQCTopology _

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.Cover.mem_propQCTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
⊢ Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
    (Sieve.generate (Hom.cover (P := P) (Spec.map f) hf).presieve₀)

Tactic:
exact Cover.mem_propQCTopology _

Premises used: AlgebraicGeometry.Scheme.Cover.mem_propQCTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
refine_3 : ∀ ⦃X : Scheme.{u}⦄ (E : (propQCPrecoverage P).ZeroHypercover X), Presieve.IsSheafFor F E.presieve₀
⊢ Presieve.IsSheaf (propQCTopology P) F

Tactic:
rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small.{u}]