chore(data/fin): reorder file to group declarations (#6109)

The `data/fin` file has a lot of definitions and lemmas. This reordering groups declarations and places ones that do not rely on `fin` operations first, like order. No definitions or lemma statements have been changed. A minimal amount of proofs have been rephrased. No reformatting of style has been done. Section titles have been added.

This is useful in preparation for redefining `fin` operations (lean#527). Additionally, it allows for better organization for other refactors like making `pred` and `pred_above` total.

src/algebra/linear_recurrence.lean

@@ -78,7 +78,7 @@ lemma is_sol_mk_sol (init : fin E.order → α) : E.is_solution (E.mk_sol init)
 
 /-- `E.mk_sol init`'s first `E.order` terms are `init`. -/
 lemma mk_sol_eq_init (init : fin E.order → α) : ∀ n : fin E.order, E.mk_sol init n = init n :=
-  λ n, by { rw mk_sol, simp only [n.is_lt, dif_pos, fin.mk_coe] }
+  λ n, by { rw mk_sol, simp only [n.is_lt, dif_pos, fin.mk_coe, fin.eta] }
 
 /-- If `u` is a solution to `E` and `init` designates its first `E.order` values,
   then `∀ n, u n = E.mk_sol init n`. -/

src/analysis/analytic/composition.lean

@@ -563,7 +563,7 @@ begin
   dsimp [composition.blocks_fun, composition.blocks, comp_change_of_variables],
   simp only [map_of_fn, nth_le_of_fn', function.comp_app],
   apply congr_arg,
-  rw [fin.ext_iff, fin.mk_coe]
+  exact fin.eta _ _
 end
 
 /-- Target set in the change of variables to compute the composition of partial sums of formal