-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
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 : ι)))
⊢ ∃ (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
have 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 sorry))) :
              ι)) ↦
      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 sorry))) :
          ι)
        a_1)
    h =
  x
Tactic: use ⟨⟨i, hi⟩, ⟨a, ha.1⟩⟩, h, ha.2, heq