no goals
α : Type ?u.12618
β : Type u_1
γ : Type ?u.12624
ι : Type ?u.12627
inst✝² : NormedField α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
t : ℝ
ht : 0 ≤ t
x : β
⊢ ‖t • x‖ = t * ‖x‖
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]