no goals
ι : Type ?u.11622
B : Type u_1
F : Type u_2
E : B → Type ?u.11633
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e e' : Pretrivialization F proj
⊢ LocalEquiv.symm (LocalEquiv.trans (LocalEquiv.symm e.toLocalEquiv) e'.toLocalEquiv) =
    LocalEquiv.trans (LocalEquiv.symm e'.toLocalEquiv) e.toLocalEquiv
rw [LocalEquiv.trans_symm_eq_symm_trans_symm, LocalEquiv.symm_symm]