chore(Order/Fin): move coe_max/coe_min (#22448)

Also deprecate `coe_sup`/`coe_inf`, since they're syntatically the same as `coe_max`/`coe_min` now.

Author: urkud

Mathlib/Order/Fin/Basic.lean

@@ -52,6 +52,15 @@ instance instBoundedOrder [NeZero n] : BoundedOrder (Fin n) where
   bot := 0
   bot_le := Fin.zero_le'
 
+@[simp, norm_cast]
+theorem coe_max (a b : Fin n) : ↑(max a b) = (max a b : ℕ) := rfl
+
+@[simp, norm_cast]
+theorem coe_min (a b : Fin n) : ↑(min a b) = (min a b : ℕ) := rfl
+
+@[deprecated (since := "2025-03-01")] alias coe_sup := coe_max
+@[deprecated (since := "2025-03-01")] alias coe_inf := coe_min
+
 /- There is a slight asymmetry here, in the sense that `0` is of type `Fin n` when we have
 `[NeZero n]` whereas `last n` is of type `Fin (n + 1)`. To address this properly would
 require a change to std4, defining `NeZero n` and thus re-defining `last n`

Mathlib/Order/Interval/Finset/Fin.lean

@@ -14,25 +14,7 @@ intervals as Finsets and Fintypes.
 
 assert_not_exists MonoidWithZero
 
-namespace Fin
-
-variable {n : ℕ} (a b : Fin n)
-
-@[simp, norm_cast]
-theorem coe_sup : ↑(a ⊔ b) = (a ⊔ b : ℕ) := rfl
-
-@[simp, norm_cast]
-theorem coe_inf : ↑(a ⊓ b) = (a ⊓ b : ℕ) := rfl
-
-@[simp, norm_cast]
-theorem coe_max : ↑(max a b) = (max a b : ℕ) := rfl
-
-@[simp, norm_cast]
-theorem coe_min : ↑(min a b) = (min a b : ℕ) := rfl
-
-end Fin
-
-open Finset Fin Function
+open Finset Function
 
 namespace Fin