Need help on square roots within The Mechanics of Proof

Stream: Lean for teaching

[Kevin Cheung]

I have been teaching a course using The Mechanics of Proof. I want to add some examples involving square roots of reals but importing Mathlib.Data.Real.Sqrt results in multiple conflicts with Library.Basic that comes with the book. Any suggestions on how to resolve the conflicts?

[Jon Eugster]

You could try putting everything MoP defines inside a namespace. Concretely, add

namespace MechanicsOfProof

to each file just after the imports. This might break some dot-notation like you'll have to write Nat.Odd.pow h instead of h.pow for (h : Odd n), but maybe dot-notation isn't used much anyways