awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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_1 : Finite.{w + 1} (↑s : Type w)
this : ∀ (i : 𝒰.I₀) (hi : i ∈ s), Finite.{w + 1} (↑(t i hi) : Type w)
⊢ ⋃ (k : (i : (↑s : Type w)) × (↑(t (↑i : 𝒰.I₀) ⋯) : Type w)),
      ⇑((𝒰.bind f).f
            ((fun (p : (i : (↑s : Type w)) × (↑(t (↑i : 𝒰.I₀) ⋯) : Type w)) ↦
                (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (f i).I₀)
                    (↑(p.fst (β := fun (i : (↑s : Type w)) ↦ (↑(t (↑i : 𝒰.I₀) ⋯) : Type w))) : 𝒰.I₀)
                    (↑(p.snd (β := fun (i : (↑s : Type w)) ↦ (↑(t (↑i : 𝒰.I₀) ⋯) : Type w))) : (f (↑p.fst : 𝒰.I₀)).I₀) :
                  (i : 𝒰.I₀) × (f i).I₀))
              k)) ''
        (↑((fun (p : (i : (↑s : Type w)) × (↑(t (↑i : 𝒰.I₀) ⋯) : Type w)) ↦
                W (↑(p.fst (β := fun (i : (↑s : Type w)) ↦ (↑(t (↑i : 𝒰.I₀) ⋯) : Type w))) : 𝒰.I₀) ⋯
                  (Sigma.snd (β := fun (i : 𝒰.I₀) ↦ (f i).I₀)
                    ((fun (p : (i : (↑s : Type w)) × (↑(t (↑i : 𝒰.I₀) ⋯) : Type w)) ↦
                        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (f i).I₀)
                            (↑(p.fst (β := fun (i : (↑s : Type w)) ↦ (↑(t (↑i : 𝒰.I₀) ⋯) : Type w))) : 𝒰.I₀)
                            (↑(p.snd (β := fun (i : (↑s : Type w)) ↦ (↑(t (↑i : 𝒰.I₀) ⋯) : Type w))) :
                              (f (↑p.fst : 𝒰.I₀)).I₀) :
                          (i : 𝒰.I₀) × (f i).I₀))
                      p))
                  ⋯)
              k) :
          Set
            ↥((𝒰.bind f).X
                ((fun (p : (i : (↑s : Type w)) × (↑(t (↑i : 𝒰.I₀) ⋯) : Type w)) ↦
                    ⟨(↑p.fst : 𝒰.I₀), (↑p.snd : (f (↑p.fst : 𝒰.I₀)).I₀)⟩)
                  k))) =
    (↑U : Set ↥X)

Tactic:
simpa [← hV, Set.iUnion_sigma, Set.iUnion_subtype, Set.image_iUnion, Set.image_image] using hU

Premises used: Set.image_image, Set.iUnion_sigma, Set.image_iUnion, Set.iUnion_subtype
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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)

Tactic:
.of_finite_of_isSpectralMap (fun i ↦ (𝒰.f i).isSpectralMap) ?_ U.2 hU.isCompact

Premises used: IsCompactOpenCovered.of_finite_of_isSpectralMap, AlgebraicGeometry.IsAffineOpen.isCompact, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.isSpectralMap, TopologicalSpace.Opens.is_open', CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
refine : ∀ x ∈ (↑U : Set ↥S), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)

Tactic:
refine .of_finite_of_isSpectralMap (fun i ↦ (𝒰.f i).isSpectralMap) ?_ U.2 hU.isCompact
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
⊢ ∀ x ∈ (↑U : Set ↥S), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x

Tactic:
(fun x _ ↦ ⟨𝒰.idx x, 𝒰.covers x⟩)

Premises used: AlgebraicGeometry.Scheme.Cover.covers, Exists.intro, AlgebraicGeometry.Scheme.Cover.idx
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
⊢ ∀ x ∈ (↑U : Set ↥S), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x

Tactic:
exact (fun x _ ↦ ⟨𝒰.idx x, 𝒰.covers x⟩)
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰_2 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : IsAffine S
P : MorphismProperty Scheme
𝒰 : Scheme.AffineCover.{u_1, u} P S
inst_1 : Finite.{u_1 + 1} (𝒰.I₀ (P := P))
⊢ QuasiCompactCover 𝒰.cover (P := P).toPreZeroHypercover

Tactic:
haveI : Finite 𝒰.cover.I₀ := ‹_›
  .of_finite

Premises used: AlgebraicGeometry.QuasiCompactCover.of_finite
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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 (S := ↥S) (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) ∅

Tactic:
IsCompactOpenCovered.empty

Premises used: IsCompactOpenCovered.empty
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : IsEmpty.{u + 1} ↥S
U : S.Opens
hU : IsAffineOpen U
h : (↑U : Set ↥S) = ∅
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)

