simp_cache_perf_issue.lean:2:0-2:7: warning: declaration uses `sorry`