-- 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)
refine :
  ⋃ (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)
⊢ IsCompactOpenCovered (X := fun (x : (𝒰.bind f).I₀) ↦ ↥((𝒰.bind f).X x)) (fun (x : (𝒰.bind f).I₀) ↦ ⇑((𝒰.bind f).f x))
    (↑U : Set ↥X)

Tactic:
refine .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 ..) ?_