From a239bba729a6c4590ab8ee6abf39d31c30c40f3d Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 1 Feb 2019 19:11:43 -0800 Subject: [PATCH] fix(src/data/*/Ico): succ_top is too aggressive as a simp lemma --- src/data/finset.lean | 2 +- src/data/list/basic.lean | 2 +- src/data/multiset.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/data/finset.lean b/src/data/finset.lean index 0cdbbef7ca56e..19ca5874a4c2e 100644 --- a/src/data/finset.lean +++ b/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) := diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index 52dceb3b4a1b2..e509d84f0f5a6 100644 --- a/src/data/list/basic.lean +++ b/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 := diff --git a/src/data/multiset.lean b/src/data/multiset.lean index be51f573db71a..ca71d66ce3343 100644 --- a/src/data/multiset.lean +++ b/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 :=