case a
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.414625
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 ∩ baseSet Z j
v : F
⊢ { fst := (b, v).fst, snd := ↑(coordChange Z i (indexAt Z (b, v).fst) (b, v).fst) (b, v).snd }.fst ∈
    baseSet Z i ∩
        baseSet Z
          (indexAt Z
            { fst := (b, v).fst, snd := ↑(coordChange Z i (indexAt Z (b, v).fst) (b, v).fst) (b, v).snd }.fst) ∩
      baseSet Z j

case hb
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.414625
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 ∩ baseSet Z j
v : F
⊢ b ∈ (localTriv Z i).baseSet ∩ (localTriv Z j).baseSet
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.414625
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 ∩ baseSet Z j
v : F
⊢ ↑(Trivialization.coordChangeL R (localTriv Z i) (localTriv Z j) b) v = ↑(coordChange Z i j b) v
rw [Trivialization.coordChangeL_apply', localTriv_symm_fst, localTriv_apply, coordChange_comp]
no goals
case a
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.414625
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 ∩ baseSet Z j
v : F
⊢ { fst := (b, v).fst, snd := ↑(coordChange Z i (indexAt Z (b, v).fst) (b, v).fst) (b, v).snd }.fst ∈
    baseSet Z i ∩
        baseSet Z
          (indexAt Z
            { fst := (b, v).fst, snd := ↑(coordChange Z i (indexAt Z (b, v).fst) (b, v).fst) (b, v).snd }.fst) ∩
      baseSet Z j

case hb
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.414625
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 ∩ baseSet Z j
v : F
⊢ b ∈ (localTriv Z i).baseSet ∩ (localTriv Z j).baseSet
exacts [⟨⟨hb.1, Z.mem_baseSet_at b⟩, hb.2⟩, hb]