feat(data/matrix/notation,data/fin): head and append simp (#5741)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/fin.lean

@@ -938,6 +938,10 @@ def append {α : Type*} {o : ℕ} (ho : o = m + n) (u : fin m → α) (v : fin n
   then u ⟨i, h⟩
   else v ⟨(i : ℕ) - m, (nat.sub_lt_left_iff_lt_add (le_of_not_lt h)).2 (ho ▸ i.property)⟩
 
+@[simp] lemma fin_append_apply_zero {α : Type*} {o : ℕ} (ho : (o + 1) = (m + 1) + n)
+  (u : fin (m + 1) → α) (v : fin n → α) :
+  fin.append ho u v 0 = u 0 := rfl
+
 end tuple
 
 section tuple_right

src/data/matrix/notation.lean

@@ -76,6 +76,8 @@ by { ext i, fin_cases i }
 
 section val
 
+@[simp] lemma head_fin_const (a : α) : vec_head (λ (i : fin (n + 1)), a) = a := rfl
+
 @[simp] lemma cons_val_zero (x : α) (u : fin m → α) : vec_cons x u 0 = x := rfl
 
 lemma cons_val_zero' (h : 0 < m.succ) (x : α) (u : fin m → α) :
@@ -211,6 +213,12 @@ begin
       exact nat.add_succ_lt_add i.property i.property } }
 end
 
+@[simp] lemma vec_head_vec_alt0 (hm : (m + 2) = (n + 1) + (n + 1)) (v : fin (m + 2) → α) :
+  vec_head (vec_alt0 hm v) = v 0 := rfl
+
+@[simp] lemma vec_head_vec_alt1 (hm : (m + 2) = (n + 1) + (n + 1)) (v : fin (m + 2) → α) :
+  vec_head (vec_alt1 hm v) = v 1 := rfl
+
 @[simp] lemma cons_vec_bit0_eq_alt0 (x : α) (u : fin n → α) (i : fin (n + 1)) :
   vec_cons x u (bit0 i) = vec_alt0 rfl (fin.append rfl (vec_cons x u) (vec_cons x u)) i :=
 by rw vec_alt0_append