awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
F : CategoryTheory.Functor.{u, v, u + 1, v + 1} Schemeᵒᵖ (Type v)
ι : Type u_1
inst : Small.{u, u_1} ι
inst_1 : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this :
  ∀ (i : ι),
    Mono (X := (unop ∘ X) i) (Y :=
      Cocone.pt (F := Discrete.functor (unop ∘ X)) (Sigma.cocone (Discrete.functor (unop ∘ X))))
      (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Presieve.IsSheafFor (X :=
    Cocone.pt (F := Discrete.functor fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X)))) F
    (Presieve.ofArrows (fun (x : ι) ↦ unop (X x)) (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X)))))

Tactic:
hF.isSheafFor _ (sigmaOpenCover _).mem_grothendieckTopology

Premises used: AlgebraicGeometry.sigmaOpenCover, CategoryTheory.Presieve.IsSheaf.isSheafFor, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
F : CategoryTheory.Functor.{u, v, u + 1, v + 1} Schemeᵒᵖ (Type v)
ι : Type u_1
inst : Small.{u, u_1} ι
inst_1 : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this :
  ∀ (i : ι),
    Mono (X := (unop ∘ X) i) (Y :=
      Cocone.pt (F := Discrete.functor (unop ∘ X)) (Sigma.cocone (Discrete.functor (unop ∘ X))))
      (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Presieve.IsSheafFor (X :=
    Cocone.pt (F := Discrete.functor fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X)))) F
    (Presieve.ofArrows (fun (x : ι) ↦ unop (X x)) (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X)))))

Tactic:
exact hF.isSheafFor _ (sigmaOpenCover _).mem_grothendieckTopology

Premises used: AlgebraicGeometry.sigmaOpenCover, CategoryTheory.Presieve.IsSheaf.isSheafFor, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
rw :
  Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app))
⊢ Membership.mem (γ := Set (Sieve c.pt)) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) c.pt)
    (Sieve.ofArrows F.obj c.ι.app)

Tactic:
rw [← GrothendieckTopology.pullback_mem_iff_of_isIso (i := iso.inv)]

Premises used: CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
apply : Sieve (colimit F)
apply₁ : Sieve.ofArrows F.obj (colimit.ι F) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)
apply₂ :
  Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.ofArrows F.obj (colimit.ι F))
⊢ Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app))

Tactic:
apply GrothendieckTopology.superset_covering _ ?_ ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Sieve (colimit F)

Tactic:
exact Sieve.ofArrows _ (colimit.ι F)

Premises used: CategoryTheory.Sieve.ofArrows, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
rw : Presieve.ofArrows F.obj (colimit.ι F) ≤ (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)).arrows
⊢ Sieve.ofArrows F.obj (colimit.ι F) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)

Tactic:
rw [Sieve.ofArrows, Sieve.generate_le_iff]

Premises used: CategoryTheory.Sieve.ofArrows, CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
Y : Scheme
i : J
⊢ 𝟙 (F.obj i) ≫ c.ι.app i = colimit.ι F i ≫ iso.inv

Tactic:
simp [iso]
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
Y : Scheme
i : J
⊢ (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)).arrows (colimit.ι F i)

Tactic:
exact ⟨_, 𝟙 _, c.ι.app i, ⟨i⟩, by simp [iso]⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.ofArrows F.obj (colimit.ι F))

Tactic:
(Scheme.IsLocallyDirected.openCover F).mem_grothendieckTopology

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ Scheme.forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{u_1, u_2} J
inst_4 : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Membership.mem (γ := Set (Sieve (colimit F))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (colimit F))
    (Sieve.ofArrows F.obj (colimit.ι F))

Tactic:
exact (Scheme.IsLocallyDirected.openCover F).mem_grothendieckTopology

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.openCover, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
⊢ PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F

Tactic:
have : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F :=
    preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology hF
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
⊢ PreservesLimitsOfShape (Discrete 𝒰.I₀) F

Tactic:
have : PreservesLimitsOfShape (Discrete 𝒰.I₀) F :=
    preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology hF
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this_1 : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
rw :
  Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
    Presieve.IsSheafFor F
      (Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt)
        (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f))
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
    Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)

