awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
refine_2 :
  ∀ (x : ↥T) (hx : x ∈ (↑U' : Set ↥T)),
    Membership.mem (γ := Set ↥T)
      (⋃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀),
        ⋃ (h : i ∈ s),
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
                (⇑((PreZeroHypercover.pullback₁ f 𝒰).f x) : (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) → ↥T))
              i ''
            (↑((fun (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (hi : i ∈ s) ↦
                    (pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi :
                      TopologicalSpace.Opens
                        ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
                          i)))
                  i h) :
              Set ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)))
      x
⊢ ⋃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀),
      ⋃ (h : i ∈ s),
        (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
              (⇑((PreZeroHypercover.pullback₁ f 𝒰).f x) : (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) → ↥T))
            i ''
          (↑((fun (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (hi : i ∈ s) ↦
                  (pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi :
                    TopologicalSpace.Opens
                      ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)))
                i h) :
            Set ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)) =
    (↑U' : Set ↥T)

Tactic:
refine subset_antisymm (by simp) (fun x hx ↦ ?_)

Premises used: subset_antisymm
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
⊢ Membership.mem (α := ↥S) (↑U : Set ↥S) (f x : ↥S)

Tactic:
have : f x ∈ (U : Set S) := hsub ⟨x, hx, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
this : Membership.mem (α := ↥S) (↑U : Set ↥S) (f x : ↥S)
⊢ ∃ (i : 𝒰.I₀) (i_1 : i ∈ s),
    Membership.mem (α := ↥S) (γ := Set ↥S) ((fun (a : ↥(𝒰.X i)) ↦ (𝒰.f i) a) '' (↑(V i ⋯) : Set ↥(𝒰.X i))) (f x : ↥S)

Tactic:
simp_rw [← heq, Set.mem_iUnion] at this

Premises used: Set.mem_iUnion
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
this :
  ∃ (i : 𝒰.I₀) (i_1 : i ∈ s),
    Membership.mem (α := ↥S) (γ := Set ↥S) ((fun (a : ↥(𝒰.X i)) ↦ (𝒰.f i) a) '' (↑(V i ⋯) : Set ↥(𝒰.X i))) (f x : ↥S)
refine_2 :
  ∀ (i : 𝒰.I₀) (hi : i ∈ s) (y : ↥(𝒰.X i)) (hy : y ∈ (↑(V i ⋯) : Set ↥(𝒰.X i)))
    (heq : Eq (α := ↥S) ((fun (a : ↥(𝒰.X i)) ↦ ((𝒰.f i) a : ↥S)) y : ↥S) (f x : ↥S)),
    Membership.mem (γ := Set ↥T)
      (⋃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀),
        ⋃ (h : i ∈ s),
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
                (⇑((PreZeroHypercover.pullback₁ f 𝒰).f x) : (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) → ↥T))
              i ''
            (↑((fun (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (hi : i ∈ s) ↦
                    (pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi :
                      TopologicalSpace.Opens
                        ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
                          i)))
                  i h) :
              Set ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)))
      x
⊢ Membership.mem (γ := Set ↥T)
    (⋃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀),
      ⋃ (h : i ∈ s),
        (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
              (⇑((PreZeroHypercover.pullback₁ f 𝒰).f x) : (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) → ↥T))
            i ''
          (↑((fun (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (hi : i ∈ s) ↦
                  (pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi :
                    TopologicalSpace.Opens
                      ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)))
                i h) :
            Set ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)))
    x

Tactic:
obtain ⟨i, hi, y, hy, heq⟩ := this
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq_1 :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ (↑(V i ⋯) : Set ↥(𝒰.X i))
heq : Eq (α := ↥S) ((fun (a : ↥(𝒰.X i)) ↦ ((𝒰.f i) a : ↥S)) y : ↥S) (f x : ↥S)
refine_2 :
  ∃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (i_1 : i ∈ s),
    Membership.mem (γ := Set ↥T)
      ((fun (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)) ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
        (↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯) :
          Set ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)))
      x
⊢ Membership.mem (γ := Set ↥T)
    (⋃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀),
      ⋃ (h : i ∈ s),
        (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
              (⇑((PreZeroHypercover.pullback₁ f 𝒰).f x) : (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) → ↥T))
            i ''
          (↑((fun (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (hi : i ∈ s) ↦
                  (pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi :
                    TopologicalSpace.Opens
                      ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)))
                i h) :
            Set ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)))
    x

