feat(data/list/of_fn): last_of_fn (#15474)

Also `of_fn_eq_nil_iff`.





Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/data/list/of_fn.lean

@@ -109,6 +109,20 @@ begin
     simp_rw [fin.cast_succ_fin_succ], }
 end
 
+@[simp] lemma of_fn_eq_nil_iff {n : ℕ} {f : fin n → α} :
+  of_fn f = [] ↔ n = 0 :=
+by cases n; simp only [of_fn_zero, of_fn_succ, eq_self_iff_true, nat.succ_ne_zero]
+
+lemma last_of_fn {n : ℕ} (f : fin n → α) (h : of_fn f ≠ [])
+  (hn : n - 1 < n := nat.pred_lt $ of_fn_eq_nil_iff.not.mp h) :
+  last (of_fn f) h = f ⟨n - 1, hn⟩ :=
+by simp [last_eq_nth_le]
+
+lemma last_of_fn_succ {n : ℕ} (f : fin n.succ → α)
+  (h : of_fn f ≠ [] := mt of_fn_eq_nil_iff.mp (nat.succ_ne_zero _)) :
+  last (of_fn f) h = f (fin.last _) :=
+last_of_fn f h
+
 /-- Note this matches the convention of `list.of_fn_succ'`, putting the `fin m` elements first. -/
 theorem of_fn_add {m n} (f : fin (m + n) → α) :
   list.of_fn f = list.of_fn (λ i, f (fin.cast_add n i)) ++ list.of_fn (λ j, f (fin.nat_add m j)) :=