remove simps

src/Std/Data/DTreeMap/Lemmas.lean

@@ -3123,7 +3123,6 @@ theorem minKey_modify_eq_minKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (modify t k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) :=
   Impl.Const.minKey_modify_eq_minKey t.wf
 
-@[simp]
 theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
     cmp (modify t k f |>.minKey he)
       (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
@@ -3263,7 +3262,6 @@ theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).minKey! = t.minKey! :=
   Impl.Const.minKey!_modify_eq_minKey! t.wf
 
-@[simp]
 theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   Impl.Const.compare_minKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)
@@ -3401,7 +3399,6 @@ theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback
     (modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
   Impl.Const.minKeyD_modify_eq_minKeyD t.wf
 
-@[simp]
 theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   Impl.Const.compare_minKeyD_modify_eq t.wf (instOrd := ⟨cmp⟩)
@@ -3752,7 +3749,6 @@ theorem maxKey_modify_eq_maxKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (modify t k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
   Impl.Const.maxKey_modify_eq_maxKey t.wf
 
-@[simp]
 theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
     cmp (modify t k f |>.maxKey he)
       (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
@@ -3892,7 +3888,6 @@ theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).maxKey! = t.maxKey! :=
   Impl.Const.maxKey!_modify_eq_maxKey! t.wf
 
-@[simp]
 theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   Impl.Const.compare_maxKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -3116,7 +3116,6 @@ theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).minKey! = t.minKey! :=
   Impl.Const.minKey!_modify_eq_minKey! h
 
-@[simp]
 theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   Impl.Const.compare_minKey!_modify_eq h (instOrd := ⟨cmp⟩)
@@ -3254,7 +3253,6 @@ theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k
     (modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
   Impl.Const.minKeyD_modify_eq_minKeyD h
 
-@[simp]
 theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   Impl.Const.compare_minKeyD_modify_eq h (instOrd := ⟨cmp⟩)
@@ -3592,7 +3590,6 @@ theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).maxKey! = t.maxKey! :=
   Impl.Const.maxKey!_modify_eq_maxKey! h
 
-@[simp]
 theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   Impl.Const.compare_maxKey!_modify_eq h (instOrd := ⟨cmp⟩)

src/Std/Data/TreeMap/Lemmas.lean

@@ -2058,7 +2058,6 @@ theorem minKey_modify_eq_minKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (modify t k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) :=
   DTreeMap.Const.minKey_modify_eq_minKey
 
-@[simp]
 theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
     cmp (modify t k f |>.minKey he)
       (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
@@ -2182,7 +2181,6 @@ theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).minKey! = t.minKey! :=
   DTreeMap.Const.minKey!_modify_eq_minKey!
 
-@[simp]
 theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   DTreeMap.Const.compare_minKey!_modify_eq
@@ -2304,7 +2302,6 @@ theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback
     (modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
   DTreeMap.Const.minKeyD_modify_eq_minKeyD
 
-@[simp]
 theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   DTreeMap.Const.compare_minKeyD_modify_eq
@@ -2617,7 +2614,6 @@ theorem maxKey_modify_eq_maxKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (modify t k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
   DTreeMap.Const.maxKey_modify_eq_maxKey
 
-@[simp]
 theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
     cmp (modify t k f |>.maxKey he)
       (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
@@ -2741,7 +2737,6 @@ theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).maxKey! = t.maxKey! :=
   DTreeMap.Const.maxKey!_modify_eq_maxKey!
 
-@[simp]
 theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   DTreeMap.Const.compare_maxKey!_modify_eq

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -2055,7 +2055,6 @@ theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).minKey! = t.minKey! :=
   DTreeMap.Raw.Const.minKey!_modify_eq_minKey! h
 
-@[simp]
 theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   DTreeMap.Raw.Const.compare_minKey!_modify_eq h
@@ -2177,7 +2176,6 @@ theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k
     (modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
   DTreeMap.Raw.Const.minKeyD_modify_eq_minKeyD h
 
-@[simp]
 theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   DTreeMap.Raw.Const.compare_minKeyD_modify_eq h
@@ -2478,7 +2476,6 @@ theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α
     (modify t k f).maxKey! = t.maxKey! :=
   DTreeMap.Raw.Const.maxKey!_modify_eq_maxKey! h
 
-@[simp]
 theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   DTreeMap.Raw.Const.compare_maxKey!_modify_eq h