no goals
E : Type u_2
X : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
x : E
I : Type u_1
inst✝ : TopologicalSpace I
h✝ : IsEvenlyCovered f (f x) I
e : Trivialization I f := Classical.choose (_ : ∃ t, f x ∈ t.baseSet)
h : f x ∈ (Classical.choose (_ : ∃ t, f x ∈ t.baseSet)).baseSet := Classical.choose_spec h✝.right
he : (f x, (↑e x).snd) = ↑e x := Trivialization.mk_proj_snd' e h
⊢ (f x, (↑e x).snd) ∈ e.target
rwa [he, e.mem_target, e.coe_fst (e.mem_source.mpr h)]