𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.578081
E : Type u_1
Eₗ : Type ?u.578087
F : Type u_2
Fₗ : Type ?u.578093
G : Type ?u.578096
Gₗ : Type ?u.578099
𝓕 : Type ?u.578102
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ TopologicalAddGroup.toUniformSpace (E →SL[σ₁₂] F) = TopologicalAddGroup.toUniformSpace (E →SL[σ₁₂] F)
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.578081
E : Type u_1
Eₗ : Type ?u.578087
F : Type u_2
Fₗ : Type ?u.578093
G : Type ?u.578096
Gₗ : Type ?u.578099
𝓕 : Type ?u.578102
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ ContinuousLinearMap.tmpUniformSpace = uniformSpace
rw [← @UniformAddGroup.toUniformSpace_eq _ ContinuousLinearMap.tmpUniformSpace, ←
  @UniformAddGroup.toUniformSpace_eq _ ContinuousLinearMap.uniformSpace]
case h.e'_3
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.578081
E : Type u_1
Eₗ : Type ?u.578087
F : Type u_2
Fₗ : Type ?u.578093
G : Type ?u.578096
Gₗ : Type ?u.578099
𝓕 : Type ?u.578102
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ UniformSpace.toTopologicalSpace = UniformSpace.toTopologicalSpace
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.578081
E : Type u_1
Eₗ : Type ?u.578087
F : Type u_2
Fₗ : Type ?u.578093
G : Type ?u.578096
Gₗ : Type ?u.578099
𝓕 : Type ?u.578102
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ TopologicalAddGroup.toUniformSpace (E →SL[σ₁₂] F) = TopologicalAddGroup.toUniformSpace (E →SL[σ₁₂] F)
congr! 1
no goals
case h.e'_3
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.578081
E : Type u_1
Eₗ : Type ?u.578087
F : Type u_2
Fₗ : Type ?u.578093
G : Type ?u.578096
Gₗ : Type ?u.578099
𝓕 : Type ?u.578102
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ UniformSpace.toTopologicalSpace = UniformSpace.toTopologicalSpace
exact ContinuousLinearMap.tmp_topology_eq