fix tests

tests/lean/run/1017.lean

@@ -30,17 +30,17 @@ instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where
     cases h; case intro w h =>
     induction w generalizing s
     case zero =>
-      intro ⟨s',h'⟩ h_next
+      intro s' h' h_next
       simp [hasNext] at h_next
       cases h_next; case intro x h_next =>
       simp [lengthBoundedBy, isEmpty, Option.isNone, take, h_next] at h
     case succ n ih =>
-      intro ⟨s',h'⟩ h_next
+      intro s' h' h_next
       simp [hasNext] at h_next
       cases h_next; case intro x h_next =>
       simp [lengthBoundedBy, take, h_next] at h
       have := ih s' h
-      exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) this
+      exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) (by simpa)
   ⟩⟩
 
 def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α

tests/lean/run/issue3175.lean

@@ -2,11 +2,9 @@ def foo : (n : Nat) → (i : Fin n) → Bool
   | 0, _ => false
   | 1, _ => false
   | _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩
-decreasing_by simp_wf; simp_arith
 
 def bar : (n : Nat) → (i : Fin n) → Bool
   | 0, _ => false
   | 1, _ => false
   | _+2, _ => bar 1 ⟨0, Nat.zero_lt_one⟩
-termination_by n i => n
-decreasing_by simp_wf; simp_arith
+termination_by n => n

tests/lean/run/simpArith1.lean

@@ -7,16 +7,6 @@ theorem ex2 : a + b < b + 1 + a + c := by
 theorem ex3 : a + (fun x => x) b < b + 1 + a + c := by
   simp_arith
 
-/--
-info: a b c : Nat
-⊢ (fun x => x) b ≤ b + c
--/
-#guard_msgs in
-theorem ex4 : a + (fun x => x) b < b + 1 + a + c := by
-  simp_arith (config := { beta := false })
-  trace_state
-  simp_arith
-
 theorem ex5 (h : a + d + b > b + 1 + (a + (c + c) + d)) : False := by
   simp_arith at h