Tactic:
rw [← Presieve.isSheafFor_sigmaDesc_iff 𝒰.f (coproductIsCoproduct _)
    (FinitaryExtensive.isVanKampen_finiteCoproducts (coproductIsCoproduct _)).isUniversal]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts, CategoryTheory.IsVanKampenColimit.isUniversal, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this_1 : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
a :
  Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f =
    Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt) (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f) ↔
    Presieve.IsSheafFor F
      (Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt)
        (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f))

Tactic:
congr!
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this_1 : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
a :
  Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f) =
    Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt) (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
⊢ Presieve.ofArrows 𝒰.sigma (P := P).X 𝒰.sigma (P := P).f =
    Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt) (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)

Tactic:
rw [← PreZeroHypercover.presieve₀, 𝒰.presieve₀_sigma]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, AlgebraicGeometry.Scheme.Cover.presieve₀_sigma
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
P : MorphismProperty Scheme
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst_1 : Finite.{u + 1} 𝒰.I₀
this_1 : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f) =
    Presieve.singleton (Y := (Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)).pt) (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
rw :
  Presheaf.IsSheaf Scheme.zariskiTopology
    (Scheme.forgetToTop.op ⋙ TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (continuousMapPresheafIsoUlift T)]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff, AlgebraicGeometry.continuousMapPresheafIsoUlift
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
h :
  Presheaf.IsSheaf TopCat.grothendieckTopology
    (TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
⊢ Presheaf.IsSheaf Scheme.zariskiTopology
    (Scheme.forgetToTop.op ⋙ TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))

Tactic:
apply Scheme.forgetToTop.op_comp_isSheaf_of_isSheaf _ TopCat.grothendieckTopology

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf, AlgebraicGeometry.Scheme.forgetToTop, TopCat.grothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
h : Presheaf.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
⊢ Presheaf.IsSheaf TopCat.grothendieckTopology
    (TopCat.uliftFunctor.op ⋙ Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))

Tactic:
apply TopCat.uliftFunctor.op_comp_isSheaf_of_isSheaf _ TopCat.grothendieckTopology

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf, TopCat.grothendieckTopology, TopCat.uliftFunctor
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
h : Presieve.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))
⊢ Presheaf.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presieve.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))

Tactic:
GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presieve.IsSheaf TopCat.grothendieckTopology (Functor.obj yoneda (TopCat.of (ULift.{u_1, v} T)))

Tactic:
exact GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
rw :
  Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheaf T)

Tactic:
rw [isSheaf_iff_isSheaf_of_type, Scheme.fpqcTopology_eq_propQCTopology,
    isSheaf_type_propQCTopology_iff]

Premises used: AlgebraicGeometry.isSheaf_type_propQCTopology_iff, CategoryTheory.isSheaf_iff_isSheaf_of_type, AlgebraicGeometry.Scheme.fpqcTopology_eq_propQCTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))

Tactic:
⟨?_, fun {R S} f hf₁ hf₂ ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
refine_1 : Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
refine_2 :
  ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S) (hf₁ : Flat (Spec.map f)) (hf₂ : Surjective (Spec.map f)),
    Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))

Tactic:
refine ⟨?_, fun {R S} f hf₁ hf₂ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
refine_1 : Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
isSheaf_zariskiTopology_continuousMapPresheaf _

Premises used: AlgebraicGeometry.isSheaf_zariskiTopology_continuousMapPresheaf
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
exact isSheaf_zariskiTopology_continuousMapPresheaf _

Premises used: AlgebraicGeometry.isSheaf_zariskiTopology_continuousMapPresheaf
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
refine_2 :
  ∀ (x : (continuousMapPresheaf T).obj (Opposite.op (Spec S))),
    (∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
        p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
          Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
                  (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                    (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
                x :
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
                  (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                    (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
                x :
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))) →
      ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
            y =
          x
⊢ Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))

Tactic:
rw [Presieve.isSheafFor_singleton]

Premises used: CategoryTheory.Presieve.isSheafFor_singleton
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)

Tactic:
have : Topology.IsQuotientMap (Spec.map f) := Flat.isQuotientMap_of_surjective _
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
⊢ ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
          (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
        y =
      x

Tactic:
⟨?_, ?_, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro