summaryrefslogtreecommitdiff
path: root/backends/lean/Base/IList/IList.lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/IList/IList.lean')
-rw-r--r--backends/lean/Base/IList/IList.lean5
1 files changed, 2 insertions, 3 deletions
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index f10ec4e7..79de93d5 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -294,7 +294,6 @@ open Arith in
have := tl.len_pos
linarith
else
- simp at hineq
have : 0 < i := by int_tac
simp [*]
apply hi
@@ -419,8 +418,8 @@ theorem index_itake_append_end [Inhabited α] (i j : Int) (l0 l1 : List α)
match l0 with
| [] => by
simp at *
- have := index_itake i j l1 (by simp_all) (by simp_all) (by simp_all; int_tac)
- simp [*]
+ have := index_itake i j l1 (by simp_all) (by simp_all) (by int_tac)
+ try simp [*]
| hd :: tl =>
have : ¬ i = 0 := by simp at *; int_tac
if hj : j = 0 then by simp_all; int_tac -- Contradiction