Error "unknown package 'analysis'"

Stream: mathlib4

[Donna Jo]

Hello, could anyone please help me fix the error "unknown package 'analysis'" when importing analysis.calculus.deriv? Thanks a lot!

[Johan Commelin]

Sounds like you are mixing lean 3 and lean 4.

[Eric Wieser]

import analysis.calculus.deriv is mathlib3 code. Are you using Lean 3 or Lean 4?

[Johan Commelin]

The error is a lean 4 error

[Eric Wieser]

@Donna Jo, you've started four threads about getting started, but haven't replied to any of the people trying to help you. Can you do that instead of creating more threads?

[Eric Wieser]

(#new members > Error "Waiting for Lean server to start and #new members > import can't be found are the merged versions of the other three threads)