no tricks when proving associativity of min

One of the exercises in chapter 2.4 is proving associativity of min. The text above the exercise suggests that there exists a shorter proof by using one of the newly introduced tricks from this chapter, like the "repeat" tactic for example. However, the offered solution does not feature any of these tricks. An additional text was added to not mislead readers into thinking that any of these tricks can be used here.

MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean

@@ -131,7 +131,6 @@ whether or not you use these tricks,
 we encourage you to prove the following:
 TEXT. -/
 -- QUOTE:
--- BOTH:
 example : max a b = max b a := by
 /- EXAMPLES:
   sorry
@@ -141,8 +140,13 @@ SOLUTIONS: -/
     apply max_le
     apply le_max_right
     apply le_max_left
+-- QUOTE.
 
--- BOTH:
+/- TEXT:
+There is no obvious way to shorten the proof of the following theorem with the mentioned tricks.
+At the very least, try using dots or the ``show`` tactic to structure the proof you found:
+TEXT. -/
+-- QUOTE:
 example : min (min a b) c = min a (min b c) := by
 /- EXAMPLES:
   sorry