awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
𝒱 : PreZeroHypercover.{w', u, u + 1} S
f : 𝒱.Hom 𝒰
inst : QuasiCompactCover 𝒱
refine :
  ∀ {U : S.Opens} (hU : IsAffineOpen U),
    IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
⊢ QuasiCompactCover 𝒰

Tactic:
refine ⟨fun {U} hU ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
𝒱 : PreZeroHypercover.{w', u, u + 1} S
f : 𝒱.Hom 𝒰
inst : QuasiCompactCover 𝒱
U : S.Opens
hU : IsAffineOpen U
i : 𝒱.I₀
⊢ ∀ (x : ↥(𝒱.X i)),
    Eq (α := ↥S) ((fun (x : 𝒱.I₀) ↦ (⇑(𝒱.f x) : (a : ↥(𝒱.X x)) → ↥S)) i x)
      (Function.comp (β := ↥(𝒰.X (f.s₀ i))) (⇑(𝒰.f (f.s₀ i)))
        ((fun (x : 𝒱.I₀) ↦ (⇑(f.h₀ x) : (a : ↥(𝒱.X x)) → ↥(𝒰.X (f.s₀ x)))) i) x)

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
𝒱 : PreZeroHypercover.{w', u, u + 1} S
f : 𝒱.Hom 𝒰
inst : QuasiCompactCover 𝒱
U : S.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)

Tactic:
exact .of_comp (a := f.s₀) (𝒱.f ·) (f.h₀ ·)
    (fun _ ↦ Scheme.Hom.continuous _) (fun i ↦ funext <| by simp [← Scheme.Hom.comp_apply])
    (fun _ ↦ Scheme.Hom.continuous _) U.2 (hU.isCompactOpenCovered 𝒱)
-- 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:
⟨fun {U'} hU' ↦ ?_⟩

Premises used: AlgebraicGeometry.QuasiCompactCover.mk
-- 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
refine :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U'),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
⊢ QuasiCompactCover (PreZeroHypercover.pullback₁ f 𝒰)

Tactic:
refine ⟨fun {U'} hU' ↦ ?_⟩
-- 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'
inr :
  ∀
    (this :
      ∀ {U' : T.Opens} (hU' : IsAffineOpen U')
        (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
        IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
          ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T))
    (h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
wlog :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)

Tactic:
wlog h : ∃ (U : S.Opens), IsAffineOpen U ∧ f '' U' ⊆ U generalizing U'

Premises used: AlgebraicGeometry.Scheme.Opens
-- 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'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)

Tactic:
.of_isCompact_of_forall_exists_isCompactOpenCovered hU'.isCompact fun x hxU ↦ ?_

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, IsCompactOpenCovered.of_isCompact_of_forall_exists_isCompactOpenCovered
-- 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'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
inr :
  ∀ (x : ↥T) (hxU : x ∈ (↑U' : Set ↥T)),
    ∃ t ⊆ (↑U' : Set ↥T),
      x ∈ t ∧
        IsOpen t ∧
          IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
            ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
            (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)

Tactic:
refine .of_isCompact_of_forall_exists_isCompactOpenCovered hU'.isCompact fun x hxU ↦ ?_
-- 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'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
x : ↥T
hxU : x ∈ (↑U' : Set ↥T)
inr :
  ∀ (W : TopologicalSpace.Opens ↥S) (hW : W ∈ S.affineOpens) (hx : Membership.mem (α := ↥S) W (f x : ↥S)),
    W ≤ ⊤ →
      ∃ t ⊆ (↑U' : Set ↥T),
        x ∈ t ∧
          IsOpen t ∧
            IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
              ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
              (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t
⊢ ∃ t ⊆ (↑U' : Set ↥T),
    x ∈ t ∧
      IsOpen t ∧
        IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
          ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t

Tactic:
obtain ⟨W, hW, hx, _⟩ := isBasis_iff_nbhd.mp S.isBasis_affineOpens (mem_top (f x))

Premises used: TopologicalSpace.Opens.mem_top, TopologicalSpace.Opens.isBasis_iff_nbhd, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Iff.mp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe
-- 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'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
x : ↥T
hxU : x ∈ (↑U' : Set ↥T)
W : TopologicalSpace.Opens ↥S
hW : W ∈ S.affineOpens
hx : Membership.mem (α := ↥S) W (f x : ↥S)
right : W ≤ ⊤
inr :
  ∀ (W' : TopologicalSpace.Opens ↥T) (hW' : W' ∈ T.affineOpens) (hx' : x ∈ W') (hle : W' ≤ f ⁻¹ᵁ W ⊓ U'),
    ∃ t ⊆ (↑U' : Set ↥T),
      x ∈ t ∧
        IsOpen t ∧
          IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
            ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
            (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t
⊢ ∃ t ⊆ (↑U' : Set ↥T),
    x ∈ t ∧
      IsOpen t ∧
        IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
          ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t

Tactic:
obtain ⟨W', hW', hx', hle⟩ := isBasis_iff_nbhd.mp T.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ W ⊓ U' from ⟨hx, hxU⟩)

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd, And.intro, Iff.mp, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- 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'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
x : ↥T
hxU : x ∈ (↑U' : Set ↥T)
W : TopologicalSpace.Opens ↥S
hW : W ∈ S.affineOpens
hx : Membership.mem (α := ↥S) W (f x : ↥S)
right : W ≤ ⊤
W' : TopologicalSpace.Opens ↥T
hW' : W' ∈ T.affineOpens
hx' : x ∈ W'
hle : W' ≤ f ⁻¹ᵁ W ⊓ U'
⊢ x ∈ (↑W' : Set ↥T)

Tactic:
simpa [hx]
-- 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'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
x : ↥T
hxU : x ∈ (↑U' : Set ↥T)
W : TopologicalSpace.Opens ↥S
hW : W ∈ S.affineOpens
hx : Membership.mem (α := ↥S) W (f x : ↥S)
right : W ≤ ⊤
W' : TopologicalSpace.Opens ↥T
hW' : W' ∈ T.affineOpens
hx' : x ∈ W'
hle : W' ≤ f ⁻¹ᵁ W ⊓ U'
⊢ ⇑f '' (↑W' : Set ↥T) ⊆ (↑W : Set ↥S)

Tactic:
simpa using le_trans hle inf_le_left

Premises used: inf_le_left, le_trans
-- 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'
this :
  ∀ {U' : T.Opens} (hU' : IsAffineOpen U') (h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
h : ¬∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
x : ↥T
hxU : x ∈ (↑U' : Set ↥T)
W : TopologicalSpace.Opens ↥S
hW : W ∈ S.affineOpens
hx : Membership.mem (α := ↥S) W (f x : ↥S)
right : W ≤ ⊤
W' : TopologicalSpace.Opens ↥T
hW' : W' ∈ T.affineOpens
hx' : x ∈ W'
hle : W' ≤ f ⁻¹ᵁ W ⊓ U'
⊢ ∃ t ⊆ (↑U' : Set ↥T),
    x ∈ t ∧
      IsOpen t ∧
        IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
          ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
          (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t

Tactic:
exact ⟨W', le_trans hle inf_le_right, by simpa [hx], W'.2,
      this hW' ⟨W, hW, by simpa using le_trans hle inf_le_left⟩⟩
-- 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'
h : ∃ (U : S.Opens), IsAffineOpen U ∧ ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)
obtain :
  ∀ (U : S.Opens) (hU : IsAffineOpen U) (hsub : ⇑f '' (↑U' : Set ↥T) ⊆ (↑U : Set ↥S)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)

Tactic:
obtain ⟨U, hU, hsub⟩ := h
-- 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)
obtain :
  ∀ (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)),
    IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦
      ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
      (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)

Tactic:
obtain ⟨s, hf, V, hc, (heq : _ = (U : Set S))⟩ := hU.isCompactOpenCovered 𝒰

Premises used: SetLike.coe, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered
-- 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)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)

Tactic:
⟨s, hf, fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ (V i hi),
      fun i hi ↦ ?_, ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, IsCompactOpenCovered, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, CategoryTheory.Limits.pullback.fst, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj, Min.min
-- 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_1 :
  ∀ (i : (PreZeroHypercover.pullback₁ f 𝒰).I₀) (hi : i ∈ s),
    IsCompact.{u} (X := (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)
      (carrier
        ((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 hi))
refine_2 :
  ⋃ (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)
⊢ IsCompactOpenCovered (X := fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x))
    (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) (↑U' : Set ↥T)

Tactic:
refine ⟨s, hf, fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ (V i hi),
      fun i hi ↦ ?_, ?_⟩
-- 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)
i : (PreZeroHypercover.pullback₁ f 𝒰).I₀
hi : i ∈ s
⊢ U' ≤ f ⁻¹ᵁ U

Tactic:
simpa using hsub
-- 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)
i : (PreZeroHypercover.pullback₁ f 𝒰).I₀
hi : i ∈ s
⊢ V i hi ≤ 𝒰.f i ⁻¹ᵁ U

Tactic:
simpa [← SetLike.coe_subset_coe, ← heq, Set.range_comp] using Set.subset_iUnion_of_subset i
        (Set.subset_iUnion_of_subset hi (Set.subset_preimage_image _ _))

Premises used: Set.range_comp, Set.subset_iUnion_of_subset, SetLike.coe_subset_coe
-- 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)
i : (PreZeroHypercover.pullback₁ f 𝒰).I₀
hi : i ∈ s
⊢ IsCompact.{u} (X := (fun (x : (PreZeroHypercover.pullback₁ f 𝒰).I₀) ↦ ↥((PreZeroHypercover.pullback₁ f 𝒰).X x)) i)
    (carrier
      ((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 hi))

Tactic:
exact hU'.isCompact_pullback_inf (hc _ _) hU (by simpa using hsub) <| by
      simpa [← SetLike.coe_subset_coe, ← heq, Set.range_comp] using Set.subset_iUnion_of_subset i
        (Set.subset_iUnion_of_subset hi (Set.subset_preimage_image _ _))

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf
-- 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)
⊢ ⋃ (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:
simp