Tactic:
simp_rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq_1 :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ (↑(V i ⋯) : Set ↥(𝒰.X i))
heq : Eq (α := ↥S) ((fun (a : ↥(𝒰.X i)) ↦ ((𝒰.f i) a : ↥S)) y : ↥S) (f x : ↥S)
refine_2 :
  ∀ (z : ↥(pullback f (𝒰.f i))) (hzl : (pullback.fst f (𝒰.f i)) z = x) (hzr : (pullback.snd f (𝒰.f i)) z = y),
    ∃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (i_1 : i ∈ s),
      Membership.mem (γ := Set ↥T)
        ((fun (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)) ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
          (↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯) :
            Set ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)))
        x
⊢ ∃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (i_1 : i ∈ s),
    Membership.mem (γ := Set ↥T)
      ((fun (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)) ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
        (↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯) :
          Set ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)))
      x

Tactic:
obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback x y heq.symm

Premises used: Eq.symm, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq_1 :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ (↑(V i ⋯) : Set ↥(𝒰.X i))
heq : Eq (α := ↥S) ((fun (a : ↥(𝒰.X i)) ↦ ((𝒰.f i) a : ↥S)) y : ↥S) (f x : ↥S)
z : ↥(pullback f (𝒰.f i))
hzl : (pullback.fst f (𝒰.f i)) z = x
hzr : (pullback.snd f (𝒰.f i)) z = y
⊢ z ∈
    (↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U') :
      Set ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i))

Tactic:
simpa [hzl]
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq_1 :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ (↑(V i ⋯) : Set ↥(𝒰.X i))
heq : Eq (α := ↥S) ((fun (a : ↥(𝒰.X i)) ↦ ((𝒰.f i) a : ↥S)) y : ↥S) (f x : ↥S)
z : ↥(pullback f (𝒰.f i))
hzl : (pullback.fst f (𝒰.f i)) z = x
hzr : (pullback.snd f (𝒰.f i)) z = y
⊢ z ∈
    (↑(pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯) :
      Set ((fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i))

Tactic:
simpa [hzr]
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq_1 :
  ⋃ (i : 𝒰.I₀),
      ⋃ (h : i ∈ s),
        (fun (x : 𝒰.I₀) ↦ (⇑(𝒰.f x) : (a : ↥(𝒰.X x)) → ↥S)) i '' (↑(V i h) : Set ((fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) i)) =
    (↑U : Set ↥S)
x : ↥T
hx : x ∈ (↑U' : Set ↥T)
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ (↑(V i ⋯) : Set ↥(𝒰.X i))
heq : Eq (α := ↥S) ((fun (a : ↥(𝒰.X i)) ↦ ((𝒰.f i) a : ↥S)) y : ↥S) (f x : ↥S)
z : ↥(pullback f (𝒰.f i))
hzl : (pullback.fst f (𝒰.f i)) z = x
hzr : (pullback.snd f (𝒰.f i)) z = y
⊢ ∃ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (i_1 : i ∈ s),
    Membership.mem (γ := Set ↥T)
      ((fun (a : ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)) ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
        (↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯) :
          Set ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)))
      x

Tactic:
exact ⟨i, hi, z, ⟨by simpa [hzl], by simpa [hzr]⟩, hzl⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
inst : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
⊢ QuasiCompactCover (PreZeroHypercover.pullback₂ f 𝒰)

Tactic:
.of_hom (PreZeroHypercover.pullbackIso f 𝒰).hom

Premises used: CategoryTheory.PreZeroHypercover.pullbackIso, AlgebraicGeometry.QuasiCompactCover.of_hom, CategoryTheory.Iso.hom
-- 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 : IsAffineOpen U
obtain :
  ∀ (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)),
    IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x))
      (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x)) (↑U : Set ↥X)
⊢ IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)

Tactic:
obtain ⟨s, hs, V, hcV, hU⟩ := hU.isCompactOpenCovered 𝒰

Premises used: AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered
-- 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)
⊢ ∀ (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))

Tactic:
have (i) (hi) : IsCompactOpenCovered ((f i).f ·) (V i hi) :=
      isCompactOpenCovered_of_isCompact (f i) (hcV i hi)
-- 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)
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))
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)
⊢ 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
-- 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))
⊢ Finite.{w + 1} (↑s : Type w)

Tactic:
have : Finite s := hs
-- 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 : Finite.{w + 1} (↑s : Type w)
⊢ ∀ (i : 𝒰.I₀) (hi : i ∈ s), Finite.{w + 1} (↑(t i hi) : Type w)

Tactic:
have (i) (hi) : Finite (t i hi) := ht i hi
-- 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)
⊢ IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)

Tactic:
.of_finite (κ := Σ (i : s), t i.1 i.2) (fun p ↦ ⟨p.1, p.2⟩) (fun p ↦ W _ p.1.2 _ p.2.2)
      (fun p ↦ hcW ..) ?_

Premises used: IsCompactOpenCovered.of_finite, Sigma.fst, Sigma.mk, Sigma.snd, Subtype.val, Subtype.property