leanprover · nomeata · Jun 20, 2025 · Jun 20, 2025 · Jun 20, 2025 · Jun 20, 2025
diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
@@ -45,7 +45,7 @@ theorem em (p : Prop) : p ∨ ¬p :=
     | Or.inr h, _ => Or.inr h
     | _, Or.inr h => Or.inr h
     | Or.inl hut, Or.inl hvf =>
-      have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
+      have hne : u ≠ v := by simp [hvf, hut]
       Or.inl hne
   have p_implies_uv : p → u = v :=
     fun hp =>

diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
@@ -50,7 +50,7 @@ attribute [simp] id_map
   (comp_map _ _ _).symm
 
 theorem Functor.map_unit [Functor f] [LawfulFunctor f] {a : f PUnit} : (fun _ => PUnit.unit) <$> a = a := by
-  simp [map]
+  simp
 
 /--
 An applicative functor satisfies the laws of an applicative functor.

diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean
@@ -67,7 +67,7 @@ protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad
   | Except.error _ => simp
   | Except.ok _ =>
     simp [←bind_pure_comp]; apply bind_congr; intro b;
-    cases b <;> simp [comp, Except.map, const]
+    cases b <;> simp [Except.map, const]
 
 protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
   change (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y

@@ -209,7 +209,7 @@ theorem Context.evalList_sort_congr
   induction c generalizing a b with
   | nil => simp [sort.loop, h₂]
   | cons c _  ih =>
-    simp [sort.loop]; apply ih; simp [evalList_insert ctx h, evalList]
+    simp [sort.loop]; apply ih; simp [evalList_insert ctx h]
     cases a with
     | nil => apply absurd h₃; simp
     | cons a as =>
@@ -282,7 +282,7 @@ theorem Context.toList_nonEmpty (e : Expr) : e.toList ≠ [] := by
     simp [Expr.toList]
     cases h : l.toList with
     | nil => contradiction
-    | cons => simp [List.append]
+    | cons => simp
 
 theorem Context.unwrap_isNeutral
   {ctx : Context α}
@@ -328,13 +328,13 @@ theorem Context.eval_toList (ctx : Context α) (e : Expr) : evalList α ctx e.to
   induction e with
   | var x => rfl
   | op l r ih₁ ih₂ =>
-    simp [evalList, Expr.toList, eval, ←ih₁, ←ih₂]
+    simp [Expr.toList, eval, ←ih₁, ←ih₂]
     apply evalList_append <;> apply toList_nonEmpty
 
 theorem Context.eval_norm (ctx : Context α) (e : Expr) : evalList α ctx (norm ctx e) = eval α ctx e := by
   simp [norm]
   cases h₁ : ContextInformation.isIdem ctx <;> cases h₂ : ContextInformation.isComm ctx <;>
-  simp_all [evalList_removeNeutrals, eval_toList, toList_nonEmpty, evalList_mergeIdem, evalList_sort]
+  simp_all [evalList_removeNeutrals, eval_toList, evalList_mergeIdem, evalList_sort]
 
 theorem Context.eq_of_norm (ctx : Context α) (a b : Expr) (h : norm ctx a == norm ctx b) : eval α ctx a = eval α ctx b := by
   have h := congrArg (evalList α ctx) (eq_of_beq h)

@@ -155,7 +155,7 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   cases xs
-  simp [attachWith_congr (List.push_toArray _ _)]
+  simp
 
 theorem pmap_eq_map_attach {p : α → Prop} {f : ∀ a, p a → β} {xs : Array α} (H) :
     pmap f xs H = xs.attach.map fun x => f x.1 (H _ x.2) := by
@@ -342,7 +342,7 @@ theorem foldl_attach {xs : Array α} {f : β → α → β} {b : β} :
     xs.attach.foldl (fun acc t => f acc t.1) b = xs.foldl f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
+    List.foldl_toArray', mem_toArray, List.foldl_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
@@ -361,7 +361,7 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
     xs.attach.foldr (fun t acc => f t.1 acc) b = xs.foldr f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
+    List.foldr_toArray', mem_toArray, List.foldr_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
@@ -470,7 +470,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
-  simp [attachWith, attach_append, map_pmap, pmap_append]
+  simp [attachWith]
 
 @[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
@@ -703,7 +703,7 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → Array β} {g : α → Array β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (xs.flatMap f) = xs.unattach.flatMap g := by
   cases xs
-  simp only [List.size_toArray, List.flatMap_toArray, List.unattach_toArray, List.length_unattach,
+  simp only [List.flatMap_toArray, List.unattach_toArray, 
     mk.injEq]
   rw [List.flatMap_subtype]
   simp [hf]

@@ -1788,7 +1788,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
   induction xs, i, h using Array.eraseIdx.induct with
   | @case1 xs i h h' xs' ih =>
     unfold eraseIdx
-    simp +zetaDelta [h', xs', ih]
+    simp +zetaDelta [h', ih]
   | case2 xs i h h' =>
     unfold eraseIdx
     simp [h']

@@ -119,13 +119,13 @@ abbrev pop_toList := @Array.toList_pop
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
 @[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
-  apply ext'; simp only [toList_append, toList_empty, List.append_nil]
+  apply ext'; simp only [toList_append, List.append_nil]
 
 @[deprecated append_empty (since := "2025-01-13")]
 abbrev append_nil := @append_empty
 
 @[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
-  apply ext'; simp only [toList_append, toList_empty, List.nil_append]
+  apply ext'; simp only [toList_append, List.nil_append]
 
 @[deprecated empty_append (since := "2025-01-13")]
 abbrev nil_append := @empty_append

@@ -223,15 +223,15 @@ theorem boole_getElem_le_count {xs : Array α} {i : Nat} {a : α} (h : i < xs.si
 @[grind =]
 theorem count_set {xs : Array α} {i : Nat} {a b : α} (h : i < xs.size) :
     (xs.set i a).count b = xs.count b - (if xs[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
-  simp [count_eq_countP, countP_set, h]
+  simp [count_eq_countP, countP_set]
 
 variable [LawfulBEq α]
 
 @[simp] theorem count_push_self {a : α} {xs : Array α} : count a (xs.push a) = count a xs + 1 := by
   simp [count_push]
 
 @[simp] theorem count_push_of_ne {xs : Array α} (h : b ≠ a) : count a (xs.push b) = count a xs := by
-  simp_all [count_push, h]
+  simp_all [count_push]
 
 theorem count_singleton_self {a : α} : count a #[a] = 1 := by simp
 
@@ -292,17 +292,17 @@ abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
 theorem count_le_count_map [BEq β] [LawfulBEq β] {xs : Array α} {f : α → β} {x : α} :
     count x xs ≤ count (f x) (map f xs) := by
   rcases xs with ⟨xs⟩
-  simp [List.count_le_count_map, countP_map]
+  simp [List.count_le_count_map]
 
 theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {xs : Array α} :
     count b (filterMap f xs) = countP (fun a => f a == some b) xs := by
   rcases xs with ⟨xs⟩
-  simp [List.count_filterMap, countP_filterMap]
+  simp [List.count_filterMap]
 
 theorem count_flatMap {α} [BEq β] {xs : Array α} {f : α → Array β} {x : β} :
     count x (xs.flatMap f) = sum (map (count x ∘ f) xs) := by
   rcases xs with ⟨xs⟩
-  simp [List.count_flatMap, countP_flatMap, Function.comp_def]
+  simp [List.count_flatMap, Function.comp_def]
 
 theorem countP_replace {a b : α} {xs : Array α} {p : α → Bool} :
     (xs.replace a b).countP p =

@@ -23,7 +23,7 @@ private theorem rel_of_isEqvAux
   induction i with
   | zero => contradiction
   | succ i ih =>
-    simp only [Array.isEqvAux, Bool.and_eq_true, decide_eq_true_eq] at heqv
+    simp only [Array.isEqvAux, Bool.and_eq_true] at heqv
     by_cases hj' : j < i
     next =>
       exact ih _ heqv.right hj'

@@ -206,7 +206,7 @@ theorem erase_eq_eraseP [LawfulBEq α] (a : α) (xs : Array α) : xs.erase a = x
 theorem erase_ne_empty_iff [LawfulBEq α] {xs : Array α} {a : α} :
     xs.erase a ≠ #[] ↔ xs ≠ #[] ∧ xs ≠ #[a] := by
   rcases xs with ⟨xs⟩
-  simp [List.erase_ne_nil_iff]
+  simp
 
 theorem exists_erase_eq [LawfulBEq α] {a : α} {xs : Array α} (h : a ∈ xs) :
     ∃ ys zs, a ∉ ys ∧ xs = ys.push a ++ zs ∧ xs.erase a = ys ++ zs := by
@@ -306,7 +306,7 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {xs : Array α} :
 @[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} :
     (replicate n a).erase a = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.erase_toArray]
-  simp [List.erase_replicate]
+  simp
 
 @[deprecated erase_replicate_self (since := "2025-03-18")]
 abbrev erase_mkArray_self := @erase_replicate_self
@@ -352,7 +352,7 @@ theorem getElem?_eraseIdx_of_lt {xs : Array α} {i : Nat} (h : i < xs.size) {j :
 theorem getElem?_eraseIdx_of_ge {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} (h' : i ≤ j) :
     (xs.eraseIdx i)[j]? = xs[j + 1]? := by
   rw [getElem?_eraseIdx]
-  simp only [dite_eq_ite, ite_eq_right_iff]
+  simp only [ite_eq_right_iff]
   intro h'
   omega
 

@@ -29,7 +29,7 @@ namespace Array
   · simp
     omega
   · simp only [size_extract] at h₁ h₂
-    simp [h]
+    simp
 
 theorem size_extract_le {as : Array α} {i j : Nat} :
     (as.extract i j).size ≤ j - i := by
@@ -162,7 +162,7 @@ theorem extract_sub_one {as : Array α} {i j : Nat} (h : j < as.size) :
 @[simp]
 theorem getElem?_extract_of_lt {as : Array α} {i j k : Nat} (h : k < min j as.size - i) :
     (as.extract i j)[k]? = some (as[i + k]'(by omega)) := by
-  simp [getElem?_extract, h]
+  simp [h]
 
 theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
     (as.extract 0 (j + 1))[j]? = as[j]? := by

@@ -81,7 +81,7 @@ theorem find?_eq_findSome?_guard {xs : Array α} : find? p xs = findSome? (Optio
 
 @[simp, grind =] theorem getElem_zero_filterMap {f : α → Option β} {xs : Array α} (h) :
     (xs.filterMap f)[0] = (xs.findSome? f).get (by cases xs; simpa [List.length_filterMap_eq_countP] using h) := by
-  cases xs; simp [← List.head_eq_getElem, ← getElem?_zero_filterMap]
+  cases xs; simp [← getElem?_zero_filterMap]
 
 @[simp, grind =] theorem back?_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f).back? = xs.findSomeRev? f := by
   cases xs; simp
@@ -122,7 +122,7 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
 theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
     (flatten xss)[0] = (xss.findSome? fun xs => xs[0]?).get (getElem_zero_flatten.proof h) := by
  have t := getElem?_zero_flatten xss
-  simp [getElem?_eq_getElem, h] at t
+  simp at t
   simp [← t]
 
 @[grind =]
@@ -308,7 +308,7 @@ abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
 @[simp, grind =] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
-  simp [List.find?_flatMap, Array.flatMap_toArray]
+  simp [List.find?_flatMap]
 
 theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
@@ -348,7 +348,7 @@ abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
-  simp [← List.toArray_replicate, List.find?_replicate_eq_none_iff, Classical.or_iff_not_imp_left]
+  simp [← List.toArray_replicate, Classical.or_iff_not_imp_left]
 
 @[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
 abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
@@ -488,7 +488,7 @@ theorem findIdx_push {xs : Array α} {a : α} {p : α → Bool} :
   simp only [push_eq_append, findIdx_append]
   split <;> rename_i h
   · rfl
-  · simp [findIdx_singleton, Nat.add_comm]
+  · simp [Nat.add_comm]
 
 theorem findIdx_le_findIdx {xs : Array α} {p q : α → Bool} (h : ∀ x ∈ xs, p x → q x) : xs.findIdx q ≤ xs.findIdx p := by
   rcases xs with ⟨xs⟩
@@ -553,7 +553,7 @@ theorem findIdx?_eq_some_of_exists {xs : Array α} {p : α → Bool} (h : ∃ x,
 theorem findIdx?_eq_none_iff_findIdx_eq {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = none ↔ xs.findIdx p = xs.size := by
   rcases xs with ⟨xs⟩
-  simp [List.findIdx?_eq_none_iff_findIdx_eq]
+  simp
 
 theorem findIdx?_eq_guard_findIdx_lt {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = Option.guard (fun i => i < xs.size) (xs.findIdx p) := by
@@ -798,7 +798,7 @@ The lemmas below should be made consistent with those for `findFinIdx?` (and pro
 
 theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
-  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
+  simp [idxOf?, finIdxOf?]
 
 @[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
 

@@ -109,19 +109,19 @@ theorem getElem_insertIdx {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.siz
         else
           xs[k-1]'(by simp [size_insertIdx] at h; omega) := by
   cases xs
-  simp [List.getElem_insertIdx, w]
+  simp [List.getElem_insertIdx]
 
 theorem getElem_insertIdx_of_lt {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < i) :
     (xs.insertIdx i x)[k]'(by simp; omega) = xs[k] := by
-  simp [getElem_insertIdx, w, h]
+  simp [getElem_insertIdx, h]
 
 theorem getElem_insertIdx_self {xs : Array α} {x : α} {i : Nat} (w : i ≤ xs.size) :
     (xs.insertIdx i x)[i]'(by simp; omega) = x := by
-  simp [getElem_insertIdx, w]
+  simp [getElem_insertIdx]
 
 theorem getElem_insertIdx_of_gt {xs : Array α} {x : α} {i k : Nat} (w : k ≤ xs.size) (h : k > i) :
     (xs.insertIdx i x)[k]'(by simp; omega) = xs[k - 1]'(by omega) := by
-  simp [getElem_insertIdx, w, h]
+  simp [getElem_insertIdx]
   rw [dif_neg (by omega), dif_neg (by omega)]
 
 @[grind =]
@@ -135,7 +135,7 @@ theorem getElem?_insertIdx {xs : Array α} {x : α} {i k : Nat} (h : i ≤ xs.si
         else
           xs[k-1]? := by
   cases xs
-  simp [List.getElem?_insertIdx, h]
+  simp [List.getElem?_insertIdx]
 
 theorem getElem?_insertIdx_of_lt {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < i) :
     (xs.insertIdx i x)[k]? = xs[k]? := by