abs_Lipschitz breaks at about lecture 11

[ketilwright]

For logisticaI reasons, I've taken to working the game levels in VSCode rather than in a browser. That requires that I bring in some definitions manually, either by pasting them in from the online game, or from the repo.

Up to lecture 11, this definition works:

theorem abs_Lipschitz {x y: ℝ} : |(|x| - |y|)| ≤ |(x - y)| := abs_abs_sub_abs_le x y

But in the chapter on Cauchy Sequences, it seems we have abandoned R in favor of R/Q.

theorem IsBdd_of_Cauchy {X : Type*} [NormedField X] [LinearOrder X] [IsStrictOrderedRing X] (a : ℕ → X) (ha : IsCauchy a) : SeqBdd a := by

So that definition for Lipschitz fails in mysterious ways. I found I can change my definition to this:

theorem abs_Lipschitz {X: Type*} [NormedField X] [LinearOrder X] [IsStrictOrderedRing X] {x y: X} : |(|x| - |y|)| ≤ |(x - y)| := abs_abs_sub_abs_le x y

That fixes my proof (in VSCode) of IsBddOfCauchy, but fails in the online game. BTW, the game reports the type of Lipschitz as:

Note: The full type of @abs_Lipschitzis ∀ {x y : ℝ}, ||x| - |y|| ≤ |x - y|

But I am out of my depth with lean at this level.