no goals
ι : Type ?u.54393
B : Type u_1
F : Type u_2
E : B → Type ?u.54404
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₁ e₂ : Trivialization F proj
p : Z
h : proj p ∈ e₁.baseSet
⊢ coordChange e₁ e₂ (proj p) (↑e₁ p).snd = (↑e₂ p).snd
rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]