unknownId.lean:3:7-3:10: error(lean.unknownIdentifier): Unknown identifier `bla✝`
unknownId.lean:6:2-6:5: error(lean.unknownIdentifier): Unknown identifier `bla✝`
unknownId.lean:11:6-11:9: error(lean.unknownIdentifier): Unknown identifier `bla✝`