no goals
ι : Type ?u.10841
B : Type u_1
F : Type u_2
E : B → Type ?u.10852
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e f : Pretrivialization F proj
⊢ f.target ∩ ↑(LocalEquiv.symm f.toLocalEquiv) ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ
rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]