no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.169480
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (r • x) = ‖r‖ * gauge s x
rw [← smul_eq_mul, ← gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs]