It's confusing that first MIL chapter is missing an import

Stream: new members

[Dan Abramov]

I filed a bug report about this here: https://github.com/avigad/mathematics_in_lean_source/pull/278

I'm wondering if this used to work before? I wouldn't have guessed what the issue is without googling this.