Skip to content

Commit 7fa953e

Browse files
committed
revert a lia back to omega
1 parent cf06366 commit 7fa953e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Data/Int/Interval.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ instance instLocallyFiniteOrder : LocallyFiniteOrder ℤ where
5757
· lia
5858
· intro
5959
use (x - (a + 1)).toNat
60-
lia
60+
omega
6161
finset_mem_Ioo a b x := by
6262
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
6363
addLeftEmbedding_apply]

0 commit comments

Comments
 (0)