no goals
ι : Type ?u.38955
B : Type ?u.38958
F : Type ?u.38961
E : B → Type ?u.38966
Z : Type ?u.38969
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
b : B
hb : b ∈ e.baseSet
p : F
⊢ ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, p) ∈ proj ⁻¹' {b}
rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]