-- 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
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
x_1 : (↑(s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_1)
a :
  (↑(↑(({
                    toFun :=
                      fun (e : (↑(s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_1)) ↦
                      (Subtype.mk (p := fun (x : (↑s : Type u_2)) ↦
                          Membership.mem (γ := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) x)
                          (Subtype.mk (p := fun (x : X) ↦ x ∈ s)
                            (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                                    (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑(↑e : (↑(f ⁻¹' s) : Type u_1)) : E)
                                      ⋯)).1 :
                              X)
                            ⋯)
                          ⋯,
                        ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑(↑e : (↑(f ⁻¹' s) : Type u_1)) : E) ⋯)).2),
                    invFun := fun (x : Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I) ↦
                      Subtype.mk (p := fun (x : (↑(f ⁻¹' s) : Type u_1)) ↦
                        x ∈ s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U)
                        (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' s)
                          (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                                (Subtype.mk (p := fun (x : X) ↦ x ∈ U) (↑(↑x.1 : (↑s : Type u_2)) : X) ⋯, x.2)) :
                            E)
                          ⋯)
                        ⋯,
                    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ } :
                  (a : (↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U) : Type u_1)) →
                    (↑(Subtype.val ⁻¹' U) : Type u_2) × I)
                x_1).1 :
          (↑s : Type u_2)) :
      X) =
    (↑(s.restrictPreimage f (↑x_1 : (↑(f ⁻¹' s) : Type u_1))) : X)
⊢ (↑(({
                toFun :=
                  fun (e : (↑(s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_1)) ↦
                  (Subtype.mk (p := fun (x : (↑s : Type u_2)) ↦
                      Membership.mem (γ := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) x)
                      (Subtype.mk (p := fun (x : X) ↦ x ∈ s)
                        (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                                (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑(↑e : (↑(f ⁻¹' s) : Type u_1)) : E)
                                  ⋯)).1 :
                          X)
                        ⋯)
                      ⋯,
                    ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                        (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑(↑e : (↑(f ⁻¹' s) : Type u_1)) : E) ⋯)).2),
                invFun := fun (x : Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I) ↦
                  Subtype.mk (p := fun (x : (↑(f ⁻¹' s) : Type u_1)) ↦
                    x ∈ s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U)
                    (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' s)
                      (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                            (Subtype.mk (p := fun (x : X) ↦ x ∈ U) (↑(↑x.1 : (↑s : Type u_2)) : X) ⋯, x.2)) :
                        E)
                      ⋯)
                    ⋯,
                left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ } :
              (a : (↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U) : Type u_1)) → (↑(Subtype.val ⁻¹' U) : Type u_2) × I)
            x_1).1 :
      (↑s : Type u_2)) =
    s.restrictPreimage f (↑x_1 : (↑(f ⁻¹' s) : Type u_1))

Tactic:
ext