Tactic:
convert! IsCompactOpenCovered.empty

Premises used: IsCompactOpenCovered.empty
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : IsEmpty.{u + 1} ↥S
U : S.Opens
hU : IsAffineOpen U
⊢ (↑U : Set ↥S) = ∅

Tactic:
simp [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S_1 : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S_1
K : Precoverage Scheme
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
⊢ QuasiCompactCover (Scheme.Hom.cover (P := P) f hf).toPreZeroHypercover

Tactic:
have _ (i) : AlgebraicGeometry.QuasiCompact ((f.cover hf).f i) := ‹_›
  .of_finite

Premises used: AlgebraicGeometry.QuasiCompactCover.of_finite
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
P : MorphismProperty Scheme
X : Scheme
f : X ⟶ S
inst : Surjective f
inst_1 : QuasiCompact f
⊢ QuasiCompactCover (PreZeroHypercover.singleton f)

Tactic:
homCover (P := ⊤) f trivial

Premises used: trivial, CategoryTheory.PreZeroHypercover.singleton, AlgebraicGeometry.QuasiCompactCover.homCover
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
P_1 P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : P.RespectsIso
X Y : Scheme
f : X ⟶ Y
inst_2 : IsIso f
⊢ QuasiCompactCover
    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage P) (Scheme.coverOfIsIso (P := P) f))

Tactic:
of_isOpenMap (fun _ ↦ f.homeomorph.isOpenMap)

Premises used: AlgebraicGeometry.QuasiCompactCover.of_isOpenMap, AlgebraicGeometry.Scheme.Hom.homeomorph, Homeomorph.isOpenMap
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
P : MorphismProperty Scheme
𝒱 : PreZeroHypercover.{u_1, u, u + 1} S
inst : QuasiCompactCover 𝒰
⊢ QuasiCompactCover (𝒰.sum 𝒱)

Tactic:
.of_hom (PreZeroHypercover.sumInl _ _)

Premises used: AlgebraicGeometry.QuasiCompactCover.of_hom, CategoryTheory.PreZeroHypercover.sumInl
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
P : MorphismProperty Scheme
𝒱 : PreZeroHypercover.{u_1, u, u + 1} S
inst : QuasiCompactCover 𝒱
⊢ QuasiCompactCover (𝒰.sum 𝒱)

Tactic:
.of_hom (PreZeroHypercover.sumInr _ _)

Premises used: AlgebraicGeometry.QuasiCompactCover.of_hom, CategoryTheory.PreZeroHypercover.sumInr
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
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)
⊢ ∃ (𝒱 : 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)

Premises used: isCompact_univ, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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)
⊢ ∀ (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

Premises used: Set.univ_subset_iff, Set.subset_def, Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, Set.mem_univ, forall_const, TopologicalSpace.Opens.coe_top
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
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)
⊢ ∃ (𝒱 : 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
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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)

Tactic:
⟨?_, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
h :
  (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
⊢ 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

Tactic:
use (hV _).isoSpec.hom.base ⟨x s, hmem s⟩

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
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) ⋯) =
    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

Tactic:
rw [← Scheme.Hom.comp_apply, ← IsAffineOpen.isoSpec_inv_ι, Category.assoc,
            Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Iso.hom_inv_id_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
⊢ (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) ⋯) =
    s

Tactic:
simp [hx]
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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

Tactic:
exact
      { I₀ := ULift (Fin n)
        X i := Γ(_, V i.down)
        f i := (hV _).fromSpec ≫ 𝒰.f (f _)
        idx s := ⟨idx s⟩
        covers s := by
          use (hV _).isoSpec.hom.base ⟨x s, hmem s⟩
          rw [← Scheme.Hom.comp_apply, ← IsAffineOpen.isoSpec_inv_ι, Category.assoc,
            Iso.hom_inv_id_assoc]
          simp [hx]
        map_prop i :=
          RespectsLeft.precomp (Q := IsOpenImmersion) _ inferInstance _ (𝒰.map_prop _) }
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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.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 }) ⋯
        ⋯) ⟶
    𝒰

Tactic:
exact
      { s₀ i := f i.down
        h₀ i := (hV i.down).fromSpec }
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
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
⊢ 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 ⋯ ≫ 𝒰.f (f i.down)) (fun (s : ↥S) ↦ { down := idx s }) ⋯
        ⋯))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
⊢ S.quasiCompactCover 𝒰 ↔ QuasiCompactCover 𝒰

Tactic:
.rfl

Premises used: Iff.rfl, AlgebraicGeometry.Scheme.quasiCompactCover
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
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)
⊢ 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

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
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)

Tactic:
⟨fun s ↦ ?_, fun _ ↦ IsZariskiLocalAtSource.sigmaDesc 𝒰.map_prop⟩

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc, And.intro, AlgebraicGeometry.Scheme.Cover.map_prop