-- Module: Mathlib.Topology.Covering.Basic
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₁ :
  Eq (α := (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
    ((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) :
      (↑((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) ⋯) ⋯ :
      { 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 })
⊢ (↑((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)

Tactic:
convert! hH ⟨⟨x, hUs x.2⟩, x.2⟩ using 4

Premises used: Subtype.mk, Subtype.val, Subtype.property