awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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
refine_3 : ∀ (𝒰 : Cover (propQCPrecoverage P) T), Presieve.IsSheafFor F 𝒰.presieve₀
⊢ ∀ (E : (propQCPrecoverage P).ZeroHypercover T), Presieve.IsSheafFor F E.presieve₀

Tactic:
(𝒰 : Scheme.Cover _ _)
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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₀
wlog :
  ∀ ⦃T : Scheme.{u}⦄ (𝒰 : Cover (propQCPrecoverage P) T) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    Presieve.IsSheafFor F 𝒰.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
wlog hT : ∃ (R : CommRingCat.{u}), T = Spec R generalizing T
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
T.affineOneHypercover.isSheafFor_of_pullback hzar ?_ ?_

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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₀
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))
⊢ Presieve.IsSheafFor F (Sieve.pullback (T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
          ← Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.Presieve.ofArrows_pullback, CategoryTheory.Sieve.pullbackArrows_comm
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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 (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:
this (𝒰.pullback₂ (T.affineCover.f i)) ⟨_, rfl⟩

Premises used: CategoryTheory.Limits.limit.π, AlgebraicGeometry.Spec, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Spec.topObj, CategoryTheory.Precoverage.ZeroHypercover.pullback₂, AlgebraicGeometry.Spec.locallyRingedSpaceObj, CategoryTheory.Limits.limit, Exists.intro, AlgebraicGeometry.Scheme.affineCover, AlgebraicGeometry.Spec.sheafedSpaceObj, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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 (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:
exact this (𝒰.pullback₂ (T.affineCover.f i)) ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Precoverage.ZeroHypercover.pullback₂, Exists.intro, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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
refine_3 :
  Presieve.IsSeparatedFor F
    (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)
⊢ Presieve.IsSeparatedFor F
    (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate]

Premises used: CategoryTheory.Sieve.pullbackArrows_comm, CategoryTheory.Presieve.isSeparatedFor_iff_generate
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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
refine_3 :
  Presieve.IsSheafFor F (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)
⊢ Presieve.IsSeparatedFor F
    (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)

Tactic:
apply Presieve.IsSheafFor.isSeparatedFor

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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.IsSheafFor (X := T.affineOneHypercover.Y k) F
    (Presieve.ofArrows (fun (i_1 : 𝒰.I₀) ↦ pullback (𝒰.f i_1) (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i))
      fun (x : 𝒰.I₀) ↦ pullback.snd (𝒰.f x) (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i))

Tactic:
this (𝒰.pullback₂ _) ⟨_, rfl⟩

Premises used: CategoryTheory.Limits.limit.π, AlgebraicGeometry.Spec, AlgebraicGeometry.Spec.topObj, CategoryTheory.Precoverage.ZeroHypercover.pullback₂, AlgebraicGeometry.Spec.locallyRingedSpaceObj, CategoryTheory.Limits.limit, Exists.intro, AlgebraicGeometry.Spec.sheafedSpaceObj, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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.IsSheafFor (X := T.affineOneHypercover.Y k) F
    (Presieve.ofArrows (fun (i_1 : 𝒰.I₀) ↦ pullback (𝒰.f i_1) (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i))
      fun (x : 𝒰.I₀) ↦ pullback.snd (𝒰.f x) (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i))

Tactic:
exact this (𝒰.pullback₂ _) ⟨_, rfl⟩

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₂, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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
obtain : ∀ (R : CommRingCat.{u}) (𝒰 : Cover (propQCPrecoverage P) (Spec R)), Presieve.IsSheafFor F 𝒰.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
obtain ⟨R, rfl⟩ := hT

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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₀
wlog :
  ∀ (R : CommRingCat.{u}) (𝒰 : Cover (propQCPrecoverage P) (Spec R))
    (h𝒰 : (∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀), Presieve.IsSheafFor F 𝒰.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
wlog h𝒰 : (∀ i, IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ generalizing R 𝒰

Premises used: Finite, CategoryTheory.PreZeroHypercover.I₀, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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)
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₀)
inr :
  ∀ (𝒱 : AffineCover P (Spec R)) (f : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)) (hfin : Finite.{u + 1} (𝒱.I₀ (P := P)))
    (ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)), Presieve.IsSheafFor F 𝒰.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
obtain ⟨𝒱, f, hfin, ho⟩ := QuasiCompactCover.exists_hom 𝒰.forgetQc

Premises used: AlgebraicGeometry.QuasiCompactCover.exists_hom, AlgebraicGeometry.Scheme.Cover.forgetQc
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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)
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₀)
𝒱 : AffineCover P (Spec R)
f_1 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f_1.h₀ j)
V : Scheme
f : V ⟶ Spec R
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).X
      (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f)

Tactic:
V.affineOneHypercover.isSheafFor_of_pullback hzar (fun i ↦ ?_) (fun i j k ↦ ?_)

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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)
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₀)
𝒱 : AffineCover P (Spec R)
f_1 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f_1.h₀ j)
V : Scheme
f : V ⟶ Spec R
refine_1 :
  ∀ (i : V.affineOneHypercover.I₀),
    Presieve.IsSheafFor F
      (Sieve.pullback (V.affineOneHypercover.f i)
          (Sieve.generate
            (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).X
              (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f))).arrows
refine_2 :
  ∀ (i j : V.affineOneHypercover.I₀) (k : V.affineOneHypercover.I₁ i j),
    Presieve.IsSeparatedFor F
      (Sieve.pullback (V.affineOneHypercover.p₁ k ≫ V.affineOneHypercover.f i)
          (Sieve.generate
            (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).X
              (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f))).arrows
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).X
      (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f)

Tactic:
refine V.affineOneHypercover.isSheafFor_of_pullback hzar (fun i ↦ ?_) (fun i j k ↦ ?_)

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
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)
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₀)
𝒱 : AffineCover P (Spec R)
f_1 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f_1.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
refine_1 :
  Presieve.IsSheafFor (X := V.affineOneHypercover.X i) F
    (Presieve.ofArrows
      (fun (i_1 : (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).I₀) ↦
        pullback ((Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f i_1) (V.affineOneHypercover.f i))
      fun (x : (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).I₀) ↦
      pullback.snd ((Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f x) (V.affineOneHypercover.f i))
⊢ Presieve.IsSheafFor F
    (Sieve.pullback (V.affineOneHypercover.f i)
        (Sieve.generate
          (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).X
            (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f))).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
            ← Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.Presieve.ofArrows_pullback, CategoryTheory.Sieve.pullbackArrows_comm