librarySearch.lean:395:0-395:7: warning: declaration uses 'sorry'
librarySearch.lean:405:0-405:7: warning: declaration uses 'sorry'
librarySearch.lean:493:0-493:7: warning: declaration uses 'sorry'