{𝕜 : Type u_6} →
  {E : Type u_7} →
    {inst : NormedField 𝕜} →
      {inst_1 : SeminormedAddCommGroup E} →
        {P : Sort u} →
          {toModule : Module 𝕜 E} →
            {norm_smul_le : ∀ (a : 𝕜) (b : E), ‖a • b‖ ≤ ‖a‖ * ‖b‖} →
              {toModule' : Module 𝕜 E} →
                {norm_smul_le' : ∀ (a : 𝕜) (b : E), ‖a • b‖ ≤ ‖a‖ * ‖b‖} →
                  { toModule := toModule, norm_smul_le := norm_smul_le } =
                      { toModule := toModule', norm_smul_le := norm_smul_le' } →
                    (toModule ≍ toModule' → P) → P