feat(data/fin): add some lemmas about coercions and of_nat (#2522)

Two of these lemmas allow norm_cast to work with inequalities
involving fin values converted to ℕ.  The rest are for simplifying
expressions where of_nat is used to convert from ℕ to fin, in cases
where an inequality means of_nat does not in fact change the value.

There are very few lemmas relating to of_nat in mathlib at present.
These lemmas were found useful in formalising solutions to an olympiad
problem, see
<https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations>,
and seem more generally relevant than to just that particular problem.

src/data/fin.lean

@@ -98,6 +98,45 @@ attribute [simp] val_zero
 @[simp] lemma coe_one  {n : ℕ} : ((1 : fin (n+2)) : ℕ) = 1 := rfl
 @[simp] lemma coe_two  {n : ℕ} : ((2 : fin (n+3)) : ℕ) = 2 := rfl
 
+/-- `a < b` as natural numbers if and only if `a < b` in `fin n`. -/
+@[norm_cast, simp] lemma coe_fin_lt {n : ℕ} {a b : fin n} : (a : ℕ) < (b : ℕ) ↔ a < b :=
+iff.rfl
+
+/-- `a ≤ b` as natural numbers if and only if `a ≤ b` in `fin n`. -/
+@[norm_cast, simp] lemma coe_fin_le {n : ℕ} {a b : fin n} : (a : ℕ) ≤ (b : ℕ) ↔ a ≤ b :=
+iff.rfl
+
+/-- Converting an in-range number to `fin (n + 1)` with `of_nat`
+produces a result whose value is the original number.  -/
+lemma of_nat_val_of_lt {n : ℕ} {a : ℕ} (h : a < n + 1) :
+  ((of_nat a) : fin (n + 1)).val = a :=
+nat.mod_eq_of_lt h
+
+/-- Converting the value of a `fin (n + 1)` to `fin (n + 1)` with `of_nat`
+results in the same value.  -/
+@[simp] lemma of_nat_val_eq_self {n : ℕ} (a : fin (n + 1)) : of_nat a.val = a :=
+begin
+  rw eq_iff_veq,
+  exact of_nat_val_of_lt a.is_lt
+end
+
+/-- `of_nat` of an in-range number, converted back to `ℕ`, is that
+number. -/
+lemma of_nat_coe_of_lt {n : ℕ} {a : ℕ} (h : a < n + 1) :
+  (((of_nat a) : fin (n + 1)) : ℕ) = a :=
+nat.mod_eq_of_lt h
+
+/-- Converting a `fin (n + 1)` to `ℕ` and back with `of_nat` results in
+the same value. -/
+@[simp] lemma of_nat_coe_eq_self {n : ℕ} (a : fin (n + 1)) : of_nat (a : ℕ) = a :=
+of_nat_val_eq_self a
+
+attribute [simp] of_nat_zero
+
+/-- `of_nat 1` is `1 : fin (n + 1)`. -/
+@[simp] lemma of_nat_one {n : ℕ} : (of_nat 1 : fin (n + 1)) = 1 :=
+rfl
+
 /-- Assume `k = l`. If two functions defined on `fin k` and `fin l` are equal on each element,
 then they coincide (in the heq sense). -/
 protected lemma heq_fun_iff {α : Type*} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α} :