fix(src/data/*/Ico): succ_top is too aggressive as a simp lemma

src/data/finset.lean

@@ -1693,7 +1693,7 @@ by rw [← to_finset, ← to_finset, ← multiset.to_finset_add,
 @[simp] theorem succ_singleton {n : ℕ} : Ico n (n+1) = {n} :=
 eq_of_veq $ multiset.Ico.succ_singleton
 
-@[simp] theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = insert m (Ico n m) :=
+theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = insert m (Ico n m) :=
 by rw [← to_finset, multiset.Ico.succ_top h, multiset.to_finset_cons, to_finset]
 
 theorem eq_cons {n m : ℕ} (h : n < m) : Ico n m = insert n (Ico (n + 1) m) :=

src/data/list/basic.lean

@@ -4065,7 +4065,7 @@ end
 @[simp] theorem succ_singleton {n : ℕ} : Ico n (n+1) = [n] :=
 by dsimp [Ico]; simp [nat.add_sub_cancel_left]
 
-@[simp] theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = Ico n m ++ [m] :=
+theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = Ico n m ++ [m] :=
 by rwa [← succ_singleton, append_consecutive]; exact nat.le_succ _
 
 theorem eq_cons {n m : ℕ} (h : n < m) : Ico n m = n :: Ico (n + 1) m :=

src/data/multiset.lean

@@ -2996,7 +2996,7 @@ congr_arg coe $ list.Ico.append_consecutive hnm hml
 @[simp] theorem succ_singleton {n : ℕ} : Ico n (n+1) = {n} :=
 congr_arg coe $ list.Ico.succ_singleton
 
-@[simp] theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = m :: Ico n m :=
+theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = m :: Ico n m :=
 by rw [Ico, list.Ico.succ_top h, ← coe_add, add_comm]; refl
 
 theorem eq_cons {n m : ℕ} (h : n < m) : Ico n m = n :: Ico (n + 1) m :=