no goals
R : Type ?u.552397
R' : Type ?u.552400
𝕜 : Type u_3
𝕜₂ : Type u_1
𝕜₃ : Type ?u.552409
𝕝 : Type ?u.552412
E : Type u_4
E₂ : Type u_2
E₃ : Type ?u.552421
F : Type ?u.552424
G : Type ?u.552427
ι : Type ?u.552430
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x✝ : E
⊢ ↑(comp p (c • f)) x✝ = ↑(‖c‖₊ • comp p f) x✝
rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
  smul_eq_mul, comp_apply]