case h
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.445706
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i j : ι
b : B
hb : b ∈ baseSet Z i
v : F
⊢ ↑(Trivialization.symmL R (localTriv Z i) b) v = ↑(coordChange Z i (indexAt Z b) b) v
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.445706
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i j : ι
b : B
hb : b ∈ baseSet Z i
⊢ Trivialization.symmL R (localTriv Z i) b = coordChange Z i (indexAt Z b) b
ext1 v
case h
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.445706
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i j : ι
b : B
hb : b ∈ baseSet Z i
v : F
⊢ cast (_ : Fiber Z (↑(LocalHomeomorph.symm (localTriv Z i).toLocalHomeomorph) (b, v)).fst = Fiber Z b)
      (↑(LocalHomeomorph.symm (localTriv Z i).toLocalHomeomorph) (b, v)).snd =
    ↑(coordChange Z i (indexAt Z b) b) v

case h.hb
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.445706
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i j : ι
b : B
hb : b ∈ baseSet Z i
v : F
⊢ b ∈ (localTriv Z i).baseSet
case h
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.445706
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i j : ι
b : B
hb : b ∈ baseSet Z i
v : F
⊢ ↑(Trivialization.symmL R (localTriv Z i) b) v = ↑(coordChange Z i (indexAt Z b) b) v
rw [(Z.localTriv i).symmL_apply R, (Z.localTriv i).symm_apply]
no goals
case h
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.445706
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i j : ι
b : B
hb : b ∈ baseSet Z i
v : F
⊢ cast (_ : Fiber Z (↑(LocalHomeomorph.symm (localTriv Z i).toLocalHomeomorph) (b, v)).fst = Fiber Z b)
      (↑(LocalHomeomorph.symm (localTriv Z i).toLocalHomeomorph) (b, v)).snd =
    ↑(coordChange Z i (indexAt Z b) b) v

case h.hb
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.445706
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i j : ι
b : B
hb : b ∈ baseSet Z i
v : F
⊢ b ∈ (localTriv Z i).baseSet
exacts [rfl, hb]