no goals
ι : Type ?u.16241
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.16255
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
z : TotalSpace E
hz : TotalSpace.proj z ∈ e.baseSet
⊢ Pretrivialization.symm e (TotalSpace.proj z) (↑e z).snd = z.snd
rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr hz)]