chore: more squeeze_simps arising from linter (#11259)

The squeezing continues!  All found by the linter at #11246.

Mathlib/Algebra/Associated.lean

@@ -538,7 +538,7 @@ theorem Associated.mul_mul [CommMonoid α] {a₁ a₂ b₁ b₂ : α}
 
 theorem Associated.pow_pow [CommMonoid α] {a b : α} {n : ℕ} (h : a ~ᵤ b) : a ^ n ~ᵤ b ^ n := by
   induction' n with n ih
-  · simp [h]; rfl
+  · simp only [Nat.zero_eq, pow_zero]; rfl
   convert h.mul_mul ih <;> rw [pow_succ]
 #align associated.pow_pow Associated.pow_pow
 
@@ -998,7 +998,7 @@ theorem dvd_of_mk_le_mk {a b : α} : Associates.mk a ≤ Associates.mk b → a 
 #align associates.dvd_of_mk_le_mk Associates.dvd_of_mk_le_mk
 
 theorem mk_le_mk_of_dvd {a b : α} : a ∣ b → Associates.mk a ≤ Associates.mk b := fun ⟨c, hc⟩ =>
-  ⟨Associates.mk c, by simp [hc]; rfl⟩
+  ⟨Associates.mk c, by simp only [hc]; rfl⟩
 #align associates.mk_le_mk_of_dvd Associates.mk_le_mk_of_dvd
 
 theorem mk_le_mk_iff_dvd_iff {a b : α} : Associates.mk a ≤ Associates.mk b ↔ a ∣ b :=

Mathlib/Algebra/Group/Conj.lean

@@ -114,7 +114,7 @@ theorem conj_zpow {i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻
   induction' i
   · change (a * b * a⁻¹) ^ (_ : ℤ) = a * b ^ (_ : ℤ) * a⁻¹
     simp [zpow_coe_nat]
-  · simp [zpow_negSucc, conj_pow]
+  · simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
     rw [mul_assoc]
 -- Porting note: Added `change`, `zpow_coe_nat`, and `rw`.
 #align conj_zpow conj_zpow

Mathlib/Data/Fin/OrderHom.lean

@@ -478,8 +478,7 @@ theorem predAbove_right_monotone (p : Fin n) : Monotone p.predAbove := fun a b H
   · calc
       _ ≤ _ := Nat.pred_le _
       _ ≤ _ := H
-  · simp at ha
-    exact le_pred_of_lt (lt_of_le_of_lt ha hb)
+  · exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)
   · exact H
 #align fin.pred_above_right_monotone Fin.predAbove_right_monotone
 

Mathlib/Data/Int/Bitwise.lean

@@ -414,7 +414,8 @@ theorem shiftLeft_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<
         by dsimp; simp [← Nat.shiftLeft_sub _ , add_tsub_cancel_left])
       fun i n => by
         dsimp
-        simp [Nat.shiftLeft_zero, Nat.shiftRight_add, ← Nat.shiftLeft_sub]
+        simp only [Nat.shiftLeft'_false, Nat.shiftRight_add, le_refl, ← Nat.shiftLeft_sub,
+          tsub_eq_zero_of_le, Nat.shiftLeft_zero]
         rfl
   | -[m+1], n, -[k+1] =>
     subNatNat_elim n k.succ

Mathlib/Data/Int/Cast/Prod.lean

@@ -19,8 +19,9 @@ variable {α β : Type*} [AddGroupWithOne α] [AddGroupWithOne β]
 instance : AddGroupWithOne (α × β) :=
   { Prod.instAddMonoidWithOne, Prod.instAddGroup with
     intCast := fun n => (n, n)
-    intCast_ofNat := fun _ => by simp; rfl
-    intCast_negSucc := fun _ => by simp; rfl }
+    intCast_ofNat := fun _ => by simp only [Int.cast_ofNat]; rfl
+    intCast_negSucc := fun _ => by simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one,
+                                    neg_add_rev]; rfl }
 
 @[simp]
 theorem fst_intCast (n : ℤ) : (n : α × β).fst = n :=

Mathlib/Data/List/BigOperators/Basic.lean

@@ -562,8 +562,9 @@ theorem sum_le_foldr_max [AddMonoid M] [AddMonoid N] [LinearOrder N] (f : M →
 theorem prod_erase_of_comm [DecidableEq M] [Monoid M] {a} {l : List M} (ha : a ∈ l)
     (comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x) :
     a * (l.erase a).prod = l.prod := by
-  induction' l with b l ih; simp at ha
-  obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem ha; simp
+  induction' l with b l ih; simp only [not_mem_nil] at ha
+  obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem ha
+  simp only [erase_cons_head, prod_cons]
   rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
     comm a ha b (l.mem_cons_self b), mul_assoc,
     ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

Mathlib/Data/List/OfFn.lean

@@ -60,7 +60,7 @@ theorem get?_ofFn {n} (f : Fin n → α) (i) : get? (ofFn f) i = ofFnNthVal f i
   if h : i < (ofFn f).length
   then by
     rw [get?_eq_get h, get_ofFn]
-    · simp at h; simp [ofFnNthVal, h]
+    · simp only [length_ofFn] at h; simp [ofFnNthVal, h]
   else by
     rw [ofFnNthVal, dif_neg] <;>
     simpa using h

Mathlib/Data/List/Perm.lean

@@ -653,7 +653,7 @@ theorem perm_of_mem_permutationsAux :
   rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)
   · exact (IH1 _ m).trans perm_middle
   · have p : l₁ ++ l₂ ~ is := by
-      simp [permutations] at m
+      simp only [mem_cons] at m
       cases' m with e m
       · simp [e]
       exact is.append_nil ▸ IH2 _ m

Mathlib/Data/List/Permutation.lean

@@ -129,7 +129,10 @@ theorem map_map_permutationsAux2 {α α'} (g : α → α') (t : α) (ts ys : Lis
 
 theorem map_map_permutations'Aux (f : α → β) (t : α) (ts : List α) :
     map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts) := by
-  induction' ts with a ts ih <;> [rfl; (simp [← ih]; rfl)]
+  induction' ts with a ts ih
+  · rfl
+  · simp only [permutations'Aux, map_cons, map_map, ← ih, cons.injEq, true_and]
+    rfl
 #align list.map_map_permutations'_aux List.map_map_permutations'Aux
 
 theorem permutations'Aux_eq_permutationsAux2 (t : α) (ts : List α) :
@@ -175,7 +178,7 @@ theorem foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) :
       (L.bind fun y => (permutationsAux2 t ts [] y id).2) ++ r := by
   induction' L with l L ih
   · rfl
-  · simp [ih]
+  · simp only [foldr_cons, ih, cons_bind, append_assoc]
     rw [← permutationsAux2_append]
 #align list.foldr_permutations_aux2 List.foldr_permutationsAux2
 

Mathlib/Data/List/Sigma.lean

@@ -223,8 +223,7 @@ theorem map_dlookup_eq_find (a : α) :
     by_cases h : a = a'
     · subst a'
       simp
-    · simp [h]
-      exact map_dlookup_eq_find a l
+    · simpa [h] using map_dlookup_eq_find a l
 #align list.map_lookup_eq_find List.map_dlookup_eq_find
 
 theorem mem_dlookup_iff {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) :
@@ -433,7 +432,7 @@ theorem exists_of_kerase {a : α} {l : List (Sigma β)} (h : a ∈ l.keys) :
     by_cases e : a = hd.1
     · subst e
       exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩
-    · simp at h
+    · simp only [keys_cons, mem_cons] at h
       cases' h with h h
       exact absurd h e
       rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩
@@ -532,7 +531,9 @@ theorem kerase_append_left {a} :
 theorem kerase_append_right {a} :
     ∀ {l₁ l₂ : List (Sigma β)}, a ∉ l₁.keys → kerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂
   | [], _, _ => rfl
-  | _ :: l₁, l₂, h => by simp [not_or] at h; simp [h.1, kerase_append_right h.2]
+  | _ :: l₁, l₂, h => by
+    simp only [keys_cons, mem_cons, not_or] at h
+    simp [h.1, kerase_append_right h.2]
 #align list.kerase_append_right List.kerase_append_right
 
 theorem kerase_comm (a₁ a₂) (l : List (Sigma β)) :
@@ -616,7 +617,7 @@ theorem kextract_eq_dlookup_kerase (a : α) :
     ∀ l : List (Sigma β), kextract a l = (dlookup a l, kerase a l)
   | [] => rfl
   | ⟨a', b⟩ :: l => by
