awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
⊢ ∃! t : Functor.obj (Functor.obj yoneda X) (op Y), x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) t

Tactic:
⟨e, ?_, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
h : (fun (t : Functor.obj (Functor.obj yoneda X) (op Y)) ↦ x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) t) e
h₁ :
  ∀ (y : Functor.obj (Functor.obj yoneda X) (op Y)),
    (fun (t : Functor.obj (Functor.obj yoneda X) (op Y)) ↦ x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) t) y →
      y = e
⊢ ∃! t : Functor.obj (Functor.obj yoneda X) (op Y), x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) t

Tactic:
refine ⟨e, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y_1 : Scheme
𝓤 : Y_1.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y_1
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y_1 ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
Y : Scheme
j : 𝓤.I₀
h : 𝓤.f j ≫ Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯ = x (𝓤.f j) ⋯
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (Functor.obj yoneda X) (𝓤.f j).op) :
        (a : (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (op Y_1))) →
          (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (op (𝓤.X j))))
      e =
    x (𝓤.f j) ⋯

Tactic:
dsimp [e]
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y_1 : Scheme
𝓤 : Y_1.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y_1
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y_1 ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
Y : Scheme
j : 𝓤.I₀
h h₁ : x (𝓤.f j) ⋯ = x (𝓤.f j) ⋯
⊢ 𝓤.f j ≫ Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯ = x (𝓤.f j) ⋯

Tactic:
rw [𝓤.ι_glueMorphisms]

Premises used: AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
e' : Functor.obj (Functor.obj yoneda X) (op Y)
h : x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) e'
h₁ : ∀ (x : 𝓤.I₀), 𝓤.f x ≫ e' = 𝓤.f x ≫ e
⊢ e' = e

Tactic:
apply 𝓤.hom_ext

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
e' : Functor.obj (Functor.obj yoneda X) (op Y)
h : x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) e'
j : 𝓤.I₀
h₁ : 𝓤.f j ≫ e' = x (𝓤.f j) ⋯
⊢ 𝓤.f j ≫ e' = 𝓤.f j ≫ e

Tactic:
rw [𝓤.ι_glueMorphisms]

Premises used: AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
e' : Functor.obj (Functor.obj yoneda X) (op Y)
h : x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) e'
j : 𝓤.I₀
⊢ 𝓤.f j ≫ e' = x (𝓤.f j) ⋯

Tactic:
h (𝓤.f j) (.mk j)

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (Functor.obj yoneda X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible (R := Presieve.ofArrows 𝓤.X 𝓤.f)
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯
e' : Functor.obj (Functor.obj yoneda X) (op Y)
h : x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) e'
j : 𝓤.I₀
⊢ 𝓤.f j ≫ e' = x (𝓤.f j) ⋯

Tactic:
exact h (𝓤.f j) (.mk j)

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
⊢ (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop

Tactic:
⟨fun _ _ hR ↦ ⟨fun _ _ f _ hf _ ↦ ?_⟩⟩

Premises used: CategoryTheory.Functor.PreservesPairwisePullbacks.mk, CategoryTheory.Precoverage.PullbacksPreservedBy.mk
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
refine :
  ∀ (x : Scheme.{u}) (x_1 : Presieve x) (hR : x_1 ∈ (precoverage IsOpenImmersion).coverings x) (x_2 x_3 : Scheme.{u})
    (f : x_2 ⟶ x) (x_4 : x_3 ⟶ x) (hf : x_1 f), x_1 x_4 → PreservesLimit (cospan f x_4) forgetToTop
⊢ (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop

Tactic:
refine ⟨fun _ _ hR ↦ ⟨fun _ _ f _ hf _ ↦ ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
x : Scheme
x_1 : Presieve x
hR : x_1 ∈ (precoverage IsOpenImmersion).coverings x
x_2 x_3 : Scheme
f : x_2 ⟶ x
x_4 : x_3 ⟶ x
hf : x_1 f
h : x_1 x_4
⊢ IsOpenImmersion f

Tactic:
have : IsOpenImmersion f := hR.2 hf
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
x : Scheme
x_1 : Presieve x
hR : x_1 ∈ (precoverage IsOpenImmersion).coverings x
x_2 x_3 : Scheme
f : x_2 ⟶ x
x_4 : x_3 ⟶ x
hf : x_1 f
h : x_1 x_4
this : IsOpenImmersion f
⊢ PreservesLimit (cospan f x_4) forgetToTop

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
⊢ (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop

Tactic:
have : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop := by
    refine ⟨fun _ _ hR ↦ ⟨fun _ _ f _ hf _ ↦ ?_⟩⟩
    have : IsOpenImmersion f := hR.2 hf
    infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
h : precoverage IsOpenImmersion ≤ Precoverage.comap forgetToTop TopCat.precoverage
⊢ forgetToTop.IsContinuous (precoverage IsOpenImmersion).toGrothendieck TopCat.grothendieckTopology

Tactic:
apply Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy

Premises used: CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
h :
  jointlySurjectivePrecoverage ≤
    Precoverage.comap forgetToTop
      (Precoverage.comap
        (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
        Types.jointlySurjectivePrecoverage)
h₁ : IsOpenImmersion.precoverage ≤ Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage
⊢ jointlySurjectivePrecoverage ⊓ IsOpenImmersion.precoverage ≤
    Precoverage.comap forgetToTop
        (Precoverage.comap
          (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
            TopCat.carrier))
          Types.jointlySurjectivePrecoverage) ⊓
      Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage

Tactic:
gcongr
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
h :
  jointlySurjectivePrecoverage ≤
    Precoverage.comap
      (forgetToTop ⋙
        CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
      Types.jointlySurjectivePrecoverage
h₁ h₂ : jointlySurjectivePrecoverage ≤ jointlySurjectivePrecoverage
⊢ jointlySurjectivePrecoverage ≤
    Precoverage.comap forgetToTop
      (Precoverage.comap
        (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
        Types.jointlySurjectivePrecoverage)

Tactic:
rw [← Precoverage.comap_comp, forgetToTop_comp_forget]

Premises used: AlgebraicGeometry.Scheme.forgetToTop_comp_forget, CategoryTheory.Precoverage.comap_comp
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
h : IsOpenImmersion.precoverage ≤ (TopCat.isOpenEmbedding.inverseImage forgetToTop).precoverage
⊢ IsOpenImmersion.precoverage ≤ Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage

Tactic:
rw [MorphismProperty.comap_precoverage]

Premises used: CategoryTheory.MorphismProperty.comap_precoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ (TopCat.isOpenEmbedding.inverseImage forgetToTop).precoverage

Tactic:
MorphismProperty.precoverage_monotone fun X Y f hf ↦ f.isOpenEmbedding

Premises used: CategoryTheory.MorphismProperty.precoverage_monotone, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ (TopCat.isOpenEmbedding.inverseImage forgetToTop).precoverage

Tactic:
exact MorphismProperty.precoverage_monotone fun X Y f hf ↦ f.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X : Scheme
i j :
  (X.affineCover.refineOneHypercover fun (i j : X.affineCover.I₀) ↦
      Precoverage.ZeroHypercover.toPreZeroHypercover (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover).I₀
⊢ Membership.mem (γ :=
    Set
      (Sieve
        (pullback
          ((X.affineCover.refineOneHypercover fun (i j : X.affineCover.I₀) ↦
                Precoverage.ZeroHypercover.toPreZeroHypercover
                  (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover).f
            i)
          ((X.affineCover.refineOneHypercover fun (i j : X.affineCover.I₀) ↦
                Precoverage.ZeroHypercover.toPreZeroHypercover
                  (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover).f
            j))))
    ((zariskiTopology : (a : Scheme) → Set (Sieve a))
      (pullback
        ((X.affineCover.refineOneHypercover fun (i j : X.affineCover.I₀) ↦
              Precoverage.ZeroHypercover.toPreZeroHypercover
                (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover).f
          i)
        ((X.affineCover.refineOneHypercover fun (i j : X.affineCover.I₀) ↦
              Precoverage.ZeroHypercover.toPreZeroHypercover
                (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover).f
          j)))
    ((X.affineCover.refineOneHypercover fun (i j : X.affineCover.I₀) ↦
          Precoverage.ZeroHypercover.toPreZeroHypercover
            (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover).sieve₁'
      i j)

Tactic:
simpa using Cover.mem_grothendieckTopology _

Premises used: 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_1 : Small.{u, u_1} ι
inst_2 : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
inst : ∀ (f : ι → Schemeᵒᵖ), PreservesLimit (Discrete.functor f) F
⊢ PreservesLimitsOfShape.{u_1, u_1, u, v, u + 1, v + 1} (Discrete ι) F

Tactic:
apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_of_discrete

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_discrete
-- 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ᵒᵖ
⊢ ∀ (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)

Tactic:
have (i : ι) : Mono (Cofan.inj (Sigma.cocone (Discrete.functor <| unop ∘ X)) i) :=
    inferInstanceAs <| Mono (Sigma.ι _ _)
-- 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)
⊢ PreservesLimit (Discrete.functor X) F

Tactic:
Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial
      (Sigma.cocone (Discrete.functor <| unop ∘ X)) (coproductIsCoproduct' _) ?_ ?_

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.initialIsInitial, Function.comp, CategoryTheory.Presieve.preservesProduct_of_isSheafFor, CategoryTheory.Limits.coproductIsCoproduct', CategoryTheory.Limits.Sigma.cocone, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
F : CategoryTheory.Functor.{u, v, u + 1, v + 1} Schemeᵒᵖ (Type v)
ι : Type u_1
inst_1 : Small.{u, u_1} ι
inst_2 : 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)
inst :
  Presieve.IsSheafFor (X := ⊥_ Scheme) F
    (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a)
inst₁ :
  _root_.Pairwise fun (i j : ι) ↦
    IsPullback (P := ⊥_ Scheme) (Z :=
      Cocone.pt (F := Discrete.functor fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))))
      (initial.to (unop (X i))) (initial.to (unop (X j)))
      (Cofan.inj (f := fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
      (Cofan.inj (f := fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))) j)
inst₂ :
  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)))))
⊢ PreservesLimit (Discrete.functor X) F

Tactic:
refine Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial
      (Sigma.cocone (Discrete.functor <| unop ∘ X)) (coproductIsCoproduct' _) ?_ ?_

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.initialIsInitial, Function.comp, CategoryTheory.Presieve.preservesProduct_of_isSheafFor, CategoryTheory.Limits.coproductIsCoproduct', CategoryTheory.Limits.Sigma.cocone, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
F : CategoryTheory.Functor.{u, v, u + 1, v + 1} Schemeᵒᵖ (Type v)
ι : Type u_1
inst_1 : Small.{u, u_1} ι
inst_2 : 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)
inst :
  Membership.mem (γ := Set (Sieve (⊥_ Scheme))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (⊥_ Scheme))
    (Sieve.generate
      (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
        Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a))
⊢ Presieve.IsSheafFor (X := ⊥_ Scheme) F
    (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a)

Tactic:
apply hF.isSheafFor

Premises used: CategoryTheory.Presieve.IsSheaf.isSheafFor
-- 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)
⊢ Membership.mem (γ := Set (Sieve (⊥_ Scheme)))
    ((Scheme.grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (⊥_ Scheme)) ⊥

Tactic:
(⊥_ Scheme).bot_mem_grothendieckTopology

Premises used: AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, AlgebraicGeometry.Scheme, CategoryTheory.Limits.initial
-- 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)
h :
  Eq.{u + 2} (α := Sieve (⊥_ Scheme))
    (Sieve.generate
      (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
        Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a))
    ⊥
⊢ Membership.mem (γ := Set (Sieve (⊥_ Scheme))) ((Scheme.zariskiTopology : (a : Scheme) → Set (Sieve a)) (⊥_ Scheme))
    (Sieve.generate
      (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
        Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a))

Tactic:
convert! (⊥_ Scheme).bot_mem_grothendieckTopology

Premises used: AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, AlgebraicGeometry.Scheme, CategoryTheory.Limits.initial
-- 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)
h :
  LE.le.{u + 1} (α := Sieve (⊥_ Scheme))
    (Sieve.generate
      (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
        Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a))
    ⊥
⊢ Eq.{u + 2} (α := Sieve (⊥_ Scheme))
    (Sieve.generate
      (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
        Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a))
    ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- 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)
