grind_preinstance_set_bug.lean:3:8-3:11: warning: declaration uses `sorry`