Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
inst✝²⁷ : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_16
inst✝¹⁴ : (x : B) → AddCommGroup (E₃ x)
inst✝¹³ : (x : B) → Module 𝕜 (E₃ x)
inst✝¹² : NormedAddCommGroup F₃
inst✝¹¹ : NormedSpace 𝕜 F₃
inst✝¹⁰ : TopologicalSpace (TotalSpace F₃ E₃)
inst✝⁹ : (x : B) → TopologicalSpace (E₃ x)
inst✝⁸ : TopologicalSpace B
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜 F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : FiberBundle F₃ E₃
inst✝² : VectorBundle 𝕜 F₃ E₃
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₃ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)
x₀ x : B
ϕ : E₁ x →L[𝕜] E₂ x →L[𝕜] E₃ x
v : F₁
w : F₂
h₁x : x ∈ (trivializationAt F₁ E₁ x₀).baseSet
h₂x : x ∈ (trivializationAt F₂ E₂ x₀).baseSet
h₃x : x ∈ (trivializationAt F₃ E₃ x₀).baseSet
⊢ ((inCoordinates F₁ E₁ (F₂ →L[𝕜] F₃) (fun x ↦ E₂ x →L[𝕜] E₃ x) x₀ x x₀ x ϕ) v) w =
    (Trivialization.linearMapAt 𝕜 (trivializationAt F₃ E₃ x₀) x)
      ((ϕ ((trivializationAt F₁ E₁ x₀).symm x v)) ((trivializationAt F₂ E₂ x₀).symm x w))

Tactic:
rw [inCoordinates_eq h₁x (by simp [h₂x, h₃x])]

Goal state after:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
inst✝²⁷ : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_16
inst✝¹⁴ : (x : B) → AddCommGroup (E₃ x)
inst✝¹³ : (x : B) → Module 𝕜 (E₃ x)
inst✝¹² : NormedAddCommGroup F₃
inst✝¹¹ : NormedSpace 𝕜 F₃
inst✝¹⁰ : TopologicalSpace (TotalSpace F₃ E₃)
inst✝⁹ : (x : B) → TopologicalSpace (E₃ x)
inst✝⁸ : TopologicalSpace B
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜 F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : FiberBundle F₃ E₃
inst✝² : VectorBundle 𝕜 F₃ E₃
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₃ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)
x₀ x : B
ϕ : E₁ x →L[𝕜] E₂ x →L[𝕜] E₃ x
v : F₁
w : F₂
h₁x : x ∈ (trivializationAt F₁ E₁ x₀).baseSet
h₂x : x ∈ (trivializationAt F₂ E₂ x₀).baseSet
h₃x : x ∈ (trivializationAt F₃ E₃ x₀).baseSet
⊢ ((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt (F₂ →L[𝕜] F₃) (fun x ↦ E₂ x →L[𝕜] E₃ x) x₀) x ⋯) ∘SL
          ϕ ∘SL ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x h₁x).symm)
        v)
      w =
    (Trivialization.linearMapAt 𝕜 (trivializationAt F₃ E₃ x₀) x)
      ((ϕ ((trivializationAt F₁ E₁ x₀).symm x v)) ((trivializationAt F₂ E₂ x₀).symm x w))