no goals
ι : Type ?u.17161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.17175
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝ : (x : B) → Zero (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∈ e.baseSet
y : F
⊢ ↑e (totalSpaceMk b (Pretrivialization.symm e b y)) = (b, y)
rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]