docs(data/fintype/sort): add module docstring (#8643)

And correct typo in the docstrings

src/data/fintype/sort.lean

@@ -3,24 +3,31 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.fintype.basic
 import data.finset.sort
+import data.fintype.basic
 
-variables {α : Type*}
+/-!
+# Sorting a finite type
+
+This file provides two equivalences for linearly ordered fintypes:
+* `mono_equiv_of_fin`: Order isomorphism between `α` and `fin (card α)`.
+* `fin_sum_equiv_of_finset`: Equivalence between `α` and `fin m ⊕ fin n` where `m` and `n` are
+  respectively the cardinalities of some `finset α` and its complement.
+-/
 
 open finset
 
 /-- Given a linearly ordered fintype `α` of cardinal `k`, the order isomorphism
 `mono_equiv_of_fin α h` is the increasing bijection between `fin k` and `α`. Here, `h` is a proof
-that the cardinality of `s` is `k`. We use this instead of an isomorphism `fin s.card ≃o α` to avoid
-casting issues in further uses of this function. -/
-def mono_equiv_of_fin (α) [fintype α] [linear_order α] {k : ℕ}
-  (h : fintype.card α = k) : fin k ≃o α :=
+that the cardinality of `α` is `k`. We use this instead of an isomorphism `fin (card α) ≃o α` to
+avoid casting issues in further uses of this function. -/
+def mono_equiv_of_fin (α : Type*) [fintype α] [linear_order α] {k : ℕ} (h : fintype.card α = k) :
+  fin k ≃o α :=
 (univ.order_iso_of_fin h).trans $ (order_iso.set_congr _ _ coe_univ).trans order_iso.set.univ
 
-variables [decidable_eq α] [fintype α] [linear_order α] {m n : ℕ} {s : finset α}
+variables {α : Type*} [decidable_eq α] [fintype α] [linear_order α] {m n : ℕ} {s : finset α}
 
-/-- If `α` is a linearly ordered type, `s : finset α` has cardinality `m` and its complement has
+/-- If `α` is a linearly ordered fintype, `s : finset α` has cardinality `m` and its complement has
 cardinality `n`, then `fin m ⊕ fin n ≃ α`. The equivalence sends elements of `fin m` to
 elements of `s` and elements of `fin n` to elements of `sᶜ` while preserving order on each
 "half" of `fin m ⊕ fin n` (using `set.order_iso_of_fin`). -/