chore: remove redundant simp annotations (#5251)

src/Init/ByCases.lean

@@ -37,20 +37,6 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
     f (ite P x y) = ite P (f x) (f y) :=
   apply_dite f P (fun _ => x) (fun _ => y)
 
-@[simp] theorem dite_eq_left_iff {P : Prop} [Decidable P] {B : ¬ P → α} :
-    dite P (fun _ => a) B = a ↔ ∀ h, B h = a := by
-  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
-
-@[simp] theorem dite_eq_right_iff {P : Prop} [Decidable P] {A : P → α} :
-    (dite P A fun _ => b) = b ↔ ∀ h, A h = b := by
-  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
-
-@[simp] theorem ite_eq_left_iff {P : Prop} [Decidable P] : ite P a b = a ↔ ¬P → b = a :=
-  dite_eq_left_iff
-
-@[simp] theorem ite_eq_right_iff {P : Prop} [Decidable P] : ite P a b = b ↔ P → a = b :=
-  dite_eq_right_iff
-
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
 @[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
 

src/Init/Data/Bool.lean

@@ -236,7 +236,7 @@ due to `beq_iff_eq`.
 @[simp] theorem bne_self_left  : ∀(a b : Bool), (a != (a != b)) = b := by decide
 @[simp] theorem bne_self_right : ∀(a b : Bool), ((a != b) != b) = a := by decide
 
-@[simp] theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
+theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by simp
 
 @[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
 instance : Std.Associative (· != ·) := ⟨bne_assoc⟩

src/Init/Data/Int/DivModLemmas.lean

@@ -1150,7 +1150,7 @@ theorem emod_bmod {x : Int} {m : Nat} : bmod (x % m) m = bmod x m := by
 
 @[simp] theorem bmod_zero : Int.bmod 0 m = 0 := by
   dsimp [bmod]
-  simp only [zero_emod, Int.zero_sub, ite_eq_left_iff, Int.neg_eq_zero]
+  simp only [Int.zero_sub, ite_eq_left_iff, Int.neg_eq_zero]
   intro h
   rw [@Int.not_lt] at h
   match m with

src/Init/Data/List/Nat/Range.lean

@@ -124,9 +124,8 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
       intro a a₁ a₂
       exact h₃ a a₁ (by omega)
 
-@[simp] theorem find?_range'_eq_none (s n : Nat) (p : Nat → Bool) :
+theorem find?_range'_eq_none (s n : Nat) (p : Nat → Bool) :
     (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i := by
-  rw [find?_eq_none]
   simp
 
 theorem erase_range' :
@@ -186,9 +185,9 @@ theorem nodup_range (n : Nat) : Nodup (range n) := by
     (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by
   simp [range_eq_range']
 
-@[simp] theorem find?_range_eq_none (n : Nat) (p : Nat → Bool) :
+theorem find?_range_eq_none (n : Nat) (p : Nat → Bool) :
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
-  simp [range_eq_range']
+  simp
 
 theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
   simp [range_eq_range', erase_range']
@@ -273,9 +272,8 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) :=
   rw [getLast_eq_head_reverse]
   simp
 
-@[simp] theorem find?_iota_eq_none (n : Nat) (p : Nat → Bool) :
+theorem find?_iota_eq_none (n : Nat) (p : Nat → Bool) :
     (iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i := by
-  rw [find?_eq_none]
   simp
 
 @[simp] theorem find?_iota_eq_some (n : Nat) (i : Nat) (p : Nat → Bool) :

src/Init/PropLemmas.lean

@@ -340,7 +340,7 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
 @[simp] theorem exists_prop' (p : Prop) : (∃ _ : α, p) ↔ Nonempty α ∧ p :=
   ⟨fun ⟨a, h⟩ => ⟨⟨a⟩, h⟩, fun ⟨⟨a⟩, h⟩ => ⟨a, h⟩⟩
 
-@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
+theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
   ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩
 
 @[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩
@@ -628,28 +628,28 @@ theorem ite_false_decide_same (p : Prop) [Decidable p] (b : Bool) :
 
 attribute [local simp] Decidable.imp_iff_left_iff
 
-@[simp] theorem dite_eq_then (p : Prop) [Decidable p] {x : α} {y : ¬ p → α} : (if h : p then x else y h) = x ↔ ∀ h : ¬ p, y h = x := by
+@[simp] theorem dite_eq_left_iff (p : Prop) [Decidable p] {x : α} {y : ¬ p → α} : (if h : p then x else y h) = x ↔ ∀ h : ¬ p, y h = x := by
   split <;> simp_all
 
-@[simp] theorem dite_eq_else (p : Prop) [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y := by
+@[simp] theorem dite_eq_right_iff (p : Prop) [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y := by
   split <;> simp_all
 
-@[simp] theorem dite_iff_then (p : Prop) [Decidable p] {x : Prop} {y : ¬ p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬ p, y h ↔ x := by
+@[simp] theorem dite_iff_left_iff (p : Prop) [Decidable p] {x : Prop} {y : ¬ p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬ p, y h ↔ x := by
   split <;> simp_all
 
-@[simp] theorem dite_iff_else (p : Prop) [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y := by
+@[simp] theorem dite_iff_right_iff (p : Prop) [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y := by
   split <;> simp_all
 
-@[simp] theorem ite_eq_then (p : Prop) [Decidable p] (x y : α) : (if p then x else y) = x ↔ ¬ p → y = x := by
+@[simp] theorem ite_eq_left_iff (p : Prop) [Decidable p] (x y : α) : (if p then x else y) = x ↔ ¬ p → y = x := by
   split <;> simp_all
 
-@[simp] theorem ite_eq_else (p : Prop) [Decidable p] (x y : α) : (if p then x else y) = y ↔ p → x = y := by
+@[simp] theorem ite_eq_right_iff (p : Prop) [Decidable p] (x y : α) : (if p then x else y) = y ↔ p → x = y := by
   split <;> simp_all
 
-@[simp] theorem ite_iff_then (p : Prop) [Decidable p] (x y : Prop) : ((if p then x else y) ↔ x) ↔ ¬ p → y = x := by
+@[simp] theorem ite_iff_left_iff (p : Prop) [Decidable p] (x y : Prop) : ((if p then x else y) ↔ x) ↔ ¬ p → y = x := by
   split <;> simp_all
 
-@[simp] theorem ite_iff_else (p : Prop) [Decidable p] (x y : Prop) : ((if p then x else y) ↔ y) ↔ p → x = y := by
+@[simp] theorem ite_iff_right_iff (p : Prop) [Decidable p] (x y : Prop) : ((if p then x else y) ↔ y) ↔ p → x = y := by
   split <;> simp_all
 
 @[simp] theorem dite_then_false (p : Prop) [Decidable p] {x : ¬ p → Prop} : (if h : p then False else x h) ↔ ∃ h : ¬ p, x h := by