case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type ?u.44757
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
p : TotalSpace Z
⊢ p.fst ∈ baseSet Z (indexAt Z p.fst)
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type ?u.44757
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
p : TotalSpace Z
⊢ ↑(localTrivAt Z p.fst) p = (p.fst, p.snd)
rw [localTrivAt, localTriv_apply, coordChange_self]
no goals
case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type ?u.44757
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
p : TotalSpace Z
⊢ p.fst ∈ baseSet Z (indexAt Z p.fst)
exact Z.mem_baseSet_at p.1