no goals
ι : Type ?u.8645
B : Type u_2
F : Type u_3
E : B → Type ?u.8656
Z : Type u_1
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ x : Z
ex : x ∈ e.source
⊢ ↑(LocalEquiv.symm e.toLocalEquiv) (proj x, (↑e x).snd) = x
rw [← e.coe_fst ex, Prod.mk.eta, ← e.coe_coe, e.left_inv ex]