no goals
ι : Type ?u.23235
B : Type u_2
F : Type u_3
E : B → Type ?u.23246
Z : Type u_1
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet
rw [e.source_eq, mem_preimage]