awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
V : Scheme
γ : V ⟶ U
Y_1 : Scheme
i :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
a : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i
fac₁ : a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i = γ ≫ α
Y : Scheme
j :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
b : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
fac₂ : b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = γ ≫ β
⊢ Sieve.arrows
    (Presheaf.equalizerSieve (FD := TypeCat.Fun) (F :=
      (zariskiTopology.yoneda.obj (glueData hf).glued).obj (P := Presheaf.IsSheaf zariskiTopology)) α β)
    γ
have change : γ ≫ α = γ ≫ β
Tactic: change γ ≫ α = γ ≫ β
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
V : Scheme
γ : V ⟶ U
Y_1 : Scheme
i :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
a : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i
fac₁ : a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i = γ ≫ α
Y : Scheme
j :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
b : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
fac₂ : b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = γ ≫ β
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
        (b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
⊢ a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i =
    b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
have h₁ : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
Tactic: apply comp_toGlued_eq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
⊢ IsIso (yonedaGluedToSheaf hf)
have rw : Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf) ∧
  Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)
Tactic: rw [← Sheaf.isLocallyBijective_iff_isIso (yonedaGluedToSheaf hf)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
⊢ Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf) ∧
    Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)
have left : Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst :
  Presheaf.IsLocallySurjective zariskiTopology (FA := TypeCat.Fun) (F := ∐ fun (b : ι) ↦ Functor.obj yoneda (X b))
    (Sigma.desc f)
left : Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf)
⊢ Sheaf.IsLocallyInjective (FD := TypeCat.Fun) (yonedaGluedToSheaf hf) ∧
    Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)
have right : Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (yonedaGluedToSheaf hf)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
⊢ Presieve.IsSheaf (propQCTopology P) F ↔
    Presieve.IsSheaf zariskiTopology F ∧
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
have refine_1 : ∀ (hF : Presieve.IsSheaf (propQCTopology P) F), Presieve.IsSheaf zariskiTopology F
Tactic: refine ⟨fun hF ↦ ⟨?_, fun {R S} f hf hs ↦ ?_⟩, fun ⟨hzar, hff⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
refine_1 : ∀ (hF : Presieve.IsSheaf (propQCTopology P) F), Presieve.IsSheaf zariskiTopology F
⊢ Presieve.IsSheaf (propQCTopology P) F ↔
    Presieve.IsSheaf zariskiTopology F ∧
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
have refine_2 : ∀ (hF : Presieve.IsSheaf (propQCTopology P) F) {R S : CommRingCat.{u}} (f : R ⟶ S) (hf : P (Spec.map f))
  (hs : Surjective (Spec.map f)), Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
Tactic: refine ⟨fun hF ↦ ⟨?_, fun {R S} f hf hs ↦ ?_⟩, fun ⟨hzar, hff⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
refine_1 : ∀ (hF : Presieve.IsSheaf (propQCTopology P) F), Presieve.IsSheaf zariskiTopology F
refine_2 :
  ∀ (hF : Presieve.IsSheaf (propQCTopology P) F) {R S : CommRingCat.{u}} (f : R ⟶ S) (hf : P (Spec.map f))
    (hs : Surjective (Spec.map f)), Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
⊢ Presieve.IsSheaf (propQCTopology P) F ↔
    Presieve.IsSheaf zariskiTopology F ∧
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
have refine_3 : (Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))) →
  ∀ (hzar : Presieve.IsSheaf zariskiTopology F)
    (hff :
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))),
    Presieve.IsSheaf (propQCTopology P) F
Tactic: refine ⟨fun hF ↦ ⟨?_, fun {R S} f hf hs ↦ ?_⟩, fun ⟨hzar, hff⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
⊢ Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
have refine_2 : Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
  (Sieve.generate (Presieve.singleton (Spec.map f)))
Tactic: apply hF.isSheafFor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
⊢ Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
    (Sieve.generate (Presieve.singleton (Spec.map f)))
have refine_2 : Membership.mem (γ := Set (Sieve (Spec R))) ((propQCTopology P : (a : Scheme) → Set (Sieve a)) (Spec R))
  (Sieve.generate (Hom.cover (P := P) (Spec.map f) hf).presieve₀)