-    simp [kextract]; dsimp; split_ifs with h
+    simp only [kextract]; dsimp; split_ifs with h
     · subst a'
       simp [kerase]
     · simp [kextract, Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]
@@ -648,7 +649,7 @@ theorem nodupKeys_dedupKeys (l : List (Sigma β)) : NodupKeys (dedupKeys l) := b
   · cases x
     simp only [foldr_cons, kinsert_def, nodupKeys_cons, ne_eq, not_true]
     constructor
-    · simp [keys_kerase]
+    · simp only [keys_kerase]
       apply l_ih.not_mem_erase
     · exact l_ih.kerase _
 #align list.nodupkeys_dedupkeys List.nodupKeys_dedupKeys
@@ -763,7 +764,7 @@ theorem dlookup_kunion_right {a} {l₁ l₂ : List (Sigma β)} (h : a ∉ l₁.k
     dlookup a (kunion l₁ l₂) = dlookup a l₂ := by
   induction l₁ generalizing l₂ with
   | nil => simp
-  | cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]
+  | cons _ _ ih => simp_all [not_or]
 #align list.lookup_kunion_right List.dlookup_kunion_right
 
 -- Porting note: removing simp, LHS not in normal form, added new version

Mathlib/Data/List/Sublists.lean

@@ -305,8 +305,7 @@ theorem sublistsLen_sublist_of_sublist {α : Type*} (n) {l₁ l₂ : List α} (h
   · refine' IH.trans _
     rw [sublistsLen_succ_cons]
     apply sublist_append_left
-  · simp [sublistsLen_succ_cons]
-    exact IH.append ((IHn s).map _)
+  · simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)
 #align list.sublists_len_sublist_of_sublist List.sublistsLen_sublist_of_sublist
 
 theorem length_of_sublistsLen {α : Type*} :
@@ -456,10 +455,11 @@ theorem revzip_sublists (l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l
 theorem revzip_sublists' (l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l.sublists' → l₁ ++ l₂ ~ l := by
   rw [revzip]
   induction' l with a l IH <;> intro l₁ l₂ h
-  · simp at h
-    simp [h]
+  · simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
+      zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]
   · rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
-      <;> [simp at h; simp]
+      <;> [simp only [mem_append, mem_map, Prod_map, id_eq, Prod.mk.injEq, Prod.exists,
+        exists_eq_right_right] at h; simp]
     rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
     · exact perm_middle.trans ((IH _ _ h).cons _)
     · exact (IH _ _ h).cons _

Mathlib/Data/Rat/Order.lean

