two more tests

leanprover · Jan 16, 2025 · d39c120 · d39c120
1 parent 1b4ac01
commit d39c120
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git 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
@@ -12,3 +12,5 @@ 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, ∃ 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