diff --git a/src/data/fin.lean b/src/data/fin.lean
index 1c1d20c4d40ee..00851779a52ff 100644
--- a/src/data/fin.lean
+++ b/src/data/fin.lean
@@ -125,9 +125,18 @@ le_of_lt_succ i.is_lt
 
 @[simp] lemma cast_lt_val (k : fin m) (h : k.1 < n) : (k.cast_lt h).val = k.val := rfl
 
+@[simp] lemma cast_le_val (k : fin m) (h : m ≤ n) : (k.cast_le h).val = k.val := rfl
+
+@[simp] lemma cast_add_val (k : fin m) : (k.cast_add n).val = k.val := rfl
+
+@[simp] lemma last_val (n : ℕ) : (last n).val = n := rfl
+
 @[simp] lemma cast_succ_cast_lt (i : fin (n + 1)) (h : i.val < n) : cast_succ (cast_lt i h) = i :=
 fin.eq_of_veq rfl
 
+@[simp] lemma cast_lt_cast_succ {n : ℕ} (a : fin n) (h : a.1 < n) : cast_lt (cast_succ a) h = a :=
+by cases a; refl
+
 @[simp] lemma sub_nat_val (i : fin (n + m)) (h : i.val ≥ m) : (i.sub_nat m h).val = i.val - m :=
 rfl