-- Module: Mathlib.Topology.Sets.CompactOpenCovered
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U
Us : (i : (↑s : Type u_2)) → Set (Opens (X (↑i : ι)))
UsB : ∀ (i : (↑s : Type u_2)), Us i ⊆ B (↑i : ι)
hUsf : ∀ (i : (↑s : Type u_2)), (Us i).Finite
hUs : ∀ (i : (↑s : Type u_2)), V (↑i : ι) ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : (↑s : Type u_2)) × (↑(Us i) : Type u_3)
this_1 : Finite.{u_2 + 1} (↑s : Type u_2)
this : ∀ (i : (↑s : Type u_2)), Finite.{u_3 + 1} (↑(Us i) : Type u_3)
x : S
h_1 : ∃ (i : ι) (i_1 : i ∈ s), x ∈ f i '' (↑(V i i_1) : Set (X i))
i : ι
hi : i ∈ s
h : X i
heq : f i h = x
a : Opens (X i)
ha :
  Membership.mem (γ := Set (Opens (X i)))
      (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
        Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
      a ∧
    h ∈ a
w : σ
w₁ :
  X
    (↑(Sigma.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
          (Sigma.mk (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
            (Subtype.mk (p := fun (x : Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))) ↦
              Membership.mem (γ := Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
                (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) x)
              a ⋯))) :
      ι)
left :
  h ∈
    (↑(↑(Sigma.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
              (Sigma.mk (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
                (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
                (Subtype.mk (p := fun (x : Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))) ↦
                  Membership.mem (γ := Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
                    (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) x)
                  a ⋯))) :
          Opens (X (↑⟨⟨i, hi⟩, ⟨a, ⋯⟩⟩.fst : ι))) :
      Set (X (↑⟨⟨i, hi⟩, ⟨a, ⋯⟩⟩.fst : ι)))
right :
  (fun
          (a_1 :
            X
              (↑(Sigma.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
                    (Sigma.mk (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
                      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
                      (Subtype.mk (p := fun (x : Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))) ↦
                        Membership.mem (γ := Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
                          (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) x)
                        a ⋯))) :
                ι)) ↦
        f
          (↑(Sigma.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
                (Sigma.mk (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
                  (Subtype.mk (p := fun (x : Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))) ↦
                    Membership.mem (γ := Set (Opens (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))))
                      (Us (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) x)
                    a ⋯))) :
            ι)
          a_1)
      h =
    x
⊢ ∃ (i : σ),
    Membership.mem (γ := Set S)
      ((fun (a : X (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι)) ↦
          f (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : ι) a) ''
        (↑(↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(Us i) : Type u_3))) : Opens (X (↑i.fst : ι))) :
          Set (X (↑i.fst : ι))))
      x

Tactic:
use ⟨⟨i, hi⟩, ⟨a, ha.1⟩⟩, h, ha.2, heq

Premises used: And.right