no goals
ι : Type ?u.55034
B : Type u_1
F : Type u_2
E : B → Type ?u.55045
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e : Trivialization F proj
b : B
h : b ∈ e.baseSet
x : F
⊢ coordChange e e b x = x
rw [coordChange, e.apply_symm_apply' h]