From b3dd78ff4c8785b6ff9bce9927df90f8c78a9109 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 22:04:13 +0200
Subject: Update Lean to v4.9.0-rc1

---
 backends/lean/Base/Arith/Base.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'backends/lean/Base/Arith/Base.lean')

diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index 8ada4171..fb6b12e5 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -1,6 +1,5 @@
 import Lean
-import Std.Data.Int.Lemmas
-import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Linarith -- Introduces a lot of useful lemmas
 
 namespace Arith
 
@@ -21,12 +20,12 @@ theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by
   have hne : x - y ≠ 0 := by
     simp
     intro h
-    have: x = y := by linarith
+    have: x = y := by omega
     simp_all
   have h := ne_zero_is_lt_or_gt hne
   match h with
-  | .inl _ => left; linarith
-  | .inr _ => right; linarith
+  | .inl _ => left; omega
+  | .inr _ => right; omega
 
 -- TODO: move?
 theorem add_one_le_iff_le_ne (n m : Nat) (h1 : m ≤ n) (h2 : m ≠ n) : m + 1 ≤ n := by
@@ -66,7 +65,7 @@ theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) :
 theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ)
   (h0 : ↑x' ≤ x) (h1 : x - ↑x' < y) :
   ↑(x.toNat - x') < y := by
-  have : 0 ≤ x := by linarith
+  have : 0 ≤ x := by omega
   simp [Int.toNat_sub_of_le, *]
 
 end Arith
-- 
cgit v1.2.3