chore(Data/Fin/Tuple): generalize Type to Sort (#17161)

Generalize definitions and theorems in `Data/Fin/Tuple/Basic` to take in `Sort` by default instead of `Type`.

The exceptions are theorems that interact with existing type classes such as `Preorder`, `Prod`, and `Set`, which expect `Type`.

For instance, the following is added specifically for some theorems about `Preorder`:

```lean4
variable {α : Fin (n + 1) → Type*}
-- instead of variable {α : Fin (n + 1) → Sort*}
```



Co-authored-by: Quang Dao <quangdao@umich.edu>

Author: quangvdao

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -302,7 +302,7 @@ noncomputable def fslope (p : FormalMultilinearSeries 𝕜 𝕜 E) : FormalMulti
 theorem coeff_fslope : p.fslope.coeff n = p.coeff (n + 1) := by
   simp only [fslope, coeff, ContinuousMultilinearMap.curryLeft_apply]
   congr 1
-  exact Fin.cons_self_tail 1
+  exact Fin.cons_self_tail (fun _ => (1 : 𝕜))
 
 @[simp]
 theorem coeff_iterate_fslope (k n : ℕ) : (fslope^[k] p).coeff n = p.coeff (n + k) := by