no goals
ι : Type ?u.6519
B : Type u_1
F : Type u_2
E : B → Type ?u.6530
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
x : B × F
⊢ x ∈ e.target ↔ x.fst ∈ e.baseSet
rw [e.target_eq, prod_univ, mem_preimage]