unknown identifier "assume"

Stream: new members

[Kevin Cheung]

I was trying some examples in the Lean Reference manual in Lean 4 that uses "assume". It seems that Lean 4 doesn't have "assume" anymore since it gives me an "unknown identifier" error. What would be the replacement for it in Lean 4?

[Alex J. Best]

I think assume used to just be another way of spelling intro

[Reid Barton]

Or fun

[Kevin Cheung]

I see. So basically the syntactic sugar "assume" has been eliminated from Lean 4.