-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x_1 : X
hx : x_1 ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x_1 I
inst : DiscreteTopology I
U : Set X
hxU : x_1 ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
hUs : U ⊆ s
this :
  Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) =
    f ⁻¹' U
x : (↑(f ⁻¹' U) : Type u_1)
⊢ (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            ((Homeomorph.symm (IsEmbedding.homeomorphImage ⋯ ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)) :
                (a : (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) →
                  (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
              ((Homeomorph.symm
                    (Homeomorph.setCongr (s :=
                      Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
                        ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
                      (t := f ⁻¹' U) this) :
                  (a : (↑(f ⁻¹' U) : Type u_1)) →
                    (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
                x))).1 :
      X) =
    f (↑x : E)
have h₁ : Eq (α := (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
  ((Homeomorph.symm (IsEmbedding.homeomorphImage sorry ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)) :
        (a : (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) →
          (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
      ((Homeomorph.symm
            (Homeomorph.setCongr (s :=
              Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
                ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
              (t := f ⁻¹' U) this) :
          (a : (↑(f ⁻¹' U) : Type u_1)) →
            (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
        x) :
    (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
  (Subtype.mk (p := fun (x : (↑(f ⁻¹' s) : Type u_1)) ↦
      Membership.mem (γ := Set (↑(f ⁻¹' s) : Type u_1)) ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) x)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' s) (↑x : E) sorry) sorry :
    { x : (↑(f ⁻¹' s) : Type u_1) //
      Membership.mem (γ := Set (↑(f ⁻¹' s) : Type u_1)) ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) x })
Tactic: convert! hH ⟨⟨x, hUs x.2⟩, x.2⟩ using 4