no goals
R : Type ?u.536498
B : Type u_4
F : Type u_5
E : B → Type ?u.536509
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✝¹⁶ : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_3
𝕜₂ : Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜₁
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst✝¹³ : TopologicalSpace B'
inst✝¹² : NormedSpace 𝕜₁ F
inst✝¹¹ : (x : B) → Module 𝕜₁ (E x)
inst✝¹⁰ : TopologicalSpace (TotalSpace E)
F' : Type u_8
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂ F'
E' : B' → Type ?u.537479
inst✝⁷ : (x : B') → AddCommMonoid (E' x)
inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)
inst✝⁵ : TopologicalSpace (TotalSpace E')
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜₁ F E
inst✝² : (x : B') → TopologicalSpace (E' x)
inst✝¹ : FiberBundle F' E'
inst✝ : VectorBundle 𝕜₂ F' E'
ι : Type u_1
ι' : Type u_2
Z : VectorBundleCore 𝕜₁ B F ι
Z' : VectorBundleCore 𝕜₂ B' F' ι'
x₀ x : B
y₀ y : B'
ϕ : F →SL[σ] F'
hx : x ∈ VectorBundleCore.baseSet Z (VectorBundleCore.indexAt Z x₀)
hy : y ∈ VectorBundleCore.baseSet Z' (VectorBundleCore.indexAt Z' y₀)
⊢ inCoordinates F (VectorBundleCore.Fiber Z) F' (VectorBundleCore.Fiber Z') x₀ x y₀ y ϕ =
    comp (VectorBundleCore.coordChange Z' (VectorBundleCore.indexAt Z' y) (VectorBundleCore.indexAt Z' y₀) y)
      (comp ϕ (VectorBundleCore.coordChange Z (VectorBundleCore.indexAt Z x₀) (VectorBundleCore.indexAt Z x) x))
simp_rw [inCoordinates, Z'.trivializationAt_continuousLinearMapAt hy,
  Z.trivializationAt_symmL hx]