awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x_1 : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x_1 ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (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_2 : (↑(SProd.sprod (β := Set I) U Set.univ) : Type (max u_2 u_3))
x : X
i : I
hx : (x, i).1 ∈ U
right : Membership.mem (γ := Set I) Set.univ (x, i).2
⊢ Eq.{u_1 + 1} (α := E)
    (Function.comp (β := Prod.{u_2, u_3} (↑U : Type u_2) I)
        (Function.comp (β := { x : E // x ∈ f ⁻¹' U }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' U))
          (⇑H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1)))
        (fun (ui : (↑(SProd.sprod (β := Set I) U Set.univ) : Type (max u_2 u_3))) ↦
          (Subtype.mk (p := fun (x : X) ↦ x ∈ U) (↑ui : X × I).1 ⋯, (↑ui : X × I).2))
        (Subtype.mk (p := fun (x : X × I) ↦ x ∈ SProd.sprod (β := Set I) U Set.univ) (x, i) ⋯) :
      E)
    ((SProd.sprod (β := Set I) U Set.univ).restrict («π» := fun (a : X × I) ↦ E)
        (fun (xi : X × I) ↦
          (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                (if hx : xi.1 ∈ U then Subtype.mk (p := fun (x : X) ↦ x ∈ U) xi.1 hx
                  else Subtype.mk (p := fun (x : X) ↦ x ∈ U) x_1 hxU,
                  xi.2)) :
            E))
        (Subtype.mk (p := fun (x : X × I) ↦ x ∈ SProd.sprod (β := Set I) U Set.univ) (x, i) ⋯) :
      E)

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (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)
e : E
he : f e ∈ U
⊢ ((↑{
              toFun := fun (e : E) ↦
                if he : f e ∈ U then
                  ((↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).1 :
                      X),
                    ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                        (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).2)
                else (x, Classical.arbitrary I),
              invFun := fun (xi : X × I) ↦
                (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                      (if hx : xi.1 ∈ U then Subtype.mk (p := fun (x : X) ↦ x ∈ U) xi.1 hx
                        else Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU,
                        xi.2)) :
                  E),
              source := f ⁻¹' U, target := SProd.sprod (β := Set I) U Set.univ, map_source' := ⋯, map_target' := ⋯,
              left_inv' := ⋯, right_inv' := ⋯, open_source := hfU, open_target := ⋯, continuousOn_toFun := ⋯,
              continuousOn_invFun := ⋯ : OpenPartialHomeomorph E (X × I) } :
          E → X × I)
        e).1 =
    f e

Tactic:
simp [he, hH]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (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)
⊢ Trivialization I f

Tactic:
exact
  { toFun e := if he : f e ∈ U then ⟨(H ⟨e, he⟩).1, (H ⟨e, he⟩).2⟩ else ⟨x, Classical.arbitrary I⟩
    invFun xi := H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)
    source := f ⁻¹' U
    target := U ×ˢ Set.univ
    map_source' e (he : f e ∈ U) := by simp [he]
    map_target' _ _ := Subtype.coe_prop _
    left_inv' e (he : f e ∈ U) := by simp [he]
    right_inv' xi := by rintro ⟨hx, -⟩; simpa [hx] using fun h ↦ (h (H.symm _).2).elim
    open_source := hfU
    open_target := hU.prod isOpen_univ
    continuousOn_toFun := continuousOn_iff_continuous_restrict.mpr <|
      ((continuous_subtype_val.prodMap continuous_id).comp H.continuous).congr
      fun ⟨e, (he : f e ∈ U)⟩ ↦ by simp [Prod.map, he]
    continuousOn_invFun := continuousOn_iff_continuous_restrict.mpr <|
      ((continuous_subtype_val.comp H.symm.continuous).comp (by fun_prop :
        Continuous fun ui ↦ ⟨⟨_, ui.2.1⟩, ui.1.2⟩)).congr fun ⟨⟨x, i⟩, ⟨hx, _⟩⟩ ↦ by simp [hx]
    baseSet := U
    open_baseSet := hU
    source_eq := rfl
    target_eq := rfl
    proj_toFun e (he : f e ∈ U) := by simp [he, hH] }
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (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)
⊢ Trivialization I f

