awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰_1 𝒰_2 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover.{w, u, u + 1} X
inst : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover.{w, u, u + 1} (𝒰.X x)
inst_1 : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU_1 : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥X)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥X)
this :
  ∀ (i : 𝒰.I₀) (hi : i ∈ s),
    IsCompactOpenCovered (X := fun (x : (f i).I₀) ↦ ↥((f i).X x)) (fun (x : (f i).I₀) ↦ ⇑((f i).f x))
      (↑(V i hi) : Set ↥(𝒰.X i))
⊢ IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)
have choose : ∀ (t : (i : 𝒰.I₀) → (hi : i ∈ s) → Set (f i).I₀) (ht : ∀ (i : 𝒰.I₀) (hi : i ∈ s), (t i hi).Finite)
  (W :
    (i : 𝒰.I₀) →
      (hi : i ∈ s) → (i_1 : (f i).I₀) → i_1 ∈ t i hi → TopologicalSpace.Opens ((fun (x : (f i).I₀) ↦ ↥((f i).X x)) i_1))
  (hcW : ∀ (i : 𝒰.I₀) (hi : i ∈ s) (i_1 : (f i).I₀) (h : i_1 ∈ t i hi), IsCompact (W i hi i_1 h).carrier)
  (hV :
    ∀ (i : 𝒰.I₀) (hi : i ∈ s),
      ⋃ (i_1 : (f i).I₀),
          ⋃ (h : i_1 ∈ t i hi),
            (fun (x : (f i).I₀) ↦ (⇑((f i).f x) : (a : ↥((f i).X x)) → ↥(𝒰.X i))) i_1 ''
              (↑(W i hi i_1 h) : Set ((fun (x : (f i).I₀) ↦ ↥((f i).X x)) i_1)) =
        (↑(V i hi) : Set ↥(𝒰.X i))),
  IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)
Tactic: choose t ht W hcW hV using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (hypothesis)
Goal:
S : Scheme
𝒰_1 𝒰_2 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover.{w, u, u + 1} X
inst : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover.{w, u, u + 1} (𝒰.X x)
inst_1 : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU_1 : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥X)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥X)
t : (i : 𝒰.I₀) → (hi : i ∈ s) → Set (f i).I₀
ht : ∀ (i : 𝒰.I₀) (hi : i ∈ s), (t i hi).Finite
W :
  (i : 𝒰.I₀) →
    (hi : i ∈ s) → (i_1 : (f i).I₀) → i_1 ∈ t i hi → TopologicalSpace.Opens ((fun (x : (f i).I₀) ↦ ↥((f i).X x)) i_1)
hcW : ∀ (i : 𝒰.I₀) (hi : i ∈ s) (i_1 : (f i).I₀) (h : i_1 ∈ t i hi), IsCompact (W i hi i_1 h).carrier
hV :
  ∀ (i : 𝒰.I₀) (hi : i ∈ s),
    ⋃ (i_1 : (f i).I₀),
        ⋃ (h : i_1 ∈ t i hi),
          (fun (x : (f i).I₀) ↦ (⇑((f i).f x) : (a : ↥((f i).X x)) → ↥(𝒰.X i))) i_1 ''
            (↑(W i hi i_1 h) : Set ((fun (x : (f i).I₀) ↦ ↥((f i).X x)) i_1)) =
      (↑(V i hi) : Set ↥(𝒰.X i))
⊢ IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)
have this : Finite.{w + 1} (↑s : Type w)
Tactic: have : Finite s := hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (hypothesis)
Goal:
S : Scheme
𝒰_1 𝒰_2 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover.{w, u, u + 1} X
inst : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover.{w, u, u + 1} (𝒰.X x)
inst_1 : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU_1 : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥X)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥X)
t : (i : 𝒰.I₀) → (hi : i ∈ s) → Set (f i).I₀
ht : ∀ (i : 𝒰.I₀) (hi : i ∈ s), (t i hi).Finite
W :
  (i : 𝒰.I₀) →
    (hi : i ∈ s) → (i_1 : (f i).I₀) → i_1 ∈ t i hi → TopologicalSpace.Opens ((fun (x : (f i).I₀) ↦ ↥((f i).X x)) i_1)
hcW : ∀ (i : 𝒰.I₀) (hi : i ∈ s) (i_1 : (f i).I₀) (h : i_1 ∈ t i hi), IsCompact (W i hi i_1 h).carrier
hV :
  ∀ (i : 𝒰.I₀) (hi : i ∈ s),
    ⋃ (i_1 : (f i).I₀),
        ⋃ (h : i_1 ∈ t i hi),
          (fun (x : (f i).I₀) ↦ (⇑((f i).f x) : (a : ↥((f i).X x)) → ↥(𝒰.X i))) i_1 ''
            (↑(W i hi i_1 h) : Set ((fun (x : (f i).I₀) ↦ ↥((f i).X x)) i_1)) =
      (↑(V i hi) : Set ↥(𝒰.X i))
