awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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₀
have 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₀
Tactic: obtain ⟨𝒱, f, hfin, ho⟩ := QuasiCompactCover.exists_hom 𝒰.forgetQc
-- 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)
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)
have 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
Tactic: refine V.affineOneHypercover.isSheafFor_of_pullback hzar (fun i ↦ ?_) (fun i j k ↦ ?_)
-- 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)
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
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).X
      (Precoverage.ZeroHypercover.pullback₂ f (𝒱.cover (P := P))).f)
have 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
Tactic: refine V.affineOneHypercover.isSheafFor_of_pullback hzar (fun i ↦ ?_) (fun i j k ↦ ?_)
-- 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)
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₀
⊢ 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
have 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))
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))
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 𝒰'.toPreZeroHypercover
have dsimp : QuasiCompactCover
  (PreZeroHypercover.pullback₂ (V.affineCover.f i) (PreZeroHypercover.pullback₂ f 𝒱.cover (P := P).toPreZeroHypercover))
Tactic: dsimp [𝒰']
-- 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)
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 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
have 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))
Tactic: rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
            ← Presieve.isSeparatedFor_iff_generate]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (hypothesis)
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)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have 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)
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
-- 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)
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₀
have inr : Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.cover (P := P).X 𝒱.cover (P := P).f)
Tactic: refine f.isSheafFor_iff ?_ fun f ↦ (H _ f).isSeparatedFor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (hypothesis)
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₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
Tactic: obtain ⟨_, _⟩ := h𝒰
Cleared hypotheses: h𝒰
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (hypothesis)
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)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have right : Finite.{u + 1} 𝒰.I₀
Tactic: obtain ⟨_, _⟩ := h𝒰
Cleared hypotheses: h𝒰
-- 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)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
have rw : Presieve.IsSheafFor F
  (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
    (𝒰.forgetQc (P := P).sigma (P := P).f default))
Tactic: rw [← Scheme.Cover.forgetQc_toPreZeroHypercover,
      ← Scheme.Cover.isSheafFor_sigma_iff hzar, Presieve.ofArrows_of_unique]
-- 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)
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} (𝒰.forgetQc (P := P).sigma (P := P).X default)
have dsimp : IsAffine.{u} (∐ 𝒰.X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact (hypothesis)
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)
⊢ Presieve.IsSheafFor F
    (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
      (𝒰.forgetQc (P := P).sigma (P := P).f default))
have this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
Tactic: have : IsAffine (𝒰.forgetQc.sigma.X default) := by dsimp; infer_instance
-- 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)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
⊢ Presieve.IsSheafFor F
    (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
      (𝒰.forgetQc (P := P).sigma (P := P).f default))
have obtain : ∀ (φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)) (hφ : Spec.map φ = f),
  Presieve.IsSheafFor F
    (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
      (𝒰.forgetQc (P := P).sigma (P := P).f default))
Tactic: obtain ⟨φ, hφ⟩ := Spec.map_surjective f
-- 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)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Presieve.IsSheafFor F
    (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
      (𝒰.forgetQc (P := P).sigma (P := P).f default))
have rw : Presieve.IsSheafFor F (Presieve.singleton (Spec.map φ))
Tactic: rw [Presieve.isSheafFor_singleton_iff_of_iso _ (Spec.map φ)
      (𝒰.forgetQc.sigma.X default).isoSpec (by simp [hφ, f])]