awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Affine (goal)
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
⊢ Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U ∈
    (smallGrothendieckTopology P : (a : P.Over ⊤ S) → Set (Sieve a)) U
have rw : ∃ (𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
  ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
  𝒰.toPresieveOverProp (P := P) (Q := P) h ≤
    (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows
Tactic: rw [Scheme.mem_smallGrothendieckTopology]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Affine (goal)
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 ⋯
⊢ ∃ (𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
    ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
    𝒰.toPresieveOverProp (P := P) (Q := P) h ≤
      (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows
have refine : ∀ (X : P.Over ⊤ S) (f : X ⟶ U),
  𝒰.toPresieveOverProp (P := P) (Q := P) sorry f →
    ∀ (i : 𝒰.I₀),
      (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows (Y :=
        (𝒰.X i).asOverProp (P := P) S sorry) (Hom.asOverProp (P := P) (𝒰.f i) S)
Tactic: refine ⟨𝒰, inferInstance,
      fun i ↦ P.comp_mem _ _ (𝒰.map_prop i) U.prop, fun X f ⟨i⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Affine (goal)
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 ⋯
⊢ ∃ (ι : 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
have 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) sorry)
          i))
    fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
    MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) sorry sorry) ∈
  (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), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Affine (goal)
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 ⋯
⊢ (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
have 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) sorry)
              i))
        fun (i : 𝒰.I₀ (P := IsOpenImmersion)) ↦
        MorphismProperty.CostructuredArrow.homMk (P := P) (Q := ⊤) (𝒰.f (P := IsOpenImmersion) i) sorry sorry)
Tactic: rw [Scheme.mem_smallGrothendieckTopology]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
⊢ zariskiTopology.Subcanonical
have h : ∀ (X : Scheme.{u_1}), Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)
Tactic: apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
X : Scheme
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)
have h : ∀ ⦃X_1 : Scheme.{u_1}⦄, ∀ R ∈ (precoverage IsOpenImmersion).coverings X_1, Presieve.IsSheafFor (Functor.obj yoneda X) R
Tactic: rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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)
⊢ ∃! t : Functor.obj (Functor.obj yoneda X) (op Y), x.IsAmalgamation (R := S) t
have 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
Tactic: obtain ⟨(𝓤 : OpenCover Y), rfl⟩ := exists_cover_of_mem_pretopology hS
Cleared hypotheses: S, hS, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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 (α := 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)
have 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)
Tactic: apply hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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
have h : (fun (t : Functor.obj (Functor.obj yoneda X) (op Y)) ↦ x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) t) e
Tactic: refine ⟨e, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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
⊢ ∃! t : Functor.obj (Functor.obj yoneda X) (op Y), x.IsAmalgamation (R := Presieve.ofArrows 𝓤.X 𝓤.f) t
have 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
Tactic: refine ⟨e, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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₀
⊢ (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) ⋯
have h : 𝓤.f j ≫ Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) sorry) sorry = x (𝓤.f j) sorry
Tactic: dsimp [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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₀
⊢ 𝓤.f j ≫ Cover.glueMorphisms 𝓤 (fun (j : 𝓤.I₀) ↦ x (𝓤.f j) ⋯) ⋯ = x (𝓤.f j) ⋯
have h : x (𝓤.f j) sorry = x (𝓤.f j) sorry
Tactic: rw [𝓤.ι_glueMorphisms]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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'
⊢ e' = e
have h₁ : ∀ (x : 𝓤.I₀), 𝓤.f x ≫ e' = 𝓤.f x ≫ e
Tactic: apply 𝓤.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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' = 𝓤.f j ≫ e
have h₁ : 𝓤.f j ≫ e' = x (𝓤.f j) sorry
Tactic: rw [𝓤.ι_glueMorphisms]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
⊢ (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
have 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
Tactic: refine ⟨fun _ _ hR ↦ ⟨fun _ _ f _ hf _ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (hypothesis)
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
⊢ PreservesLimit (cospan f x_4) forgetToTop
have this : IsOpenImmersion f
Tactic: have : IsOpenImmersion f := hR.2 hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (hypothesis)
Goal:
⊢ forgetToTop.IsContinuous (precoverage IsOpenImmersion).toGrothendieck TopCat.grothendieckTopology
have this : (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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ forgetToTop.IsContinuous (precoverage IsOpenImmersion).toGrothendieck TopCat.grothendieckTopology
have h : precoverage IsOpenImmersion ≤ Precoverage.comap forgetToTop TopCat.precoverage
Tactic: apply Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ 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
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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)
⊢ 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
have h₁ : IsOpenImmersion.precoverage ≤ Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage
Tactic: gcongr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ 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)
have 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
Tactic: rw [← Precoverage.comap_comp, forgetToTop_comp_forget]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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
⊢ 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)
have h₁ : jointlySurjectivePrecoverage ≤ jointlySurjectivePrecoverage
Tactic: rw [← Precoverage.comap_comp, forgetToTop_comp_forget]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
Goal:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage
have h : IsOpenImmersion.precoverage ≤ (TopCat.isOpenEmbedding.inverseImage forgetToTop).precoverage
Tactic: rw [MorphismProperty.comap_precoverage]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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
⊢ PreservesLimitsOfShape.{u_1, u_1, u, v, u + 1, v + 1} (Discrete ι) F
have inst : ∀ (f : ι → Schemeᵒᵖ), PreservesLimit (Discrete.functor f) F
Tactic: apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_of_discrete
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (hypothesis)
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ᵒᵖ
⊢ PreservesLimit (Discrete.functor X) F
have 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)
Tactic: have (i : ι) : Mono (Cofan.inj (Sigma.cocone (Discrete.functor <| unop ∘ X)) i) :=
    inferInstanceAs <| Mono (Sigma.ι _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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
have inst : Presieve.IsSheafFor (X := ⊥_ Scheme) F
  (Presieve.ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a)
Tactic: refine Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial
      (Sigma.cocone (Discrete.functor <| unop ∘ X)) (coproductIsCoproduct' _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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)
⊢ PreservesLimit (Discrete.functor X) F
have 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)
Tactic: refine Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial
      (Sigma.cocone (Discrete.functor <| unop ∘ X)) (coproductIsCoproduct' _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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)
⊢ PreservesLimit (Discrete.functor X) F
have 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)))))
Tactic: refine Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial
      (Sigma.cocone (Discrete.functor <| unop ∘ X)) (coproductIsCoproduct' _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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 := ⊥_ Scheme) F
    (Presieve.ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ ⊥_ Scheme) a)
have 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))
Tactic: apply hF.isSheafFor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.BigZariski (goal)
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.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))
have 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))
  ⊥
Tactic: convert! (⊥_ Scheme).bot_mem_grothendieckTopology