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))
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₀
𝒰' : (precoverage P).ZeroHypercover (V.affineCover.X i) :=
  Precoverage.ZeroHypercover.pullback₂ (V.affineCover.f i) (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P)))
dsimp :
  QuasiCompactCover
    (PreZeroHypercover.pullback₂ (V.affineCover.f i)
      (PreZeroHypercover.pullback₂ f 𝒱.cover (P := P).toPreZeroHypercover))
⊢ QuasiCompactCover 𝒰'.toPreZeroHypercover

Tactic:
dsimp [𝒰']
-- 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₀
𝒰' : (precoverage P).ZeroHypercover (V.affineCover.X i) :=
  Precoverage.ZeroHypercover.pullback₂ (V.affineCover.f i) (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P)))
⊢ QuasiCompactCover
    (PreZeroHypercover.pullback₂ (V.affineCover.f i)
      (PreZeroHypercover.pullback₂ f 𝒱.cover (P := P).toPreZeroHypercover))

Tactic:
infer_instance
-- 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₀
𝒰' : (precoverage P).ZeroHypercover (V.affineCover.X i) :=
  Precoverage.ZeroHypercover.pullback₂ (V.affineCover.f i) (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P)))
⊢ 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))

Tactic:
exact this _ (.ofQuasiCompactCover 𝒰' (qc := by dsimp [𝒰']; infer_instance))
            ⟨fun j ↦ .of_isIso (pullbackLeftPullbackSndIso (𝒱.f j) f (V.affineCover.f i)).hom, hfin⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsAffine.of_isIso, CategoryTheory.Limits.pullbackLeftPullbackSndIso, AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover, AlgebraicGeometry.Scheme.AffineCover.f, And.intro, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.affineCover, 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₀)
𝒱 : 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 j : V.affineOneHypercover.I₀
k : V.affineOneHypercover.I₁ i j
refine_2 :
  Presieve.IsSeparatedFor (X := V.affineOneHypercover.Y k) 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.p₁ k ≫ 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.p₁ k ≫ V.affineOneHypercover.f i))
⊢ 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

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

Premises used: CategoryTheory.Presieve.ofArrows_pullback, 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))
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 j : V.affineOneHypercover.I₀
k : V.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor (X := V.affineOneHypercover.Y k) 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.p₁ k ≫ 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.p₁ k ≫ V.affineOneHypercover.f i))

Tactic:
exact (this _ (.ofQuasiCompactCover ((𝒱.cover.pullback₂ f).pullback₂ _)
              (qc := by dsimp; infer_instance))
            ⟨fun l ↦ .of_isIso (pullbackLeftPullbackSndIso (𝒱.f l) f _).hom, hfin⟩).isSeparatedFor

Premises used: AlgebraicGeometry.IsAffine.of_isIso, CategoryTheory.Limits.pullbackLeftPullbackSndIso, CategoryTheory.Precoverage.ZeroHypercover.pullback₂, AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover, AlgebraicGeometry.Scheme.AffineCover.f, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, And.intro, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.AffineCover.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))
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 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
⊢ ∀ (V : Scheme.{u}) (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:
have H (V : Scheme.{u}) (f : V ⟶ Spec R) : Presieve.IsSheafFor F
          (.ofArrows (𝒱.cover.pullback₂ f).X (𝒱.cover.pullback₂ f).f) := by
        refine V.affineOneHypercover.isSheafFor_of_pullback hzar (fun i ↦ ?_) (fun i j k ↦ ?_)
        · rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
            ← Presieve.isSheafFor_iff_generate]
          let 𝒰' := (𝒱.cover.pullback₂ f).pullback₂ (V.affineCover.f i)
          exact this _ (.ofQuasiCompactCover 𝒰' (qc := by dsimp [𝒰']; infer_instance))
            ⟨fun j ↦ .of_isIso (pullbackLeftPullbackSndIso (𝒱.f j) f (V.affineCover.f i)).hom, hfin⟩
        · rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
            ← Presieve.isSeparatedFor_iff_generate]
          exact (this _ (.ofQuasiCompactCover ((𝒱.cover.pullback₂ f).pullback₂ _)
              (qc := by dsimp; infer_instance))
            ⟨fun l ↦ .of_isIso (pullbackLeftPullbackSndIso (𝒱.f l) f _).hom, hfin⟩).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))
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 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
H :
  ∀ (V : Scheme.{u}) (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)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
f.isSheafFor_iff ?_ fun f ↦ (H _ f).isSeparatedFor

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff
-- 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 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
H :
  ∀ (V : Scheme.{u}) (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)
inr : Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.cover (P := P).X 𝒱.cover (P := P).f)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
refine f.isSheafFor_iff ?_ fun f ↦ (H _ f).isSeparatedFor

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff
-- 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 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
H :
  ∀ (V : Scheme.{u}) (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)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.cover (P := P).X 𝒱.cover (P := P).f)

Tactic:
this _ (.ofQuasiCompactCover 𝒱.cover)
        ⟨fun i ↦ inferInstanceAs <| IsAffine (Spec _), hfin⟩

Premises used: _private.0.AlgebraicGeometry.isSheaf_type_propQCTopology_iff._proof_1, AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover, And.intro, AlgebraicGeometry.Scheme.AffineCover.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))
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 : 𝒱.cover (P := P) ⟶ 𝒰.forgetQc (P := P)
hfin : Finite.{u + 1} (𝒱.I₀ (P := P))
ho : ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
H :
  ∀ (V : Scheme.{u}) (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)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.cover (P := P).X 𝒱.cover (P := P).f)

Tactic:
exact this _ (.ofQuasiCompactCover 𝒱.cover)
        ⟨fun i ↦ inferInstanceAs <| IsAffine (Spec _), hfin⟩

Premises used: _private.0.AlgebraicGeometry.isSheaf_type_propQCTopology_iff._proof_1, AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover, And.intro, AlgebraicGeometry.Scheme.AffineCover.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))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
h𝒰 : (∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀
⊢ ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)

Tactic:
obtain ⟨_, _⟩ := h𝒰
-- 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)
h𝒰 : (∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)) ∧ Finite.{u + 1} 𝒰.I₀
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
⊢ Finite.{u + 1} 𝒰.I₀

Tactic:
obtain ⟨_, _⟩ := h𝒰
-- 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)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
rw :
  Presieve.IsSheafFor F
    (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
      (𝒰.forgetQc (P := P).sigma (P := P).f default))
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
rw [← Scheme.Cover.forgetQc_toPreZeroHypercover,
      ← Scheme.Cover.isSheafFor_sigma_iff hzar, Presieve.ofArrows_of_unique]

Premises used: AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff, AlgebraicGeometry.Scheme.Cover.forgetQc_toPreZeroHypercover, CategoryTheory.Presieve.ofArrows_of_unique
-- 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)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
dsimp : IsAffine.{u} (∐ 𝒰.X)
⊢ IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)

Tactic:
dsimp
-- 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)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
⊢ IsAffine.{u} (∐ 𝒰.X)

Tactic:
infer_instance