diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 2e96006e0222..e115b42ec865 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -1057,11 +1057,10 @@ instance decidableBallLE (n : Nat) (P : ∀ k, k ≤ n → Prop) [∀ n h, Decid
   decidable_of_iff (∀ (k) (h : k < succ n), P k (le_of_lt_succ h))
     ⟨fun m k h => m k (lt_succ_of_le h), fun m k _ => m k _⟩
 
-instance decidableExistsLT [DecidablePred p] :
-    DecidablePred fun n => ∃ m : Nat, m < n ∧ p m :=
-  fun n => match Nat.decidableBallLT n (fun (m : Nat) (_ : m < n) => ¬p m) with
-  | isTrue h => isFalse (by simpa using h)
-  | isFalse h => isTrue (by simpa using h)
+instance decidableExistsLT [DecidablePred p] : DecidablePred fun n => ∃ m : Nat, m < n ∧ p m
+  | n => match Nat.decidableBallLT n (fun (m : Nat) (_ : m < n) => ¬p m) with
+    | isTrue h => isFalse (by simpa using h)
+    | isFalse h => isTrue (by simpa using h)
 
 instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Nat, m ≤ n ∧ p m :=
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
diff --git a/tests/lean/run/natDecidableBallLT.lean b/tests/lean/run/natDecidableBallLT.lean
index 3d8f7f7e0be5..38e17ad5024f 100644
--- a/tests/lean/run/natDecidableBallLT.lean
+++ b/tests/lean/run/natDecidableBallLT.lean
@@ -10,5 +10,7 @@ set_option maxHeartbeats 5000
 example : ∀ a < 600, a ^ 2 ≠ 7 := by decide
 example : ∀ a ≤ 600, a ^ 2 ≠ 7 := by decide
 example : ∀ a : Fin 600, (a : Nat) ^ 2 ≠ 7 := by decide
-example : ∃ a < 600, a^2 = 90000 := by decide
-example : ∃ a ≤ 600, a^2 = 90000 := by decide
+example : ∃ a < 600, a ^ 2 = 90000 := by decide
+example : ∃ a ≤ 600, a ^ 2 = 90000 := by decide
+example : ∃ a, ∃ h : a < 599, (⟨a, h⟩ : Fin 599) * 2 = 1 := by decide
+example : ∃ a, ∃ h : a ≤ 600, (⟨a, Nat.lt_add_one_of_le h⟩ : Fin 601) * 2 = 1 := by decide