no goals
𝓕 : Type ?u.791224
𝕜 : Type ?u.791227
α : Type ?u.791230
ι : Type ?u.791233
κ : Type ?u.791236
E : Type u_1
F : Type ?u.791242
G : Type ?u.791245
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
a : E
⊢ ‖a ^ n‖₊ ≤ ↑n * ‖a‖₊
simpa only [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_nat_cast] using
  norm_pow_le_mul_norm n a