Y_1 : Scheme
f : Y_1 ⟶ ⊥_ Scheme
Y : Scheme
i : Empty
w : Y_1 ⟶ i.elim
right : w ≫ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) i = f
⊢ Sieve.arrows ⊥ f

Tactic:
i.elim

Premises used: Empty.elim
-- 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)
Y_1 : Scheme
f : Y_1 ⟶ ⊥_ Scheme
Y : Scheme
i : Empty
w : Y_1 ⟶ i.elim
right : w ≫ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) i = f
⊢ Sieve.arrows ⊥ f

Tactic:
exact i.elim

Premises used: Empty.elim
-- 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)
i j : ι
⊢ i ≠ j →
    (fun (i j : ι) ↦
        IsPullback (P := ⊥_ Scheme) (Z :=
          Cocone.pt (F := Discrete.functor fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))))
          (initial.to (unop (X i))) (initial.to (unop (X j)))
          (Cofan.inj (f := fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
          (Cofan.inj (f := fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))) j))
      i j

Tactic:
CoproductDisjoint.isPullback_of_isInitial
      (coproductIsCoproduct' <| Discrete.functor <| unop ∘ X) initialIsInitial

Premises used: CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial, CategoryTheory.Discrete.functor, CategoryTheory.Limits.initialIsInitial, Function.comp, CategoryTheory.Limits.coproductIsCoproduct', CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.colimit.desc, Opposite.unop
-- 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)
i j : ι
⊢ i ≠ j →
    (fun (i j : ι) ↦
        IsPullback (P := ⊥_ Scheme) (Z :=
          Cocone.pt (F := Discrete.functor fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))))
          (initial.to (unop (X i))) (initial.to (unop (X j)))
          (Cofan.inj (f := fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
          (Cofan.inj (f := fun (x : ι) ↦ unop (X x)) (Sigma.cocone (Discrete.functor (unop ∘ X))) j))
      i j

Tactic:
exact CoproductDisjoint.isPullback_of_isInitial
      (coproductIsCoproduct' <| Discrete.functor <| unop ∘ X) initialIsInitial

Premises used: CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial, CategoryTheory.Discrete.functor, CategoryTheory.Limits.initialIsInitial, Function.comp, CategoryTheory.Limits.coproductIsCoproduct', Opposite.unop