∀ {S : Type u_2} {𝕜 : Type u_3} {E : Type u_1} [inst : CommRing 𝕜] [inst_1 : NormedRing E] [inst_2 : Algebra 𝕜 E]
  [inst_3 : SetLike S E] [inst_4 : SubringClass S E] [inst_5 : SMulMemClass S 𝕜 E] (s : S) (a b : ↥s),
  ‖a * b‖ ≤ ‖a‖ * ‖b‖