-- Mathlib/Topology/VectorBundle/Hom.lean
theorem continuousLinearMap_symm_apply' {b : B} (hb : b ∈ e₁.baseSet ∩ e₂.baseSet)
    (L : F₁ →SL[σ] F₂) :
    (continuousLinearMap σ e₁ e₂).symm b L =
      (e₂.symmL 𝕜₂ b).comp (L.comp <| e₁.continuousLinearMapAt 𝕜₁ b)

Proof state:
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:
exact hb

Result:
no goals

Proof state:
𝕜₁ : 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₂
⊢ (continuousLinearMap σ e₁ e₂).symm b L =
    (Trivialization.symmL 𝕜₂ e₂ b).comp (L.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ b))

Tactic:
rw [symm_apply]

Result:
𝕜₁ : 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).comp (L.comp (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

Proof state:
𝕜₁ : 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).comp (L.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ b))

Tactic:
rfl

Result:
no goals