this : Finite.{w + 1} (↑s : Type w)
⊢ IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)
have this₁ : ∀ (i : 𝒰.I₀) (hi : i ∈ s), Finite.{w + 1} (↑(t i hi) : Type w)
Tactic: have (i) (hi) : Finite (t i hi) := ht i hi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰_1 𝒰_2 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
𝒰 : Scheme.Cover.{u_1, u} K S
inst : Scheme.JointlySurjective K
inst_1 : ∀ (i : 𝒰.I₀), QuasiCompact (𝒰.f i)
inst_2 : Finite.{u_1 + 1} 𝒰.I₀
U : S.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
have refine : ∀ x ∈ (↑U : Set ↥S), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x
Tactic: refine .of_finite_of_isSpectralMap (fun i ↦ (𝒰.f i).isSpectralMap) ?_ U.2 hU.isCompact
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : IsEmpty.{u + 1} ↥S
U : S.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
have h : (↑U : Set ↥S) = ∅
Tactic: convert! IsCompactOpenCovered.empty
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
have obtain : ∀ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens) (hV : ∀ (i : Fin n), IsAffineOpen (V i))
  (h : ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑⊤ : Set ↥S)),
  ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
Tactic: obtain ⟨n, f, V, hV, h⟩ := QuasiCompactCover.exists_isAffineOpen_of_isCompact 𝒰.1
    (show IsCompact (⊤ : TopologicalSpace.Opens S).carrier from isCompact_univ)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (hypothesis)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
h : ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑⊤ : Set ↥S)
⊢ ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
have h₁ : ∀ (x : ↥S), ∃ (i : Fin n), ∃ x_1 ∈ V i, (𝒰.f (f i)) x_1 = x
Tactic: simp only [coe_top, ← Set.univ_subset_iff, Set.subset_def, Set.mem_univ, Set.mem_iUnion,
    Set.mem_image, SetLike.mem_coe, forall_const] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
h : ∀ (x : ↥S), ∃ (i : Fin n), ∃ x_1 ∈ V i, (𝒰.f (f i)) x_1 = x
⊢ ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
have choose : ∀ (idx : (x : ↥S) → Fin n) (x : (x : ↥S) → ↥(𝒰.X (f (idx x))))
  (hmem : ∀ (x_1 : ↥S), Membership.mem (γ := (𝒰.X (f (idx x_1))).Opens) (V (idx x_1)) (x x_1))
  (hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1),
  ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
Tactic: choose idx x hmem hx using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : (x : ↥S) → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), Membership.mem (γ := (𝒰.X (f (idx x_1))).Opens) (V (idx x_1)) (x x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
have refine_1 : Scheme.AffineCover.{w, u} P S
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : (x : ↥S) → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), Membership.mem (γ := (𝒰.X (f (idx x_1))).Opens) (V (idx x_1)) (x x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
refine_1 : Scheme.AffineCover.{w, u} P S
⊢ ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
have refine_2 : Scheme.AffineCover.cover (P := P)
    (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
      (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
      (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f i.down)) (fun (s : ↥S) ↦ { down := idx s }) sorry
      sorry) ⟶
  𝒰
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : (x : ↥S) → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), Membership.mem (γ := (𝒰.X (f (idx x_1))).Opens) (V (idx x_1)) (x x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
refine_1 : Scheme.AffineCover.{w, u} P S
refine_2 :
  Scheme.AffineCover.cover (P := P)
      (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
        (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
        (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec ⋯ ≫ 𝒰.f (f i.down)) (fun (s : ↥S) ↦ { down := idx s }) ⋯
        ⋯) ⟶
    𝒰
⊢ ∃ (𝒱 : Scheme.AffineCover.{w, u} P S) (f : 𝒱.cover (P := P) ⟶ 𝒰),
    Finite.{w + 1} (𝒱.I₀ (P := P)) ∧ ∀ (j : 𝒱.cover (P := P).I₀), IsOpenImmersion (f.h₀ j)
have refine_3 : Finite.{w + 1}
  (Scheme.AffineCover.I₀ (P := P) (S := S)
    (Scheme.AffineCover.mk (P := P) (ULift.{w, 0} (Fin n))
      (fun (i : ULift.{w, 0} (Fin n)) ↦ Γ(𝒰.X (f i.down), V i.down))
      (fun (i : ULift.{w, 0} (Fin n)) ↦ IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f i.down)) (fun (s : ↥S) ↦ { down := idx s }) sorry
      sorry))
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : (x : ↥S) → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), Membership.mem (γ := (𝒰.X (f (idx x_1))).Opens) (V (idx x_1)) (x x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
s : ↥S
⊢ Membership.mem (γ := Set ↥S)
    (Set.range (ι :=
      ↥(Spec Γ(𝒰.X (f { down := idx s }.down), V (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) }))))
      ⇑(IsAffineOpen.fromSpec ⋯ ≫ 𝒰.f (f (ULift.down.{w, 0} { down := idx s }))))
    s
