inaccessibleAnnotDefEqIssue.lean:5:18-5:31: warning: declaration uses `sorry`