The ecample in The Schröder-Bernstein Theorem

Stream: lean4

[Jiaheng Xiong]

I try to run the example of The Schröder-Bernstein Theorem in Theorem Proving in Lean, but the invFun can not be used while the book told me this function is included in the Mathlib. This is my code:
import Mathlib
noncomputable section
open Classical
variable {α β : Type*} [Nonempty β]

#check (invFun g : α → β)
#check (leftInverse_invFun : Injective g → LeftInverse (invFun g) g)
#check (leftInverse_invFun : Injective g → ∀ y, invFun g (g y) = y)
#check (invFun_eq : (∃ y, g y = x) → g (invFun g x) = x)
And VS report unknown identifier 'invFun'

[Patrick Massot]

Replace open Classical by open Classical Function

[Patrick Massot]

And did you mean "Mathematics in Lean" rather than "Theorem proving in Lean"? Those are different books.

[Patrick Massot]

You are not meant to copy-paste a random snippet from the book. All code in each section is related. You can clone the repository as explained in the introduction to get Lean files that are ready to explore.

[Jiaheng Xiong]

Thank you. I am sorry, it is Mathematics in Lean.