tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`