isDefEqProjPerfIssue.lean:33:8-33:11: warning: declaration uses `sorry`