no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_6
Eₗ : Type ?u.3580788
F : Type u_4
Fₗ : Type ?u.3580794
G : Type u_5
Gₗ : Type ?u.3580800
𝓕 : Type ?u.3580803
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
inst✝² : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g✝ : E →SL[σ₁₂] F
x✝ y z : E
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomIsometric σ₁₂
f : F →ₛₗᵢ[σ₂₃] G
g : E →SL[σ₁₂] F
x : E
⊢ ‖↑(ContinuousLinearMap.comp (toContinuousLinearMap f) g) x‖ = ‖↑g x‖
simp only [norm_map, coe_toContinuousLinearMap, coe_comp', Function.comp_apply]