awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
⊢ ∃ 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
have 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
Tactic: obtain ⟨W, hW, hx, _⟩ := isBasis_iff_nbhd.mp S.isBasis_affineOpens (mem_top (f x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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 ≤ ⊤
⊢ ∃ 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
have 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
Tactic: obtain ⟨W', hW', hx', hle⟩ := isBasis_iff_nbhd.mp T.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ W ⊓ U' from ⟨hx, hxU⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨U, hU, hsub⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨s, hf, V, hc, (heq : _ = (U : Set S))⟩ := hU.isCompactOpenCovered 𝒰
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
have 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))
Tactic: refine ⟨s, hf, fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ (V i hi),
      fun i hi ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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))
⊢ 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)
have 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)
Tactic: refine ⟨s, hf, fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ (V i hi),
      fun i hi ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
have 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
Tactic: refine subset_antisymm (by simp) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (hypothesis)
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 (γ := 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
have this : Membership.mem (α := ↥S) (↑U : Set ↥S) (f x : ↥S)
Tactic: have : f x ∈ (U : Set S) := hsub ⟨x, hx, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (hypothesis)
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)
⊢ 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
have this₁ : ∃ (i : 𝒰.I₀) (i_1 : i ∈ s),
  Membership.mem (α := ↥S) (γ := Set ↥S) ((fun (a : ↥(𝒰.X i)) ↦ (𝒰.f i) a) '' (↑(V i sorry) : Set ↥(𝒰.X i))) (f x : ↥S)
Tactic: simp_rw [← heq, Set.mem_iUnion] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
⊢ 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
have refine_2 : ∀ (i : 𝒰.I₀) (hi : i ∈ s) (y : ↥(𝒰.X i)) (hy : y ∈ (↑(V i sorry) : 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
Tactic: obtain ⟨i, hi, y, hy, heq⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
⊢ 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
have 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 sorry) :
        Set ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)))
    x
Tactic: simp_rw [Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.QuasiCompact (goal)
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)
⊢ ∃ (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
have 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 sorry) :
          Set ↥((PreZeroHypercover.pullback₁ f 𝒰).X i)))
      x
Tactic: obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback x y heq.symm
-- 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 : IsAffineOpen U
⊢ IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)
have 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)
Tactic: obtain ⟨s, hs, V, hcV, hU⟩ := hU.isCompactOpenCovered 𝒰
-- 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)
⊢ 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),
  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)