fix: Exercise 8.5.5(b) — pullback of < need not be a linear order

[Chessing234]

Summary

• Ex_8_5_5_b is false: take X = Bool, Y = ℝ, and f constantly 0.
• The proposed relation f x < f y ∨ x = y reduces to equality on Bool.
• That is not a total order (false and true are incomparable), so it cannot arise from a LinearOrder on X.

Test plan

• CI / lake build Analysis/Section_8_5.lean

[teorth]

Closing this one under the repository's solutions policy — see the consolidated note on #667 for the full explanation and for what would be most welcome instead.

Briefly: this PR discharges sorrys that are reader exercises in Analysis I, and removes the accompanying hint comment ("the first line of this construction should be either apply isTrue or apply isFalse"). From the README:

Portions of the text that were left as exercises to the reader are rendered in this translation as sorrys. Readers are welcome to fork the repository here to try their hand at these exercises, but I do not intend to place solutions in this repository directly.

Nothing wrong with the mathematics here — this is purely about what belongs in the main repository.