chore(Control/Random): Use NeZero instead of returning Fin n.succ (#22672)

Changes the random generation of `Fin`s to take `NeZero n` instead of giving a `Fin n.succ`.

Author: plp127

Mathlib/Control/Random.lean

@@ -95,10 +95,10 @@ def randBound (α : Type u)
   (BoundedRandom.randomR lo hi h : RandGT g _ _)
 
 /-- Generate a random `Fin`. -/
-def randFin {n : Nat} [RandomGen g] : RandGT g m (Fin n.succ) :=
-  fun ⟨g⟩ ↦ pure <| randNat g 0 n |>.map (Fin.ofNat' _) ULift.up
+def randFin {n : Nat} [NeZero n] [RandomGen g] : RandGT g m (Fin n) :=
+  fun ⟨g⟩ ↦ pure <| randNat g 0 (n - 1) |>.map (Fin.ofNat' n) ULift.up
 
-instance {n : Nat} : Random m (Fin n.succ) where
+instance {n : Nat} [NeZero n] : Random m (Fin n) where
   random := randFin
 
 /-- Generate a random `Bool`. -/
@@ -113,10 +113,10 @@ instance {α : Type u} [ULiftable m m'] [Random m α] : Random m' (ULift.{v} α)
 
 instance : BoundedRandom m Nat where
   randomR lo hi h _ := do
-    let z ← rand (Fin (hi - lo).succ)
+    let z ← rand (Fin (hi - lo + 1))
     pure ⟨
       lo + z.val, Nat.le_add_right _ _,
-      Nat.add_le_of_le_sub' h (Nat.le_of_succ_le_succ z.isLt)
+      Nat.add_le_of_le_sub' h (Nat.le_of_lt_add_one z.isLt)
     ⟩
 
 instance : BoundedRandom m Int where

MathlibTest/random.lean

@@ -89,7 +89,7 @@ info: GOOD
   IO.runRandWith 257 <| do
     let mut count := 0
     for _ in [:10000] do
-      if (← randFin (n := 2)) == 1 then count := count + 1
+      if (← randFin : Fin 3) == 1 then count := count + 1
     if Float.abs (0.333 - (count / Nat.toFloat 10000)) < 0.01 then
       IO.println "GOOD"
     else
@@ -103,7 +103,7 @@ info: GOOD
   IO.runRandWith 257 <| do
     let mut count := 0
     for _ in [:10000] do
-      if (← randFin (n := 1)) == 0 then count := count + 1
+      if (← randFin : Fin 2) == 0 then count := count + 1
     if Float.abs (0.5 - (count / Nat.toFloat 10000)) < 0.01 then
       IO.println "GOOD"
     else
@@ -117,7 +117,7 @@ info: GOOD
   IO.runRandWith 257 <| do
     let mut count := 0
     for _ in [:10000] do
-      if (← randFin (n := 9)) == 5 then count := count + 1
+      if (← randFin : Fin 10) == 5 then count := count + 1
     if Float.abs (0.1 - (count / Nat.toFloat 10000)) < 0.01 then
       IO.println "GOOD"
     else