no goals
ι : Type ?u.11860
B : Type u_1
F : Type u_2
E : B → Type ?u.11871
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.trans (LocalEquiv.symm e.toLocalEquiv) e'.toLocalEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ
rw [LocalEquiv.trans_source, e'.source_eq, LocalEquiv.symm_source, e.target_eq, inter_comm,
  e.preimage_symm_proj_inter, inter_comm]