-- 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)
⊢ 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 })
have h₁ : Eq (α :=
  (↑(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)) :
    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 :
    (↑(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)) :
      Type u_1))
  ((IsEmbedding.homeomorphImage sorry ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) :
        (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) →
          (↑(Subtype.val '' (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) :
    (↑(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)) :
      Type u_1))
Tactic: rw [Homeomorph.symm_apply_eq]