ι : Type ?u.6755
B : Type u_1
F : Type u_2
E : B → Type ?u.6766
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
this : proj (↑(LocalEquiv.symm e.toLocalEquiv) x) = (↑e (↑(LocalEquiv.symm e.toLocalEquiv) x)).fst
⊢ proj (↑(LocalEquiv.symm e.toLocalEquiv) x) = x.fst
ι : Type ?u.6755
B : Type u_1
F : Type u_2
E : B → Type ?u.6766
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
⊢ proj (↑(LocalEquiv.symm e.toLocalEquiv) x) = x.fst
have := (e.coe_fst (e.map_target hx)).symm
no goals
ι : Type ?u.6755
B : Type u_1
F : Type u_2
E : B → Type ?u.6766
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
this : proj (↑(LocalEquiv.symm e.toLocalEquiv) x) = (↑e (↑(LocalEquiv.symm e.toLocalEquiv) x)).fst
⊢ proj (↑(LocalEquiv.symm e.toLocalEquiv) x) = x.fst
rwa [← e.coe_coe, e.right_inv hx] at this