have h : (IsAffineOpen.fromSpec sorry ≫ 𝒰.f (f (ULift.down.{w, 0} { down := idx s })))
    ((Iso.hom (IsAffineOpen.isoSpec sorry))
        (Subtype.mk (p := fun (x : ↥(𝒰.X (f (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) })))) ↦
          Membership.mem (γ :=
            TopologicalSpace.Opens ↥(𝒰.X (f (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) }))))
            (V (ULift.down.{w, 0} { down := idx s })) x)
          (x s) sorry) :
      ↥(Spec Γ(𝒰.X (f { down := idx s }.down), V (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) })))) =
  s
Tactic: use (hV _).isoSpec.hom.base ⟨x s, hmem s⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover.{w, u} (Scheme.precoverage P) S
inst : P.RespectsLeft IsOpenImmersion
inst_1 : CompactSpace.{u} ↥S
inst_2 : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : (x : ↥S) → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), Membership.mem (γ := (𝒰.X (f (idx x_1))).Opens) (V (idx x_1)) (x x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
s : ↥S
⊢ (IsAffineOpen.fromSpec ⋯ ≫ 𝒰.f (f (ULift.down.{w, 0} { down := idx s })))
      ((Iso.hom (IsAffineOpen.isoSpec ⋯))
          (Subtype.mk (p := fun (x : ↥(𝒰.X (f (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) })))) ↦
            Membership.mem (γ :=
              TopologicalSpace.Opens ↥(𝒰.X (f (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) }))))
              (V (ULift.down.{w, 0} { down := idx s })) x)
            (x s) ⋯) :
        ↥(Spec Γ(𝒰.X (f { down := idx s }.down), V (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) })))) =
    s
have h : (Scheme.Opens.ι (V (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) })) ≫
      𝒰.f (f (ULift.down.{w, 0} { down := idx s })))
    (Subtype.mk (p := fun (x : ↥(𝒰.X (f (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) })))) ↦
      Membership.mem (γ :=
        TopologicalSpace.Opens ↥(𝒰.X (f (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) }))))
        (V (ULift.down.{w, 0} { down := idx s : ULift.{w, 0} (Fin n) })) x)
      (x s) sorry) =
  s
Tactic: rw [← Scheme.Hom.comp_apply, ← IsAffineOpen.isoSpec_inv_ι, Category.assoc,
            Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
⊢ PreZeroHypercover.presieve₀.{v, u, u + 1}
      { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f } ∈
    (precoverage P).coverings S
have rw : (∀ (x : ↥S),
    ∃ (i :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
        { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
      Membership.mem (γ := Set ↥S)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
        { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
    P
      (PreZeroHypercover.f
        { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
          PreZeroHypercover.{v, u, u + 1} S }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
⊢ (∀ (x : ↥S),
      ∃ (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
          { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
        Membership.mem (γ := Set ↥S)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                  f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                  f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
          { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
      P
        (PreZeroHypercover.f
          { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
            PreZeroHypercover.{v, u, u + 1} S }
          i)
have refine : ∀ (s : ↥S),
  ∃ (i :
    PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
      { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
    Membership.mem (γ := Set ↥S)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i))
      s
Tactic: refine ⟨fun s ↦ ?_, fun _ ↦ IsZariskiLocalAtSource.sigmaDesc 𝒰.map_prop⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
s : ↥S
⊢ ∃ (i :
    PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
      { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
    Membership.mem (γ := Set ↥S)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i))
      s
have obtain : ∀ (i : 𝒰.I₀) (y : ↥(𝒰.X i)),
  ∃ (i_1 :
    PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
      { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
    Membership.mem (α := ↥S) (γ := Set ↥S)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i_1))
        ⇑(PreZeroHypercover.f
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i_1))
      ((𝒰.f i) y : ↥S)
Tactic: obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
S : Scheme
𝒰 : Cover.{v, u} (precoverage P) S
⊢ PreZeroHypercover.presieve₀.{v, u, u + 1} 𝒰.sigma (P := P).toPreZeroHypercover =
    Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f)
have refine : PreZeroHypercover.presieve₀.{v, u, u + 1} 𝒰.sigma (P := P).toPreZeroHypercover ≤
  Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f)
Tactic: refine le_antisymm ?_ fun T g ⟨⟩ ↦ ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
S : Scheme
𝒰 : Cover.{v, u} (precoverage P) S
⊢ PreZeroHypercover.presieve₀.{v, u, u + 1} 𝒰.sigma (P := P).toPreZeroHypercover ≤
    Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f)
have rw : ∀ (i : 𝒰.sigma (P := P).I₀), Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f) (𝒰.sigma (P := P).f i)
Tactic: rw [Presieve.ofArrows_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰_1 𝒱 𝒰 : Cover.{v, u} (precoverage P) S
⊢ HEq (α :=
    (i : 𝒰.sigma (P := P).I₀) →
      𝒰.sigma (P := P).X i ⟶ 𝒰.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) (𝟙 𝒰)) i))
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰))) (PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P))))
have simp : PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) = PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P)))
Tactic: simp only [sigma_I₀, sigma_X, heq_eq_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰_1 𝒱 𝒰 : Cover.{v, u} (precoverage P) S
⊢ PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) = PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P)))
have h : ∀ (j : 𝒰.sigma (P := P).I₀),
  PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) j = PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P))) j
Tactic: ext j : 1