Tactic: rw [← Hom.presieve₀_cover _ hf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
⊢ Presieve.IsSheaf (propQCTopology P) F
have refine_3 : ∀ ⦃X : Scheme.{u}⦄ (E : (propQCPrecoverage P).ZeroHypercover X), Presieve.IsSheafFor F E.presieve₀
Tactic: rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small.{u}]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
⊢ ∀ (E : (propQCPrecoverage P).ZeroHypercover T), Presieve.IsSheafFor F E.presieve₀
have refine_3 : ∀ (𝒰 : Cover (propQCPrecoverage P) T), Presieve.IsSheafFor F 𝒰.presieve₀
Tactic: (𝒰 : Scheme.Cover _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have refine_3 : ∀
  (this :
    ∀ ⦃T : Scheme.{u}⦄ (𝒰 : Cover (propQCPrecoverage P) T) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
      Presieve.IsSheafFor F 𝒰.presieve₀)
  (hT : ¬∃ (R : CommRingCat.{u}), T = Spec R), Presieve.IsSheafFor F 𝒰.presieve₀
Tactic: wlog hT : ∃ (R : CommRingCat.{u}), T = Spec R generalizing T
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
refine_3 :
  ∀
    (this :
      ∀ ⦃T : Scheme.{u}⦄ (𝒰 : Cover (propQCPrecoverage P) T) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
        Presieve.IsSheafFor F 𝒰.presieve₀)
    (hT : ¬∃ (R : CommRingCat.{u}), T = Spec R), Presieve.IsSheafFor F 𝒰.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have wlog : ∀ ⦃T : Scheme.{u}⦄ (𝒰 : Cover (propQCPrecoverage P) T) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
  Presieve.IsSheafFor F 𝒰.presieve₀
Tactic: wlog hT : ∃ (R : CommRingCat.{u}), T = Spec R generalizing T
Cleared hypotheses: T, 𝒰
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this :
  ∀ ⦃T : Scheme.{u}⦄ (𝒰 : Cover (propQCPrecoverage P) T) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
i : T.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F (Sieve.pullback (T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows
have refine_3 : Presieve.IsSheafFor (X := T.affineOneHypercover.X i) F
  (Presieve.ofArrows (fun (i_1 : 𝒰.I₀) ↦ pullback (𝒰.f i_1) (T.affineOneHypercover.f i)) fun (x : 𝒰.I₀) ↦
    pullback.snd (𝒰.f x) (T.affineOneHypercover.f i))
Tactic: rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
          ← Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this :
  ∀ ⦃T : Scheme.{u}⦄ (𝒰 : Cover (propQCPrecoverage P) T) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows
have refine_3 : Presieve.IsSeparatedFor F (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)
Tactic: rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this :
  ∀ ⦃T : Scheme.{u}⦄ (𝒰 : Cover (propQCPrecoverage P) T) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)
have refine_3 : Presieve.IsSheafFor F (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)
Tactic: apply Presieve.IsSheafFor.isSeparatedFor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
hT : ∃ (R : CommRingCat.{u}), T = Spec R
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have obtain : ∀ (R : CommRingCat.{u}) (𝒰 : Cover (propQCPrecoverage P) (Spec R)), Presieve.IsSheafFor F 𝒰.presieve₀
Tactic: obtain ⟨R, rfl⟩ := hT
Cleared hypotheses: T, 𝒰, hT
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have inr : ∀
  (this :
    ∀ (R : CommRingCat.{u}) (𝒰 : Cover (propQCPrecoverage P) (Spec R))
      (h𝒰 : (∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀), Presieve.IsSheafFor F 𝒰.presieve₀)
  (h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀)), Presieve.IsSheafFor F 𝒰.presieve₀
Tactic: wlog h𝒰 : (∀ i, IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ generalizing R 𝒰
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
inr :
  ∀
    (this :
      ∀ (R : CommRingCat.{u}) (𝒰 : Cover (propQCPrecoverage P) (Spec R))
        (h𝒰 : (∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀), Presieve.IsSheafFor F 𝒰.presieve₀)
    (h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀)), Presieve.IsSheafFor F 𝒰.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have wlog : ∀ (R : CommRingCat.{u}) (𝒰 : Cover (propQCPrecoverage P) (Spec R))
  (h𝒰 : (∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀), Presieve.IsSheafFor F 𝒰.presieve₀
Tactic: wlog h𝒰 : (∀ i, IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ generalizing R 𝒰
Cleared hypotheses: R, 𝒰