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₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ 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₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
x✝¹ : B × (F₁ →SL[σ] F₂)
x : B
f : F₁ →SL[σ] F₂
x✝ : (x, f) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
right✝ : (x, f).2 ∈ univ
v : F₁
⊢ (Trivialization.continuousLinearMapAt 𝕜₂ e₂ x)
      ((Trivialization.symmL 𝕜₂ e₂ x)
        (f ((Trivialization.continuousLinearMapAt 𝕜₁ e₁ x) ((Trivialization.symmL 𝕜₁ e₁ x) v)))) =
    f v

Tactic:
Trivialization.continuousLinearMapAt_symmL,

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₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ 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₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
x✝¹ : B × (F₁ →SL[σ] F₂)
x : B
f : F₁ →SL[σ] F₂
x✝ : (x, f) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
right✝ : (x, f).2 ∈ univ
v : F₁
⊢ f ((Trivialization.continuousLinearMapAt 𝕜₁ e₁ x) ((Trivialization.symmL 𝕜₁ e₁ x) v)) = f v

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₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ 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₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
x✝¹ : B × (F₁ →SL[σ] F₂)
x : B
f : F₁ →SL[σ] F₂
x✝ : (x, f) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
right✝ : (x, f).2 ∈ univ
v : F₁
⊢ x ∈ e₂.baseSet