tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`