-- Mathlib/Topology/VectorBundle/Basic.lean
theorem inCoordinates_eq {x₀ x : B} {y₀ y : B'} {ϕ : E x →SL[σ] E' y}
    (hx : x ∈ (trivializationAt F E x₀).baseSet) (hy : y ∈ (trivializationAt F' E' y₀).baseSet) :
    inCoordinates F E F' E' x₀ x y₀ y ϕ =
      ((trivializationAt F' E' y₀).continuousLinearEquivAt 𝕜₂ y hy : E' y →L[𝕜₂] F').comp
        (ϕ.comp <|
          (((trivializationAt F E x₀).continuousLinearEquivAt 𝕜₁ x hx).symm : F →L[𝕜₁] E x))

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁹ : (x : B) → AddCommMonoid (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : 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 F E)
F' : Type u_8
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst✝⁷ : (x : B') → AddCommMonoid (E' x)
inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)
inst✝⁵ : TopologicalSpace (TotalSpace F' E')
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜₁ F E
inst✝² : (x : B') → TopologicalSpace (E' x)
inst✝¹ : FiberBundle F' E'
inst✝ : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : E x →SL[σ] E' y
hx : x ∈ (trivializationAt F E x₀).baseSet
hy : y ∈ (trivializationAt F' E' y₀).baseSet
⊢ inCoordinates F E F' E' x₀ x y₀ y ϕ =
    (↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy)).comp
      (ϕ.comp ↑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm)

Tactic:
ext

Result:
case h
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁹ : (x : B) → AddCommMonoid (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : 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 F E)
F' : Type u_8
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst✝⁷ : (x : B') → AddCommMonoid (E' x)
inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)
inst✝⁵ : TopologicalSpace (TotalSpace F' E')
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜₁ F E
inst✝² : (x : B') → TopologicalSpace (E' x)
inst✝¹ : FiberBundle F' E'
inst✝ : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : E x →SL[σ] E' y
hx : x ∈ (trivializationAt F E x₀).baseSet
hy : y ∈ (trivializationAt F' E' y₀).baseSet
x✝ : F
⊢ (inCoordinates F E F' E' x₀ x y₀ y ϕ) x✝ =
    ((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy)).comp
        (ϕ.comp ↑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm))
      x✝

Proof state:
case h
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁹ : (x : B) → AddCommMonoid (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : 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 F E)
F' : Type u_8
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst✝⁷ : (x : B') → AddCommMonoid (E' x)
inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)
inst✝⁵ : TopologicalSpace (TotalSpace F' E')
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜₁ F E
inst✝² : (x : B') → TopologicalSpace (E' x)
inst✝¹ : FiberBundle F' E'
inst✝ : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : E x →SL[σ] E' y
hx : x ∈ (trivializationAt F E x₀).baseSet
hy : y ∈ (trivializationAt F' E' y₀).baseSet
x✝ : F
⊢ (inCoordinates F E F' E' x₀ x y₀ y ϕ) x✝ =
    ((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy)).comp
        (ϕ.comp ↑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm))
      x✝

Tactic:
simp_rw [inCoordinates, ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe,
  Trivialization.coe_continuousLinearEquivAt_eq, Trivialization.symm_continuousLinearEquivAt_eq]

Result:
no goals