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)
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 (Spec.map φ))
have refine_1 : P (Spec.map φ)
Tactic: refine 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
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
refine_1 : P (Spec.map φ)
⊢ Presieve.IsSheafFor F (Presieve.singleton (Spec.map φ))
have refine_2 : Surjective (Spec.map φ)
Tactic: refine 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
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
⊢ Surjective (Spec.map φ)
have refine_2 : Surjective (X := Spec Γ(∐ 𝒰.X, ⊤)) (Iso.inv (∐ 𝒰.X).isoSpec ≫ Sigma.desc 𝒰.f)
Tactic: simp only [hφ, f, Cover.sigma_I₀, PUnit.default_eq_unit, Cover.sigma_X, Cover.sigma_f, f]
-- 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)
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
⊢ Surjective (X := Spec Γ(∐ 𝒰.X, ⊤)) (Iso.inv (∐ 𝒰.X).isoSpec ≫ Sigma.desc 𝒰.f)
have this₁ : Surjective (X := ∐ 𝒰.X) (Sigma.desc 𝒰.f)
Tactic: have : Surjective (Sigma.desc 𝒰.f) := inferInstanceAs <| Surjective (Sigma.desc 𝒰.forgetQc.f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
⊢ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P))) =
    Sieve.ofArrows 𝒰.X 𝒰.f
have h : ∀ ⦃V : Scheme.{u}⦄ (f : V ⟶ X.left),
  Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P)))) f ↔
    (Sieve.ofArrows 𝒰.X 𝒰.f).arrows f
Tactic: ext V f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
⊢ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P)))) f ↔
    (Sieve.ofArrows 𝒰.X 𝒰.f).arrows f
have h : (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
    𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f sorry) ↔
  ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
Tactic: simp only [Sieve.overEquiv_iff, Sieve.generate_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
      𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯) ↔
    ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
have h : (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
    𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f sorry) →
  ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
h :
  (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
      𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯) →
    ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
⊢ (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
      𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯) ↔
    ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
have h₁ : (∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f) →
  ∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
    𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (hypothesis)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
⊢ ∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
    𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯
have this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
Tactic: have : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S := comp_over (𝒰.f k) S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ ∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
    𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯
have h₁ : Eq (α := CategoryTheory.Over.mk (f ≫ X.hom) ⟶ X)
  (CategoryStruct.comp (Y := (𝒰.X k).asOver S) (Over.homMk h sorry) (Hom.asOver (𝒰.f k) S)) (Over.homMk f sorry)
Tactic: refine ⟨(𝒰.X k).asOver S, Over.homMk h (by simp [← hcomp, this]), (𝒰.f k).asOver S, ⟨k⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ Eq (α := CategoryTheory.Over.mk (f ≫ X.hom) ⟶ X)
    (CategoryStruct.comp (Y := (𝒰.X k).asOver S) (Over.homMk h ⋯) (Hom.asOver (𝒰.f k) S)) (Over.homMk f ⋯)
have h₁ : Eq (α := (CategoryTheory.Over.mk (f ≫ X.hom)).left ⟶ X.left)
  (Over.Hom.left (CategoryStruct.comp (Y := (𝒰.X k).asOver S) (Over.homMk h sorry) (Hom.asOver (𝒰.f k) S)))
  (Over.Hom.left (Over.homMk f sorry))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
⊢ 𝒰.toPresieveOver (P := P) ≤ R.arrows ↔
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
have simp_rw : LE.le (α := Sieve X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P))) : Sieve X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) ↔
  Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R
Tactic: simp_rw [← Sieve.giGenerate.gc.le_iff_le, ← Sieve.overEquiv_le_overEquiv_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
⊢ LE.le (α := Sieve X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P))) : Sieve X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) ↔
    Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R
have rw : Sieve.ofArrows 𝒰.X 𝒰.f ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R ↔
  Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R