@@ -128,7 +128,7 @@ protected theorem le_iff_Nonneg (a b : ℚ) : a ≤ b ↔ Rat.Nonneg (b - a) :=
           apply mul_pos <;> rwa [pos_iff_ne_zero]
       · simp only [divInt_ofNat, ← zero_iff_num_zero, mkRat_eq_zero hb] at h'
         simp [h', Rat.Nonneg]
-      · simp [Rat.Nonneg, Rat.sub_def, normalize_eq]
+      · simp only [Rat.Nonneg, sub_def, normalize_eq]
         refine ⟨fun H => ?_, fun H _ => ?_⟩
         · refine Int.ediv_nonneg ?_ (Nat.cast_nonneg _)
           rw [sub_nonneg]

Mathlib/Data/Rel.lean

@@ -338,7 +338,7 @@ theorem core_id (s : Set α) : core (@Eq α) s = s := by simp [core]
 #align rel.core_id Rel.core_id
 
 theorem core_comp (s : Rel β γ) (t : Set γ) : core (r • s) t = core r (core s t) := by
-  ext x; simp [core, comp]; constructor
+  ext x; simp only [core, comp, forall_exists_index, and_imp, Set.mem_setOf_eq]; constructor
   · exact fun h y rxy z => h z y rxy
   · exact fun h z y rzy => h y rzy z
 #align rel.core_comp Rel.core_comp

Mathlib/Data/Seq/Computation.lean

@@ -310,8 +310,7 @@ theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s
         exact False.elim h
       · rw [destruct_pure, destruct_think] at h
         exact False.elim h
-      · simp at h
-        simp [*]
+      · simp_all
   · exact ⟨s₁, s₂, rfl, rfl, r⟩
 #align computation.eq_of_bisim Computation.eq_of_bisim
 
@@ -705,7 +704,7 @@ theorem destruct_map (f : α → β) (s) : destruct (map f s) = lmap f (rmap (ma
 @[simp]
 theorem map_id : ∀ s : Computation α, map id s = s
   | ⟨f, al⟩ => by
-    apply Subtype.eq; simp [map, Function.comp]
+    apply Subtype.eq; simp only [map, comp_apply, id_eq]
     have e : @Option.rec α (fun _ => Option α) none some = id := by ext ⟨⟩ <;> rfl
     have h : ((fun x: Option α => x) = id) := rfl
     simp [e, h, Stream'.map_id]

Mathlib/Data/Seq/Parallel.lean

@@ -102,7 +102,6 @@ theorem terminates_parallel.aux :
           (Sum.inr List.nil) l with a' ls <;> erw [e] at e'
         · contradiction
         have := IH' m _ e
-        simp [parallel.aux2] at e'
         -- Porting note: `revert e'` & `intro e'` are required.
         revert e'
         cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
@@ -135,7 +134,7 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
     have H : Seq.destruct S = some (some c, _) := by
       dsimp [Seq.destruct, (· <$> ·)]
       rw [← a]
-      simp
+      simp only [Option.map_some', Option.some.injEq]
       rfl
     induction' h : parallel.aux2 l with a l'
     · have C : corec parallel.aux1 (l, S) = pure a := by

Mathlib/Data/Seq/Seq.lean

@@ -775,8 +775,7 @@ theorem join_cons (a : α) (s S) : join (cons (a, s) S) = cons a (append s (join
       apply recOn s
       · simp [join_cons_cons, join_cons_nil]
       · intro x s
-        simp [join_cons_cons, join_cons_nil]
-        exact Or.inr ⟨x, s, S, rfl, rfl⟩
+        simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨x, s, S, rfl, rfl⟩
 #align stream.seq.join_cons Stream'.Seq.join_cons
 
 @[simp]
@@ -793,19 +792,19 @@ theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S)
           · apply recOn T
             · simp
             · intro s T
-              cases' s with a s; simp
+              cases' s with a s; simp only [join_cons, destruct_cons, true_and]
               refine' ⟨s, nil, T, _, _⟩ <;> simp
           · intro s S
-            cases' s with a s; simp
-            exact ⟨s, S, T, rfl, rfl⟩
+            cases' s with a s
+            simpa using ⟨s, S, T, rfl, rfl⟩
         · intro _ s
           exact ⟨s, S, T, rfl, rfl⟩
   · refine' ⟨nil, S, T, _, _⟩ <;> simp
 #align stream.seq.join_append Stream'.Seq.join_append
 
 @[simp]
 theorem ofStream_cons (a : α) (s) : ofStream (a::s) = cons a (ofStream s) := by
-  apply Subtype.eq; simp [ofStream, cons]; rw [Stream'.map_cons]
+  apply Subtype.eq; simp only [ofStream, cons]; rw [Stream'.map_cons]
 #align stream.seq.of_stream_cons Stream'.Seq.ofStream_cons
 
 @[simp]
@@ -991,8 +990,8 @@ theorem map_join' (f : α → β) (S) : Seq.map f (Seq.join S) = Seq.join (Seq.m
         apply recOn s <;> simp
         · apply recOn S <;> simp
           · intro x S
-            cases' x with a s; simp [map]
-            exact ⟨_, _, rfl, rfl⟩
+            cases' x with a s
+            simpa [map] using ⟨_, _, rfl, rfl⟩
         · intro _ s
           exact ⟨s, S, rfl, rfl⟩
   · refine' ⟨nil, S, _, _⟩ <;> simp
@@ -1017,7 +1016,8 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
         apply recOn s <;> simp
         · apply recOn SS <;> simp
           · intro S SS
-            cases' S with s S; cases' s with x s; simp [map]
+            cases' S with s S; cases' s with x s
+            simp only [Seq.join_cons, join_append, destruct_cons]
             apply recOn s <;> simp
             · exact ⟨_, _, rfl, rfl⟩
             · intro x s