case h.h
𝕜 : Type u_2
B : Type u_3
F : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b) v = ↑(ContinuousLinearEquiv.refl 𝕜 F) v
𝕜 : Type u_2
B : Type u_3
F : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
⊢ Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F
ext v
case h.h
𝕜 : Type u_2
B : Type u_3
F : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (↑(trivialization B F) (↑(LocalHomeomorph.symm (trivialization B F).toLocalHomeomorph) (b, v))).snd =
    ↑(ContinuousLinearEquiv.refl 𝕜 F) v

case h.h.hb
𝕜 : Type u_2
B : Type u_3
F : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ b ∈ (trivialization B F).baseSet ∩ (trivialization B F).baseSet
case h.h
𝕜 : Type u_2
B : Type u_3
F : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b) v = ↑(ContinuousLinearEquiv.refl 𝕜 F) v
rw [Trivialization.coordChangeL_apply']
no goals
case h.h
𝕜 : Type u_2
B : Type u_3
F : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (↑(trivialization B F) (↑(LocalHomeomorph.symm (trivialization B F).toLocalHomeomorph) (b, v))).snd =
    ↑(ContinuousLinearEquiv.refl 𝕜 F) v

case h.h.hb
𝕜 : Type u_2
B : Type u_3
F : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ b ∈ (trivialization B F).baseSet ∩ (trivialization B F).baseSet
exacts [rfl, ⟨mem_univ _, mem_univ _⟩]