Tactic:
classical exact
  { toFun e := if he : f e ∈ U then ⟨(H ⟨e, he⟩).1, (H ⟨e, he⟩).2⟩ else ⟨x, Classical.arbitrary I⟩
    invFun xi := H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)
    source := f ⁻¹' U
    target := U ×ˢ Set.univ
    map_source' e (he : f e ∈ U) := by simp [he]
    map_target' _ _ := Subtype.coe_prop _
    left_inv' e (he : f e ∈ U) := by simp [he]
    right_inv' xi := by rintro ⟨hx, -⟩; simpa [hx] using fun h ↦ (h (H.symm _).2).elim
    open_source := hfU
    open_target := hU.prod isOpen_univ
    continuousOn_toFun := continuousOn_iff_continuous_restrict.mpr <|
      ((continuous_subtype_val.prodMap continuous_id).comp H.continuous).congr
      fun ⟨e, (he : f e ∈ U)⟩ ↦ by simp [Prod.map, he]
    continuousOn_invFun := continuousOn_iff_continuous_restrict.mpr <|
      ((continuous_subtype_val.comp H.symm.continuous).comp (by fun_prop :
        Continuous fun ui ↦ ⟨⟨_, ui.2.1⟩, ui.1.2⟩)).congr fun ⟨⟨x, i⟩, ⟨hx, _⟩⟩ ↦ by simp [hx]
    baseSet := U
    open_baseSet := hU
    source_eq := rfl
    target_eq := rfl
    proj_toFun e (he : f e ∈ U) := by simp [he, hH] }
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : IsEvenlyCovered f x I
⊢ x ∈ h.toTrivialization.baseSet

