diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 3d3a08c601..937d4dc6f8 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -106,6 +106,8 @@ instance instOfNat : OfNat (Fin (no_index (n+1))) i where
 instance : Inhabited (Fin (no_index (n+1))) where
   default := 0
 
+@[simp] theorem zero_eta : (⟨0, Nat.zero_lt_succ _⟩ : Fin (n + 1)) = 0 := rfl
+
 theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
   fun h' => absurd (eq_of_val_eq h') h
 
diff --git a/tests/lean/run/1302.lean b/tests/lean/run/1302.lean
index 0cc9fa7d65..49026a8127 100644
--- a/tests/lean/run/1302.lean
+++ b/tests/lean/run/1302.lean
@@ -1,4 +1,4 @@
-@[simp] theorem get_cons_zero {as : List α} : (a :: as).get ⟨0, Nat.zero_lt_succ _⟩ = a := rfl
+@[simp] theorem get_cons_zero {as : List α} : (a :: as).get (0 : Fin (as.length + 1)) = a := rfl
 
 example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
   simp
@@ -10,4 +10,4 @@ example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
   simp
 
 example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
-  rw [get_cons_zero]
+  rw [Fin.zero_eta, get_cons_zero]