Unknown identifier 'take'

[jachymb]

The first "Try it yourself example" of the chapter "4 Quantifiers and Equality" won't compile and throws the error Unknown identifier 'take' using Lean 3.28. I guess there should be an assume instead of take and also take probably should not be hilighted anymore and have it's other mentions in the document removed too.

[jachymb]

but it seems the tutorial is intended for LEAN 2 only? So maybe this should just be closed.