Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜₁ : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝¹³ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝⁹ : (x : B) → AddCommGroup (E₂ x)
inst✝⁸ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁶ : TopologicalSpace B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : FiberBundle F₁ E₁
inst✝³ : (x : B) → TopologicalSpace (E₂ x)
inst✝² : FiberBundle F₂ E₂
inst✝¹ : Trivialization.IsLinear 𝕜₁ e₁
inst✝ : Trivialization.IsLinear 𝕜₂ e₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ cast ⋯ (↑(continuousLinearMap σ e₁ e₂).symm (b, L)).snd =
    Trivialization.symmL 𝕜₂ e₂ b ∘SL L ∘SL Trivialization.continuousLinearMapAt 𝕜₁ e₁ b

pp: case hb
𝕜₁ : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝¹³ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝⁹ : (x : B) → AddCommGroup (E₂ x)
inst✝⁸ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁶ : TopologicalSpace B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : FiberBundle F₁ E₁
inst✝³ : (x : B) → TopologicalSpace (E₂ x)
inst✝² : FiberBundle F₂ E₂
inst✝¹ : Trivialization.IsLinear 𝕜₁ e₁
inst✝ : Trivialization.IsLinear 𝕜₂ e₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ b ∈ (continuousLinearMap σ e₁ e₂).baseSet

Tactic:
]

Goal state after:
𝕜₁ : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝¹³ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝⁹ : (x : B) → AddCommGroup (E₂ x)
inst✝⁸ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁶ : TopologicalSpace B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : FiberBundle F₁ E₁
inst✝³ : (x : B) → TopologicalSpace (E₂ x)
inst✝² : FiberBundle F₂ E₂
inst✝¹ : Trivialization.IsLinear 𝕜₁ e₁
inst✝ : Trivialization.IsLinear 𝕜₂ e₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ cast ⋯ (↑(continuousLinearMap σ e₁ e₂).symm (b, L)).snd =
    Trivialization.symmL 𝕜₂ e₂ b ∘SL L ∘SL Trivialization.continuousLinearMapAt 𝕜₁ e₁ b

case hb
𝕜₁ : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝¹³ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝⁹ : (x : B) → AddCommGroup (E₂ x)
inst✝⁸ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁶ : TopologicalSpace B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : FiberBundle F₁ E₁
inst✝³ : (x : B) → TopologicalSpace (E₂ x)
inst✝² : FiberBundle F₂ E₂
inst✝¹ : Trivialization.IsLinear 𝕜₁ e₁
inst✝ : Trivialization.IsLinear 𝕜₂ e₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ b ∈ (continuousLinearMap σ e₁ e₂).baseSet