chore(Algebra/Order/Group): golf entire max_sub_max_le_max using grind (leanprover-community#29850)

Author: euprunin

Mathlib/Algebra/Order/Group/MinMax.lean

@@ -65,13 +65,7 @@ section LinearOrderedAddCommGroup
 variable {α : Type*} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]
 
 theorem max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b - d) := by
-  simp only [sub_le_iff_le_add, max_le_iff]; constructor
-  · calc
-    a = a - c + c := (sub_add_cancel a c).symm
-    _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_left _ _) (le_max_left _ _)
-  · calc
-    b = b - d + d := (sub_add_cancel b d).symm
-    _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_right _ _) (le_max_right _ _)
+  grind
 
 theorem abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max |a - c| |b - d| := by
   refine abs_sub_le_iff.2 ⟨?_, ?_⟩