Tactic:
h.2.choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, And.right, And.left, Classical.choose
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
x : E
inst_3 : Nonempty I
h : IsEvenlyCovered f (f x) I
⊢ Eq.{u_3 + 1} (α := I)
    ((h.fiberHomeomorph.symm : (a : (↑(f ⁻¹' {f x}) : Type u_1)) → I)
        ((↑h.toTrivialization : E → X × (↑(f ⁻¹' {f x}) : Type u_1)) x).2 :
      I)
    ((h.fiberHomeomorph.symm : (a : (↑(f ⁻¹' {f x}) : Type u_1)) → I)
        (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ f ⁻¹' {f x}) x ⋯) :
      I)

Tactic:
simp [toTrivialization, toTrivialization', dif_pos h.2.choose_spec.1, fiberHomeomorph]

Premises used: Exists.choose_spec, dif_pos, IsEvenlyCovered.fiberHomeomorph, IsEvenlyCovered.toTrivialization', And.right, And.left, IsEvenlyCovered.toTrivialization
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
x : E
h : IsEvenlyCovered f (f x) I
⊢ ContinuousAt f x

Tactic:
have ⟨_, _, hxU, _, _, H, _⟩ := h
  have : Nonempty I := ⟨(H ⟨x, hxU⟩).2⟩
  let e := h.toTrivialization
  e.continuousAt_proj (e.mem_source.mpr (mem_toTrivialization_baseSet h))

Premises used: Iff.mpr, ContinuousAt, Nonempty.intro, Subtype.mk, Bundle.Trivialization.mem_source, Bundle.Trivialization.continuousAt_proj, IsEvenlyCovered.toTrivialization, IsEvenlyCovered.mem_toTrivialization_baseSet, _private.0.IsEvenlyCovered.continuousAt.match_1, Prod.snd, DFunLike.coe
-- 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
I : Type u_3
inst_3 : TopologicalSpace I
J : Type u_4
inst_4 : TopologicalSpace J
g : I ≃ₜ J
x : X
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 : (↑(f ⁻¹' U) : Type u_1)
⊢ (↑((H.trans (Homeomorph.prodCongr (Homeomorph.refl (↑U : Type u_2)) g) :
              (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × J)
            x_1).1 :
      X) =
    f (↑x_1 : E)

Tactic:
simp [hH]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
h.of_fiber_homeomorph h.fiberHomeomorph

Premises used: IsEvenlyCovered.of_fiber_homeomorph, IsEvenlyCovered.fiberHomeomorph
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : Prod.{u_2, u_3} (↑t.baseSet : Type u_2) I
rw : t.invFun ((↑xi.1 : X), xi.2) ∈ t.source
⊢ t.invFun ((↑xi.1 : X), xi.2) ∈ f ⁻¹' t.baseSet

Tactic:
rw [Set.mem_preimage, ← t.mem_source]

Premises used: Bundle.Trivialization.mem_source, Set.mem_preimage
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : Prod.{u_2, u_3} (↑t.baseSet : Type u_2) I
⊢ t.invFun ((↑xi.1 : X), xi.2) ∈ t.source

Tactic:
t.map_target (t.target_eq ▸ ⟨xi.1.2, ⟨⟩⟩)

Premises used: Set.Mem, Eq.rec, OpenPartialHomeomorph.toFun', Bundle.Trivialization.target_eq, Prod.fst, And.intro, Bundle.Trivialization.map_target, Eq.symm, Subtype.property, True.intro
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : Prod.{u_2, u_3} (↑t.baseSet : Type u_2) I
⊢ t.invFun ((↑xi.1 : X), xi.2) ∈ t.source

Tactic:
exact t.map_target (t.target_eq ▸ ⟨xi.1.2, ⟨⟩⟩)

Premises used: Bundle.Trivialization.map_target
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : Prod.{u_2, u_3} (↑t.baseSet : Type u_2) I
⊢ (fun (e : (↑(f ⁻¹' t.baseSet) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : X) ↦ x ∈ t.baseSet) (f (↑e : E)) ⋯, ((↑t : E → X × I) (↑e : E)).2))
      ((fun (xi : Prod.{u_2, u_3} (↑t.baseSet : Type u_2) I) ↦
          (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' t.baseSet) (t.invFun ((↑xi.1 : X), xi.2)) ⋯ :
            { x : E // x ∈ f ⁻¹' t.baseSet }))
        xi) =
    xi

Tactic:
simp [t.proj_symm_apply', t.apply_symm_apply']

Premises used: Bundle.Trivialization.apply_symm_apply', Bundle.Trivialization.proj_symm_apply'
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
e : (↑(f ⁻¹' t.baseSet) : Type u_1)
⊢ (f ⁻¹' t.baseSet).restrict («π» := fun (a : E) ↦ X × I) (↑t.toPartialEquiv : E → X × I) e =
    Function.comp (β := Prod.{u_2, u_3} { x : X // x ∈ t.baseSet } I)
      (Prod.map (Subtype.val (p := fun (x : X) ↦ x ∈ t.baseSet)) id)
      (fun (e : (↑(f ⁻¹' t.baseSet) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : X) ↦ x ∈ t.baseSet) (f (↑e : E)) ⋯, ((↑t : E → X × I) (↑e : E)).2))
      e

Tactic:
simp [t.mk_proj_snd' e.2]

Premises used: Bundle.Trivialization.mk_proj_snd', Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
x_1 : (↑(f ⁻¹' t.baseSet) : Type u_1)
⊢ (↑(({
                toFun := fun (e : (↑(f ⁻¹' t.baseSet) : Type u_1)) ↦
                  (Subtype.mk (p := fun (x : X) ↦ x ∈ t.baseSet) (f (↑e : E)) ⋯, ((↑t : E → X × I) (↑e : E)).2),
                invFun := fun (xi : Prod.{u_2, u_3} (↑t.baseSet : Type u_2) I) ↦
                  Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' t.baseSet) (t.invFun ((↑xi.1 : X), xi.2)) ⋯,
                left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ } :
              (a : (↑(f ⁻¹' t.baseSet) : Type u_1)) → (↑t.baseSet : Type u_2) × I)
            x_1).1 :
      X) =
    f (↑x_1 : E)

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : IsEmpty I
x : X
U : Set X
hUx : U ∈ 𝓝 x
hfU : f ⁻¹' U = ∅
⊢ IsEvenlyCovered f x I

Tactic:
have ⟨V, hVU, hV, hxV⟩ := mem_nhds_iff.mp hUx
  have hfV : f ⁻¹' V = ∅ := Set.eq_empty_of_subset_empty ((Set.preimage_mono hVU).trans hfU.le)
  have := Set.isEmpty_coe_sort.mpr hfV
  ⟨inferInstance, _, hxV, hV, hfV ▸ isOpen_empty, .empty, isEmptyElim⟩

Premises used: Iff.mpr, Homeomorph.empty, mem_nhds_iff, isEmptyElim, Eq.rec, inferInstance, HasSubset.Subset.trans, Eq.le, Set.isEmpty_coe_sort, IsEvenlyCovered, Set.eq_empty_of_subset_empty, Set.preimage_mono, _private.0.IsEvenlyCovered.of_preimage_eq_empty.match_1, And.intro, Exists.intro, Iff.mp, Eq.symm, isOpen_empty
-- 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)
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
fun_prop
-- 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)
e : (↑(s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_1)
⊢ Membership.mem (γ := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U)
    (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)
      ⋯)

Tactic:
simpa only [hH] using e.2

Premises used: Subtype.property
-- 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_1 : X
hxs : x_1 ∈ s
h : IsEvenlyCovered f x_1 I
inst : DiscreteTopology I
U : Set X
hxU : x_1 ∈ 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 : Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I
⊢ (↑((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) ∈
    f ⁻¹' s

Tactic:
simp [← hH]
-- 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_1 : X
hxs : x_1 ∈ s
h : IsEvenlyCovered f x_1 I
inst : DiscreteTopology I
U : Set X
hxU : x_1 ∈ 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 : Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I
⊢ 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)
      ⋯ ∈
    s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U

Tactic:
simp [← hH]
-- 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)
⊢ (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)
            ⋯)
          ⋯)
      ((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) :
            Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I))
        x_1) =
    x_1

Tactic:
simp
-- 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 : Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I
⊢ (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) :
          Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I))
      ((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)
              ⋯)
            ⋯)
        x_1) =
    x_1

Tactic:
simp