awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left :=
  Cover.changeProp (Q := P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineCover ⋯
x : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ U.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
x_1 : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
X : P.Over ⊤ S
f : X ⟶ U
h : 𝒰.toPresieveOverProp (P := P) (Q := P) ⋯ f
i : 𝒰.I₀
⊢ 𝒰.f i ≫ U.toComma (P := P) (Q := ⊤) (W := ⊤).hom =
    ((MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
            (affineOverMk (P := P) (𝒰.f i ≫ U.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯)).toComma
        (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left :=
  Cover.changeProp (Q := P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineCover ⋯
x : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ U.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
x_1 : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
X : P.Over ⊤ S
f : X ⟶ U
h : 𝒰.toPresieveOverProp (P := P) (Q := P) ⋯ f
i : 𝒰.I₀
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α := (𝒰.X i).asOverProp (P := P) S ⋯ ⟶ U)
    (MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤)
        (𝟙 (Comma.toComma (P := P) (Q := ⊤) (W := ⊤) ((𝒰.X i).asOverProp (P := P) S ⋯)).left) True.intro ⋯ ≫
      MorphismProperty.Over.homMk (P := P) (Q := ⊤) (𝒰.f i) ⋯ trivial)
    (Hom.asOverProp (P := P) (𝒰.f i) S)
⊢ Eq (α := (𝒰.X i).asOverProp (P := P) S ⋯ ⟶ U)
    (MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤)
        (𝟙 (Comma.toComma (P := P) (Q := ⊤) (W := ⊤) ((𝒰.X i).asOverProp (P := P) S ⋯)).left) True.intro ⋯ ≫
      MorphismProperty.Over.homMk (P := P) (Q := ⊤) (𝒰.f i) ⋯ trivial)
    (Hom.asOverProp (P := P) (𝒰.f i) S)

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left :=
  Cover.changeProp (Q := P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineCover ⋯
x : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ U.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
x_1 : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
X : P.Over ⊤ S
f : X ⟶ U
h : 𝒰.toPresieveOverProp (P := P) (Q := P) ⋯ f
i : 𝒰.I₀
⊢ { arrows := Presieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U,
        downward_closed := ⋯ : Sieve U }.arrows
    (Y := (𝒰.X i).asOverProp (P := P) S ⋯) (Hom.asOverProp (P := P) (𝒰.f i) S)

Tactic:
exact ⟨⟨affineOverMk (𝒰.f i ≫ U.hom) (P.comp_mem _ _ (𝒰.map_prop i) U.prop),
      CostructuredArrow.homMk (𝟙 _) ⟨⟩ rfl, Over.homMk (𝒰.f i) (by simp) trivial,
      by cat_disch⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.toComma (P := P) (Q := ⊤) (W := ⊤).left.AffineOpenCover :=
  X.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineOpenCover
𝒱 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left := Cover.changeProp (Q := P) 𝒰.openCover ⋯
x : (i : 𝒱.I₀) → (𝒱.X i).Over S :=
  fun (i : 𝒱.I₀) ↦ { hom := 𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
this : Cover.Over S (P := P) 𝒱 := Cover.Over.mk (P := P) inferInstance ⋯
i : 𝒰.I₀ (P := IsOpenImmersion)
⊢ ⊤ (𝒰.f (P := IsOpenImmersion) i)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.toComma (P := P) (Q := ⊤) (W := ⊤).left.AffineOpenCover :=
  X.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineOpenCover
𝒱 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left := Cover.changeProp (Q := P) 𝒰.openCover ⋯
x : (i : 𝒱.I₀) → (𝒱.X i).Over S :=
  fun (i : 𝒱.I₀) ↦ { hom := 𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
this : Cover.Over S (P := P) 𝒱 := Cover.Over.mk (P := P) inferInstance ⋯
refine :
  (Sieve.ofArrows
      (fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
        (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
          ((fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
              affineOverMk (P := P) (𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯)
            i))
      fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
      MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) ⋯ ⋯) ∈
    (smallGrothendieckTopology P : (a : P.Over ⊤ S) → Set (Sieve a)) X
⊢ ∃ (ι : Type u) (U : ι → P.CostructuredArrow ⊤ Scheme.Spec S) (f :
    (i : ι) → (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj (U i) ⟶ X),
    Sieve.ofArrows (fun (i : ι) ↦ (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj (U i)) f ∈
      (smallGrothendieckTopology P : (a : P.Over ⊤ S) → Set (Sieve a)) X

Tactic:
refine ⟨𝒰.I₀, fun i ↦ affineOverMk (𝒰.f i ≫ X.hom)
      (P.comp_mem _ _ (IsZariskiLocalAtSource.of_isOpenImmersion (𝒰.f i)) X.prop),
      fun i ↦ CostructuredArrow.homMk (𝒰.f i) (by simp), ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.toComma (P := P) (Q := ⊤) (W := ⊤).left.AffineOpenCover :=
  X.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineOpenCover
𝒱 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left := Cover.changeProp (Q := P) 𝒰.openCover ⋯
x : (i : 𝒱.I₀) → (𝒱.X i).Over S :=
  fun (i : 𝒱.I₀) ↦ { hom := 𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
this : Cover.Over S (P := P) 𝒱 := Cover.Over.mk (P := P) inferInstance ⋯
rw :
  ∃ (𝒰_1 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰_1) (h :
    ∀ (j : 𝒰_1.I₀), P (𝒰_1.X j ↘ S)),
    𝒰_1.toPresieveOverProp (P := P) (Q := P) h ≤
      Sieve.arrows
        (Sieve.ofArrows
          (fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
            (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
              ((fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
                  affineOverMk (P := P) (𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯)
                i))
          fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
          MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) ⋯ ⋯)
⊢ (Sieve.ofArrows
      (fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
        (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
          ((fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
              affineOverMk (P := P) (𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯)
            i))
      fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
      MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) ⋯ ⋯) ∈
    (smallGrothendieckTopology P : (a : P.Over ⊤ S) → Set (Sieve a)) X

Tactic:
rw [Scheme.mem_smallGrothendieckTopology]

Premises used: AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.toComma (P := P) (Q := ⊤) (W := ⊤).left.AffineOpenCover :=
  X.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineOpenCover
𝒱 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left := Cover.changeProp (Q := P) 𝒰.openCover ⋯
x : (i : 𝒱.I₀) → (𝒱.X i).Over S :=
  fun (i : 𝒱.I₀) ↦ { hom := 𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
this : Cover.Over S (P := P) 𝒱 := Cover.Over.mk (P := P) inferInstance ⋯
x_1 : P.Over ⊤ S
x_2 : x_1 ⟶ X
h : 𝒱.toPresieveOverProp (P := P) (Q := P) ⋯ x_2
i : 𝒱.I₀
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α := (𝒱.X i).asOverProp (P := P) S ⋯ ⟶ X) (Hom.asOverProp (P := P) (𝒱.f i) S)
    (𝟙 ((𝒱.X i).asOverProp (P := P) S ⋯) ≫
      MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) ⋯ ⋯)
⊢ Eq (α := (𝒱.X i).asOverProp (P := P) S ⋯ ⟶ X) (Hom.asOverProp (P := P) (𝒱.f i) S)
    (𝟙 ((𝒱.X i).asOverProp (P := P) S ⋯) ≫
      MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) ⋯ ⋯)

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.toComma (P := P) (Q := ⊤) (W := ⊤).left.AffineOpenCover :=
  X.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineOpenCover
𝒱 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left := Cover.changeProp (Q := P) 𝒰.openCover ⋯
x : (i : 𝒱.I₀) → (𝒱.X i).Over S :=
  fun (i : 𝒱.I₀) ↦ { hom := 𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
this : Cover.Over S (P := P) 𝒱 := Cover.Over.mk (P := P) inferInstance ⋯
⊢ ∃ (𝒰_1 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰_1) (h :
    ∀ (j : 𝒰_1.I₀), P (𝒰_1.X j ↘ S)),
    𝒰_1.toPresieveOverProp (P := P) (Q := P) h ≤
      Sieve.arrows
        (Sieve.ofArrows
          (fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
            (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
              ((fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
                  affineOverMk (P := P) (𝒰.f (P := IsOpenImmersion) i ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯)
                i))
          fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
          MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) ⋯ ⋯)

Tactic:
exact ⟨𝒱, inferInstance, fun i ↦ P.comp_mem _ _ (𝒱.map_prop i) X.prop,
      fun _ _ ⟨i⟩ ↦ (Sieve.mem_ofArrows_iff ..).mpr ⟨i, 𝟙 _, by cat_disch⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
⊢ (AffineEtale.Spec S).Faithful

Tactic:
inferInstanceAs <| (MorphismProperty.CostructuredArrow.toOver _ _ _).Faithful

Premises used: _private.0.AlgebraicGeometry.Scheme.AffineEtale.instFaithfulEtaleSpec._proof_1
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
⊢ (AffineEtale.Spec S).Full

Tactic:
inferInstanceAs <| (MorphismProperty.CostructuredArrow.toOver _ _ _).Full

Premises used: _private.0.AlgebraicGeometry.Scheme.AffineEtale.instFullEtaleSpec._proof_1
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
⊢ (AffineEtale.Spec S).IsCoverDense S.smallEtaleTopology

Tactic:
inferInstanceAs <| (MorphismProperty.CostructuredArrow.toOver _ _ _).IsCoverDense
    (smallGrothendieckTopology _)

Premises used: _private.0.AlgebraicGeometry.Scheme.AffineEtale.instIsCoverDenseEtaleSpecSmallEtaleTopology._proof_1
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
⊢ Functor.IsDenseSubsite ((AffineEtale.Spec S).inducedTopology S.smallEtaleTopology) S.smallEtaleTopology
    (AffineEtale.Spec S)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
⊢ (AffineEtale.Spec S).IsOneHypercoverDense (topology S) S.smallEtaleTopology

Tactic:
isOneHypercoverDense_toOver_Spec _

Premises used: CategoryTheory.Functor.inducedTopology, AlgebraicGeometry.Scheme.AffineEtale.topology, AlgebraicGeometry.Scheme.Etale, AlgebraicGeometry.Scheme.isOneHypercoverDense_toOver_Spec, AlgebraicGeometry.Scheme.AffineEtale, AlgebraicGeometry.Scheme.smallEtaleTopology, AlgebraicGeometry.Scheme.AffineEtale.Spec
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
⊢ EssentiallySmall.{u, u, u + 1} S.AffineEtale

Tactic:
essentiallySmall_costructuredArrow_Spec _ fun _ _ _ _ ↦ inferInstance

Premises used: inferInstance, AlgebraicGeometry.Scheme.AffineEtale, AlgebraicGeometry.essentiallySmall_costructuredArrow_Spec
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
⊢ HasSheafify (AffineEtale.topology S) A

Tactic:
hasSheafifyEssentiallySmallSite.{u} _ _

Premises used: CategoryTheory.hasSheafifyEssentiallySmallSite
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
⊢ Functor.IsEquivalence (C := Sheaf S.smallEtaleTopology A) (D := Sheaf (AffineEtale.topology S) A)
    ((AffineEtale.Spec S).sheafPushforwardContinuous A (AffineEtale.topology S) S.smallEtaleTopology)

Tactic:
Functor.isEquivalence_of_isOneHypercoverDense _ _ _ _

Premises used: CategoryTheory.Functor.isEquivalence_of_isOneHypercoverDense
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
⊢ HasSheafify S.smallEtaleTopology A

Tactic:
Functor.IsDenseSubsite.hasSheafify_of_isEquivalence
    (AffineEtale.topology S) S.smallEtaleTopology (AffineEtale.Spec S)

Premises used: AlgebraicGeometry.Scheme.AffineEtale.topology, CategoryTheory.Functor.IsDenseSubsite.hasSheafify_of_isEquivalence, AlgebraicGeometry.Scheme.smallEtaleTopology, AlgebraicGeometry.Scheme.AffineEtale.Spec
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
⊢ (AffineEtale.topology S).WEqualsLocallyBijective A (FA := FA) (CA := CD)

Tactic:
.ofEssentiallySmall (AffineEtale.topology S)

Premises used: AlgebraicGeometry.Scheme.AffineEtale.topology, CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
⊢ S.smallEtaleTopology.WEqualsLocallyBijective A (FA := FA) (CA := CD)

Tactic:
.transport  _ _ _
    (Functor.IsDenseSubsite.coverPreserving (AffineEtale.topology S) _
      (AffineEtale.Spec S))

Premises used: AlgebraicGeometry.Scheme.AffineEtale.topology, CategoryTheory.Functor.IsDenseSubsite.coverPreserving, CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport, AlgebraicGeometry.Scheme.AffineEtale.Spec
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_8 : Abelian.{u, u'} A
inst_9 : IsGrothendieckAbelian.{u, u, u'} A
⊢ IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u} (Sheaf (AffineEtale.topology S) A)

Tactic:
Sheaf.isGrothendieckAbelian_of_essentiallySmall _ _

Premises used: CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_8 : Abelian.{u, u'} A
inst_9 : IsGrothendieckAbelian.{u, u, u'} A
⊢ IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u} (Sheaf S.smallEtaleTopology A)

Tactic:
IsGrothendieckAbelian.of_equivalence (AffineEtale.sheafEquiv S A)

Premises used: CategoryTheory.IsGrothendieckAbelian.of_equivalence, AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv
-- Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale
Goal:
S : Scheme
A : Type u'
inst : Category.{u, u'} A
FA : A → A → Type u_1
CD : A → Type u
inst_1 : (X Y : A) → FunLike.{u_1 + 1, u + 1, u + 1} (FA X Y) (CD X) (CD Y)
inst_2 : ConcreteCategory A FA (CC := CD)
inst_3 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_4 : HasColimits.{u, u'} A
inst_5 : HasLimits.{u, u'} A
inst_6 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CD))
inst_7 : PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A (FC := FA) (CC := CD))
R : Type u
inst_8 : Ring R
⊢ IsGrothendieckAbelian.{u, u + 1, u + 1} (Sheaf S.smallEtaleTopology (ModuleCat R))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
⊢ zariskiTopology = zariskiPretopology.toGrothendieck

Tactic:
Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck.symm

Premises used: AlgebraicGeometry.Scheme.pretopology, CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck, Eq.symm, AlgebraicGeometry.Scheme.zariskiPretopology
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
h : ∀ (X : Scheme.{u_1}), Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)
⊢ zariskiTopology.Subcanonical

Tactic:
apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X : Scheme
h :
  ∀ ⦃X_1 : Scheme.{u_1}⦄,
    ∀ R ∈ (precoverage IsOpenImmersion).coverings X_1, Presieve.IsSheafFor (Functor.obj yoneda X) R
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)

Tactic:
rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]

Premises used: CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Sites.BigZariski
Goal:
X Y : Scheme
S : Presieve Y
hS : S ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (Functor.obj yoneda X) S
hx : x.Compatible (R := S)
h :
  ∀ (𝓤 : 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)),
    ∃! t : Functor.obj (Functor.obj yoneda X) (op Y), x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) t
⊢ ∃! t : Functor.obj (Functor.obj yoneda X) (op Y), x.IsAmalgamation (R := S) t

Tactic:
obtain ⟨(𝓤 : OpenCover Y), rfl⟩ := exists_cover_of_mem_pretopology hS

Premises used: AlgebraicGeometry.Scheme.OpenCover, AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology, rfl
-- 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)
i j : 𝓤.I₀
a :
  Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan (𝓤.f i) (𝓤.f j))).pt)
        WalkingCospan.left ⟶
      Y)
    ((limit.cone (cospan (𝓤.f i) (𝓤.f j))).π.1 WalkingCospan.left ≫ 𝓤.f i)
    ((limit.cone (cospan (𝓤.f i) (𝓤.f j))).π.1 WalkingCospan.right ≫ 𝓤.f j)
⊢ Eq (α := pullback (𝓤.f i) (𝓤.f j) ⟶ X) (pullback.fst (𝓤.f i) (𝓤.f j) ≫ (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) i)
    (pullback.snd (𝓤.f i) (𝓤.f j) ≫ (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) j)

Tactic:
apply hx
-- 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)
i j : 𝓤.I₀
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan (𝓤.f i) (𝓤.f j))).pt)
        WalkingCospan.left ⟶
      Y)
    ((limit.cone (cospan (𝓤.f i) (𝓤.f j))).π.1 WalkingCospan.left ≫ 𝓤.f i)
    ((limit.cone (cospan (𝓤.f i) (𝓤.f j))).π.1 WalkingCospan.right ≫ 𝓤.f j)

Tactic:
Limits.pullback.condition

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.pullback.condition
-- 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)
i j : 𝓤.I₀
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan (𝓤.f i) (𝓤.f j))).pt)
        WalkingCospan.left ⟶
      Y)
    ((limit.cone (cospan (𝓤.f i) (𝓤.f j))).π.1 WalkingCospan.left ≫ 𝓤.f i)
    ((limit.cone (cospan (𝓤.f i) (𝓤.f j))).π.1 WalkingCospan.right ≫ 𝓤.f j)

Tactic:
exact Limits.pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition