no goals
ι : Type ?u.15747
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.15761
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
⊢ totalSpaceMk b (Pretrivialization.symm e b y) = ↑(LocalEquiv.symm e.toLocalEquiv) (b, y)
rw [e.symm_apply hb, TotalSpace.mk_cast (e.proj_symm_apply' hb), TotalSpace.eta]