-- 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
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)
⊢ (↑(({
                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))
have 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)
                                    sorry)).1 :
                            X)
                          sorry)
                        sorry,
                      ((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) sorry)).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) sorry, x.2)) :
                          E)
                        sorry)
                      sorry,
                  left_inv := sorry, right_inv := sorry, continuous_toFun := sorry, continuous_invFun := sorry } :
                (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)
Tactic: ext