ι : Type ?u.9079
B : Type u_1
F : Type u_2
E : B → Type ?u.9090
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
x : B × F
hx : x ∈ e.target
⊢ x ∈ ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' e.baseSet)
ι : Type ?u.9079
B : Type u_1
F : Type u_2
E : B → Type ?u.9090
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
⊢ ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target
refine' inter_eq_right_iff_subset.mpr fun x hx => _
ι : Type ?u.9079
B : Type u_1
F : Type u_2
E : B → Type ?u.9090
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
x : B × F
hx : x ∈ e.target
⊢ x.fst ∈ e.baseSet
ι : Type ?u.9079
B : Type u_1
F : Type u_2
E : B → Type ?u.9090
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
x : B × F
hx : x ∈ e.target
⊢ x ∈ ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' e.baseSet)
simp only [mem_preimage, LocalEquiv.invFun_as_coe, e.proj_symm_apply hx]
no goals
ι : Type ?u.9079
B : Type u_1
F : Type u_2
E : B → Type ?u.9090
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
x : B × F
hx : x ∈ e.target
⊢ x.fst ∈ e.baseSet
exact e.mem_target.mp hx