isDefEqPerfIssue.lean:6:12-6:13: warning: declaration uses `sorry`