Tactic: rw [overEquiv_generate_toPresieveOver_eq_ofArrows]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
Y X : Over S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S (P := P) 𝒰
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (Presieve.pullbackArrows f (𝒰.toPresieveOver (P := P)))
have refine : Presieve.pullbackArrows f (𝒰.toPresieveOver (P := P)) =
  (Cover.pullbackCoverOver' (P := P) S 𝒰 (Over.Hom.left f)).toPresieveOver (P := P)
Tactic: refine ⟨𝒰.pullbackCoverOver' S f.left, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
H :
  ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f),
    Membership.mem (γ := Set (Presieve Y))
      {R : Presieve Y |
        ∃ (𝒰 : Cover (precoverage P) Y.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
      (T f H)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (𝒰.toPresieveOver (P := P).bind T)
have choose : ∀ (V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left)
  (h_1 : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H))
  (hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)),
  Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (𝒰.toPresieveOver (P := P).bind T)
Tactic: choose V h hV using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h_1 : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (𝒰.toPresieveOver (P := P).bind T)
have refine : 𝒰.toPresieveOver (P := P).bind T =
  Cover.toPresieveOver (P := P) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ V (Hom.asOver (𝒰.f j) S) sorry)
Tactic: refine ⟨𝒰.bind (fun j => V ((𝒰.f j).asOver S) ⟨j⟩), inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h_1 : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)
⊢ 𝒰.toPresieveOver (P := P).bind T =
    Cover.toPresieveOver (P := P) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ V (Hom.asOver (𝒰.f j) S) ⋯)
have h₁ : Presieve X = Presieve (C := Over S) (OverClass.asOver X.left S) →
  X = OverClass.asOver X.left S →
    HEq (𝒰.toPresieveOver (P := P)) (β := Presieve (C := Over S) (OverClass.asOver X.left S))
        (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ OverClass.asOver (𝒰.X j) S) fun (j : 𝒰.I₀) ↦ Hom.asOver (𝒰.f j) S) →
      ∀ (x : Over S) (x_1 : x ⟶ X) (x_2 : 𝒰.toPresieveOver (P := P) x_1),
        T x_1 x_2 =
          Presieve.ofArrows (fun (j : (V x_1 x_2).I₀) ↦ ((V x_1 x_2).X j).asOver S) fun (j : (V x_1 x_2).I₀) ↦
            Hom.asOver ((V x_1 x_2).f j) S
Tactic: convert!
      Presieve.ofArrows_bind _ (fun j ↦ (𝒰.f j).asOver S) _ (fun Y f H j ↦ ((V f H).X j).asOver S)
        (fun Y f H j ↦ ((V f H).f j).asOver S)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
⊢ overGrothendieckTopology P S = (overPretopology P S).toGrothendieck
have h : ∀ (X : Over S) (R : Sieve X),
  R ∈ (overGrothendieckTopology P S : (a : Over S) → Set (Sieve a)) X ↔
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
Tactic: ext X R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
⊢ Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
      ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) ↔
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
have h : Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) →
  R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
h :
  Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
      ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) →
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
⊢ Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
      ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) ↔
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
have h₁ : R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X →
  Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
hR :
  Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
have h : ∀ (𝒰 : Cover (precoverage P) X.left)
  (hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)),
  R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
Tactic: obtain ⟨𝒰, hle⟩ := exists_cover_of_mem_grothendieckTopology hR
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
hR :
  Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
have h : ∀
  (hR :
    ∃ (𝒰 : Cover (precoverage P) X.left),
      Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R))
  (𝒰 : Cover (precoverage P) X.left)
  (hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)),
  R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
Tactic: rw [mem_grothendieckTopology_iff] at hR
Cleared hypotheses: hR, 𝒰, hle
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
hR :
  ∃ (𝒰 : Cover (precoverage P) X.left),
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
this_1 : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
have right : 𝒰.toPresieveOver (P := P) ≤ R.arrows
Tactic: use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
hT : 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)
have h₁ : ∃ (𝒰 : Cover (precoverage P) X.left),
  Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
Tactic: rw [mem_grothendieckTopology_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
hT : 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X.left),
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
have h₁ : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
Tactic: use 𝒰
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
hT : 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
have h₁ : ∀ (hT : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)),
  Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
Tactic: rwa [Cover.toPresieveOver_le_arrows_iff] at hT
Cleared hypotheses: hT