chore: add Rat.max_def lemma

src/Init/Data/Rat/Lemmas.lean

@@ -1023,6 +1023,19 @@ theorem ofScientific_def' :
   · push_cast
     rfl
 
+/-!
+# min and max
+-/
+
+@[grind =] protected theorem max_def {n m : Rat} : max n m = if n ≤ m then m else n := rfl
+
+@[grind =] protected theorem min_def {n m : Rat} : min n m = if n ≤ m then n else m := rfl
+
+
+/-!
+# floor
+-/
+
 theorem floor_def (a : Rat) : a.floor = a.num / a.den := by
   rw [Rat.floor]
   split <;> simp_all

tests/lean/run/grind_rat.lean

@@ -0,0 +1 @@
+example : (1 : Rat) + max 2 3 = 4 := by grind