Lean isn't classical.

Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.