chore: squeeze some non-terminal simps (#11247)

This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!

Mathlib/Algebra/GradedMonoid.lean

@@ -446,7 +446,7 @@ theorem List.dProd_cons (fι : α → ι) (fA : ∀ a, A (fι a)) (a : α) (l :
 theorem GradedMonoid.mk_list_dProd (l : List α) (fι : α → ι) (fA : ∀ a, A (fι a)) :
     GradedMonoid.mk _ (l.dProd fι fA) = (l.map fun a => GradedMonoid.mk (fι a) (fA a)).prod := by
   match l with
-  | [] => simp; rfl
+  | [] => simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]; rfl
   | head::tail =>
     simp[← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
 #align graded_monoid.mk_list_dprod GradedMonoid.mk_list_dProd

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -223,12 +223,12 @@ instance (priority := 10) CancelMonoidWithZero.to_noZeroDivisors : NoZeroDivisor
 
 @[simp]
 theorem mul_eq_mul_right_iff : a * c = b * c ↔ a = b ∨ c = 0 := by
-  by_cases hc : c = 0 <;> [simp [hc]; simp [mul_left_inj', hc]]
+  by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]
 #align mul_eq_mul_right_iff mul_eq_mul_right_iff
 
 @[simp]
 theorem mul_eq_mul_left_iff : a * b = a * c ↔ b = c ∨ a = 0 := by
-  by_cases ha : a = 0 <;> [simp [ha]; simp [mul_right_inj', ha]]
+  by_cases ha : a = 0 <;> [simp only [ha, zero_mul, or_true]; simp [mul_right_inj', ha]]
 #align mul_eq_mul_left_iff mul_eq_mul_left_iff
 
 theorem mul_right_eq_self₀ : a * b = a ↔ b = 1 ∨ a = 0 :=

Mathlib/Algebra/Order/CauSeq/Completion.lean

@@ -263,7 +263,8 @@ protected theorem mul_inv_cancel {x : (Cauchy abv)} : x ≠ 0 → x * x⁻¹ = 1
 #align cau_seq.completion.mul_inv_cancel CauSeq.Completion.mul_inv_cancel
 
 theorem ofRat_inv (x : β) : ofRat x⁻¹ = ((ofRat x)⁻¹ : (Cauchy abv)) :=
-  congr_arg mk <| by split_ifs with h <;> [simp [const_limZero.1 h]; rfl]
+  congr_arg mk <| by split_ifs with h <;>
+    [simp only [const_limZero.1 h, GroupWithZero.inv_zero, const_zero]; rfl]
 #align cau_seq.completion.of_rat_inv CauSeq.Completion.ofRat_inv
 
 /- porting note: This takes a long time to compile.

Mathlib/Algebra/Order/Nonneg/Ring.lean

@@ -220,7 +220,7 @@ instance addMonoidWithOne [OrderedSemiring α] : AddMonoidWithOne { x : α // 0
     Nonneg.orderedAddCommMonoid with
     natCast := fun n => ⟨n, Nat.cast_nonneg n⟩
     natCast_zero := by simp
-    natCast_succ := fun _ => by simp; rfl }
+    natCast_succ := fun _ => by simp only [Nat.cast_add, Nat.cast_one]; rfl }
 #align nonneg.add_monoid_with_one Nonneg.addMonoidWithOne
 
 @[simp, norm_cast]

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -250,12 +250,12 @@ lemma mul_eq_bot_iff : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠
 #align with_bot.mul_eq_bot_iff WithBot.mul_eq_bot_iff
 
 lemma mul_coe_eq_bind {b : α} (hb : b ≠ 0) : ∀ a, (a * b : WithBot α) = a.bind fun a ↦ ↑(a * b)
-  | ⊥ => by simp [bot_mul, hb]; rfl
+  | ⊥ => by simp only [ne_eq, coe_eq_zero, hb, not_false_eq_true, bot_mul]; rfl
   | (a : α) => rfl
 #align with_bot.mul_coe WithBot.mul_coe_eq_bind
 
 lemma coe_mul_eq_bind {a : α} (ha : a ≠ 0) : ∀ b, (a * b : WithBot α) = b.bind fun b ↦ ↑(a * b)
-  | ⊥ => by simp [bot_mul, ha]; rfl
+  | ⊥ => by simp only [ne_eq, coe_eq_zero, ha, not_false_eq_true, mul_bot]; rfl
   | (b : α) => rfl
 
 @[simp]

Mathlib/Algebra/Ring/Divisibility/Basic.lean

@@ -77,15 +77,17 @@ variable [Semigroup α] [HasDistribNeg α] {a b c : α}
 @[simp]
 theorem dvd_neg : a ∣ -b ↔ a ∣ b :=
   -- Porting note: `simpa` doesn't close the goal with `rfl` anymore
-  (Equiv.neg _).exists_congr_left.trans <| by simp; rfl
+  (Equiv.neg _).exists_congr_left.trans <| by simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg,
+                                                neg_inj]; rfl
 #align dvd_neg dvd_neg
 
 /-- The negation of an element `a` of a semigroup with a distributive negation divides another
 element `b` iff `a` divides `b`. -/
 @[simp]
 theorem neg_dvd : -a ∣ b ↔ a ∣ b :=
   -- Porting note: `simpa` doesn't close the goal with `rfl` anymore
-  (Equiv.neg _).exists_congr_left.trans <| by simp; rfl
+  (Equiv.neg _).exists_congr_left.trans <| by simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg,
+                                                neg_mul, neg_neg]; rfl
 #align neg_dvd neg_dvd
 
 alias ⟨Dvd.dvd.of_neg_left, Dvd.dvd.neg_left⟩ := neg_dvd

Mathlib/Algebra/Tropical/Basic.lean

@@ -291,9 +291,11 @@ instance instLinearOrderTropical : LinearOrder (Tropical R) :=
     le_total := fun a b => le_total (untrop a) (untrop b)
     decidableLE := Tropical.decidableLE
     max := fun a b => trop (max (untrop a) (untrop b))
-    max_def := fun a b => untrop_injective (by simp [max_def]; split_ifs <;> simp)
+    max_def := fun a b => untrop_injective (by
+      simp only [max_def, untrop_le_iff, untrop_trop]; split_ifs <;> simp)
     min := (· + ·)
-    min_def := fun a b => untrop_injective (by simp [min_def]; split_ifs <;> simp) }
+    min_def := fun a b => untrop_injective (by
+      simp only [untrop_add, min_def, untrop_le_iff]; split_ifs <;> simp) }
 
 @[simp]
 theorem untrop_sup (x y : Tropical R) : untrop (x ⊔ y) = untrop x ⊔ untrop y :=

Mathlib/CategoryTheory/Adjunction/Reflective.lean

@@ -177,7 +177,9 @@ lemma equivEssImageOfReflective_map_counitIso_app_hom [Reflective i]
     (X : Functor.EssImageSubcategory i) :
   (Functor.essImageInclusion i).map (equivEssImageOfReflective_counitIso_app X).hom =
     inv (NatTrans.app (ofRightAdjoint i).unit X.obj) := by
-    simp [equivEssImageOfReflective_counitIso_app, asIso]
+    simp only [Functor.comp_obj, Functor.essImageInclusion_obj, Functor.toEssImage_obj_obj,
+      equivEssImageOfReflective_counitIso_app, asIso, Iso.symm_mk, Functor.essImageInclusion_map,
+      Functor.id_obj]
     rfl
 
 lemma equivEssImageOfReflective_map_counitIso_app_inv [Reflective i]

Mathlib/Control/Basic.lean

@@ -254,7 +254,7 @@ theorem CommApplicative.commutative_map {m : Type u → Type v} [h : Applicative
   f <$> a <*> b = flip f <$> b <*> a :=
   calc
     f <$> a <*> b = (fun p : α × β => f p.1 p.2) <$> (Prod.mk <$> a <*> b) := by
-      simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map]; rfl
+      simp only [map_seq, map_map]; rfl
     _ = (fun b a => f a b) <$> b <*> a := by
       rw [@CommApplicative.commutative_prod m h]
       simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map, (· ∘ ·)]

Mathlib/Control/Bitraversable/Instances.lean

@@ -103,7 +103,7 @@ instance (priority := 10) Bitraversable.isLawfulTraversable [LawfulBitraversable
     LawfulTraversable (t α) := by
   constructor <;> intros <;>
     simp [traverse, comp_tsnd, functor_norm]
-  · simp [tsnd_eq_snd_id]; rfl
+  · simp only [tsnd_eq_snd_id, Id.pure_eq]; rfl
   · simp [tsnd, binaturality, Function.comp, functor_norm]
 #align bitraversable.is_lawful_traversable Bitraversable.isLawfulTraversable
 
@@ -151,7 +151,7 @@ instance : Bitraversable (bicompr F t) where bitraverse := @Bicompr.bitraverse t
 instance [LawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (bicompr F t) := by
   constructor <;> intros <;>
     simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]
-  · simp [bitraverse_eq_bimap_id', traverse_eq_map_id']; rfl
+  · simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply, Id.pure_eq]; rfl
   · dsimp only [bicompr]
     simp [naturality, binaturality']
 

Mathlib/Control/EquivFunctor.lean

@@ -68,7 +68,7 @@ theorem mapEquiv_symm_apply (y : f β) : (mapEquiv f e).symm y = EquivFunctor.ma
 
 @[simp]
 theorem mapEquiv_refl (α) : mapEquiv f (Equiv.refl α) = Equiv.refl (f α) := by
- simp [EquivFunctor.mapEquiv]; rfl
+ simp only [mapEquiv, map_refl', Equiv.refl_symm]; rfl
 #align equiv_functor.map_equiv_refl EquivFunctor.mapEquiv_refl
 
 @[simp]

Mathlib/Control/Fold.lean

@@ -318,7 +318,8 @@ theorem foldr.ofFreeMonoid_comp_of (f : β → α → α) :
 theorem foldlm.ofFreeMonoid_comp_of {m} [Monad m] [LawfulMonad m] (f : α → β → m α) :
     foldlM.ofFreeMonoid f ∘ FreeMonoid.of = foldlM.mk ∘ flip f := by
   ext1 x
-  simp [(· ∘ ·), foldlM.ofFreeMonoid, foldlM.mk, flip]
+  simp only [foldlM.ofFreeMonoid, flip, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply,
+    FreeMonoid.toList_of, List.foldlM_cons, List.foldlM_nil, bind_pure, foldlM.mk, op_inj]
   rfl
 #align traversable.mfoldl.of_free_monoid_comp_of Traversable.foldlm.ofFreeMonoid_comp_of
 

Mathlib/Control/Functor.lean

@@ -203,7 +203,7 @@ variable [LawfulFunctor F] [LawfulFunctor G]
 variable {α β γ : Type v}
 
 protected theorem id_map : ∀ x : Comp F G α, Comp.map id x = x
-  | Comp.mk x => by simp [Comp.map, Functor.map_id]; rfl
+  | Comp.mk x => by simp only [Comp.map, id_map, id_map']; rfl
   -- Porting note: `rfl` wasn't needed in mathlib3
 #align functor.comp.id_map Functor.Comp.id_map
 

Mathlib/Control/Monad/Cont.lean

@@ -141,15 +141,15 @@ instance {ε} [MonadCont m] : MonadCont (ExceptT ε m) where
 
 instance {ε} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ExceptT ε m) where
   callCC_bind_right := by
-    intros; simp [callCC, ExceptT.callCC, callCC_bind_right]; ext
+    intros; simp only [callCC, ExceptT.callCC, ExceptT.run_bind, callCC_bind_right]; ext
     dsimp
     congr with ⟨⟩ <;> simp [ExceptT.bindCont, @callCC_dummy m _]
   callCC_bind_left := by
     intros
-    simp [callCC, ExceptT.callCC, callCC_bind_right, ExceptT.goto_mkLabel, map_eq_bind_pure_comp,
-      bind_assoc, @callCC_bind_left m _, Function.comp]
+    simp only [callCC, ExceptT.callCC, ExceptT.goto_mkLabel, map_eq_bind_pure_comp, Function.comp,
+      ExceptT.run_bind, ExceptT.run_mk, bind_assoc, pure_bind, @callCC_bind_left m _]
     ext; rfl
-  callCC_dummy := by intros; simp [callCC, ExceptT.callCC, @callCC_dummy m _]; ext; rfl
+  callCC_dummy := by intros; simp only [callCC, ExceptT.callCC, @callCC_dummy m _]; ext; rfl
 
 def OptionT.mkLabel {α β} : Label (Option.{u} α) m β → Label α (OptionT m) β
   | ⟨f⟩ => ⟨fun a => monadLift <| f (some a)⟩
@@ -170,15 +170,15 @@ instance [MonadCont m] : MonadCont (OptionT m) where
 
 instance [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (OptionT m) where
   callCC_bind_right := by
-    intros; simp [callCC, OptionT.callCC, callCC_bind_right]; ext
+    intros; simp only [callCC, OptionT.callCC, OptionT.run_bind, callCC_bind_right]; ext
     dsimp
     congr with ⟨⟩ <;> simp [@callCC_dummy m _]
   callCC_bind_left := by
     intros;
-    simp [callCC, OptionT.callCC, callCC_bind_right, OptionT.goto_mkLabel, map_eq_bind_pure_comp,
-      bind_assoc, @callCC_bind_left m _, Function.comp]
+    simp only [callCC, OptionT.callCC, OptionT.goto_mkLabel, OptionT.run_bind, OptionT.run_mk,
+      bind_assoc, pure_bind, @callCC_bind_left m _]
     ext; rfl
-  callCC_dummy := by intros; simp [callCC, OptionT.callCC, @callCC_dummy m _]; ext; rfl
+  callCC_dummy := by intros; simp only [callCC, OptionT.callCC, @callCC_dummy m _]; ext; rfl
 
 /- Porting note: In Lean 3, `One ω` is required for `MonadLift (WriterT ω m)`. In Lean 4,
                  `EmptyCollection ω` or `Monoid ω` is required. So we give definitions for the both
@@ -233,13 +233,14 @@ instance {σ} [MonadCont m] : MonadCont (StateT σ m) where
 instance {σ} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (StateT σ m) where
   callCC_bind_right := by
     intros
-    simp [callCC, StateT.callCC, callCC_bind_right]; ext; rfl
+    simp only [callCC, StateT.callCC, StateT.run_bind, callCC_bind_right]; ext; rfl
   callCC_bind_left := by
     intros;
-    simp [callCC, StateT.callCC, callCC_bind_left, StateT.goto_mkLabel]; ext; rfl
+    simp only [callCC, StateT.callCC, StateT.goto_mkLabel, StateT.run_bind, StateT.run_mk,
+      callCC_bind_left]; ext; rfl
   callCC_dummy := by
     intros;
-    simp [callCC, StateT.callCC, callCC_bind_right, @callCC_dummy m _]
+    simp only [callCC, StateT.callCC, @callCC_dummy m _]
     ext; rfl
 
 def ReaderT.mkLabel {α β} (ρ) : Label α m β → Label α (ReaderT ρ m) β
@@ -259,11 +260,13 @@ instance {ρ} [MonadCont m] : MonadCont (ReaderT ρ m) where
   callCC := ReaderT.callCC
 
 instance {ρ} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ReaderT ρ m) where
-  callCC_bind_right := by intros; simp [callCC, ReaderT.callCC, callCC_bind_right]; ext; rfl
+  callCC_bind_right := by intros; simp only [callCC, ReaderT.callCC, ReaderT.run_bind,
+                                    callCC_bind_right]; ext; rfl
   callCC_bind_left := by
-    intros; simp [callCC, ReaderT.callCC, callCC_bind_left, ReaderT.goto_mkLabel]
+    intros; simp only [callCC, ReaderT.callCC, ReaderT.goto_mkLabel, ReaderT.run_bind,
+      ReaderT.run_monadLift, monadLift_self, callCC_bind_left]
     ext; rfl
-  callCC_dummy := by intros; simp [callCC, ReaderT.callCC, @callCC_dummy m _]; ext; rfl
+  callCC_dummy := by intros; simp only [callCC, ReaderT.callCC, @callCC_dummy m _]; ext; rfl
 
 /-- reduce the equivalence between two continuation passing monads to the equivalence between
 their underlying monad -/

Mathlib/Control/Traversable/Equiv.lean

@@ -60,7 +60,7 @@ protected theorem id_map {α : Type u} (x : t' α) : Equiv.map eqv id x = x := b
 
 protected theorem comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : t' α) :
     Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x) := by
-  simp [Equiv.map]; apply comp_map
+  simpa [Equiv.map] using comp_map ..
 #align equiv.comp_map Equiv.comp_map
 
 protected theorem lawfulFunctor : @LawfulFunctor _ (Equiv.functor eqv) :=
@@ -140,7 +140,7 @@ protected theorem id_traverse (x : t' α) : Equiv.traverse eqv (pure : α → Id
 
 protected theorem traverse_eq_map_id (f : α → β) (x : t' α) :
     Equiv.traverse eqv ((pure : β → Id β) ∘ f) x = pure (Equiv.map eqv f x) := by
-  simp [Equiv.traverse, traverse_eq_map_id, functor_norm]; rfl
+  simp only [Equiv.traverse, traverse_eq_map_id, Id.map_eq, Id.pure_eq]; rfl
 #align equiv.traverse_eq_map_id Equiv.traverse_eq_map_id
 
 protected theorem comp_traverse (f : β → F γ) (g : α → G β) (x : t' α) :

Mathlib/Control/Traversable/Lemmas.lean

@@ -100,7 +100,7 @@ theorem id_sequence (x : t α) : sequence (f := Id) (pure <$> x) = pure x := by
 
 theorem comp_sequence (x : t (F (G α))) :
     sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x) := by
-  simp [sequence, traverse_map]; rw [← comp_traverse]; simp [map_id]
+  simp only [sequence, traverse_map, id_comp]; rw [← comp_traverse]; simp [map_id]
 #align traversable.comp_sequence Traversable.comp_sequence
 
 theorem naturality' (η : ApplicativeTransformation F G) (x : t (F α)) :

Mathlib/Data/Erased.lean

@@ -62,7 +62,7 @@ theorem out_mk {α} (a : α) : (mk a).out = a := by
 
 @[simp]
 theorem mk_out {α} : ∀ a : Erased α, mk (out a) = a
-  | ⟨s, h⟩ => by simp [mk]; congr; exact Classical.choose_spec h
+  | ⟨s, h⟩ => by simp only [mk]; congr; exact Classical.choose_spec h
 #align erased.mk_out Erased.mk_out
 
 @[ext]

Mathlib/Data/Int/Dvd/Basic.lean

@@ -21,7 +21,9 @@ namespace Int
 @[norm_cast]
 theorem coe_nat_dvd {m n : ℕ} : (↑m : ℤ) ∣ ↑n ↔ m ∣ n :=
   ⟨fun ⟨a, ae⟩ =>
-    m.eq_zero_or_pos.elim (fun m0 => by simp [m0] at ae; simp [ae, m0]) fun m0l => by
+    m.eq_zero_or_pos.elim (fun m0 => by
+      simp only [m0, Nat.cast_zero, zero_mul, cast_eq_zero] at ae
+      simp [ae, m0]) fun m0l => by
       cases'
         eq_ofNat_of_zero_le
           (@nonneg_of_mul_nonneg_right ℤ _ m a (by simp [ae.symm]) (by simpa using m0l)) with

Mathlib/Data/List/Basic.lean

@@ -1938,7 +1938,7 @@ theorem nthLe_take (L : List α) {i j : ℕ} (hi : i < L.length) (hj : i < j) :
 length `> i`. Version designed to rewrite from the small list to the big list. -/
 theorem get_take' (L : List α) {j i} :
     get (L.take j) i = get L ⟨i.1, lt_of_lt_of_le i.2 (by simp [le_refl])⟩ := by
-  let ⟨i, hi⟩ := i; simp at hi; rw [get_take L _ hi.1]
+  let ⟨i, hi⟩ := i; simp only [length_take, lt_min_iff] at hi; rw [get_take L _ hi.1]
 
 set_option linter.deprecated false in
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
@@ -3220,7 +3220,7 @@ theorem lookmap_map_eq (g : α → β) (h : ∀ (a), ∀ b ∈ f a, g a = g b) :
   | [] => rfl
   | a :: l => by
     cases' h' : f a with b
-    · simp [h']; exact lookmap_map_eq _ h l
+    · simpa [h'] using lookmap_map_eq _ h l
     · simp [lookmap_cons_some _ _ h', h _ _ h']
 #align list.lookmap_map_eq List.lookmap_map_eq
 
@@ -4207,7 +4207,10 @@ theorem forall_iff_forall_mem : ∀ {l : List α}, Forall p l ↔ ∀ x ∈ l, p
 
 theorem Forall.imp (h : ∀ x, p x → q x) : ∀ {l : List α}, Forall p l → Forall q l
   | [] => id
-  | x :: l => by simp; rw [← and_imp]; exact And.imp (h x) (Forall.imp h)
+  | x :: l => by
+    simp only [forall_cons, and_imp]
+    rw [← and_imp]
+    exact And.imp (h x) (Forall.imp h)
 #align list.all₂.imp List.Forall.imp
 
 @[simp]
@@ -4283,11 +4286,11 @@ theorem sizeOf_dropSlice_lt [SizeOf α] (i j : ℕ) (hj : 0 < j) (xs : List α)
         | cons _ xs_tl =>
           cases n
           · simp
-          · simp [drop]
+          · simp only [drop, cons.sizeOf_spec]
             rw [← Nat.zero_add (sizeOf (drop _ xs_tl))]
             exact Nat.add_le_add (Nat.zero_le _) (drop_sizeOf_le xs_tl _)
         · simp
-    · simp
+    · simp only [cons.sizeOf_spec, add_lt_add_iff_left]
       apply xs_ih _ j hj
       apply lt_of_succ_lt_succ hi
 #align list.sizeof_slice_lt List.sizeOf_dropSlice_lt

Mathlib/Data/List/Func.lean

@@ -103,8 +103,7 @@ theorem length_set : ∀ {m : ℕ} {as : List α}, as {m ↦ a}.length = max as.
   | 0, a :: as => by
     rw [max_eq_left]
     · rfl
-    · simp [Nat.le_add_right]
-      exact Nat.succ_le_succ (Nat.zero_le _)
+    · simpa [Nat.le_add_right] using Nat.succ_le_succ (Nat.zero_le _)
   | m + 1, [] => by
     simp [set, length, @length_set m, Nat.zero_max]
   | m + 1, _ :: as => by

Mathlib/Data/List/MinMax.lean

@@ -41,7 +41,8 @@ def argAux (a : Option α) (b : α) : Option α :=
 @[simp]
 theorem foldl_argAux_eq_none : l.foldl (argAux r) o = none ↔ l = [] ∧ o = none :=
   List.reverseRecOn l (by simp) fun tl hd => by
-    simp [argAux]; cases foldl (argAux r) o tl <;> simp; try split_ifs <;> simp
+    simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil, and_false, false_and,
+      iff_false]; cases foldl (argAux r) o tl <;> simp; try split_ifs <;> simp
 #align list.foldl_arg_aux_eq_none List.foldl_argAux_eq_none
 
 private theorem foldl_argAux_mem (l) : ∀ a m : α, m ∈ foldl (argAux r) (some a) l → m ∈ a :: l :=

Mathlib/Data/List/Palindrome.lean

@@ -49,7 +49,7 @@ variable {l : List α}
 
 theorem reverse_eq {l : List α} (p : Palindrome l) : reverse l = l := by
   induction p <;> try (exact rfl)
-  simp; assumption
+  simpa
 #align list.palindrome.reverse_eq List.Palindrome.reverse_eq
 
 theorem of_reverse_eq {l : List α} : reverse l = l → Palindrome l := by

Mathlib/Data/Multiset/Antidiagonal.lean

@@ -78,7 +78,7 @@ theorem antidiagonal_cons (a : α) (s) :
     simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
       map_coe, antidiagonal_coe', coe_add]
     rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
-    · congr; simp; rw [map_reverse]; simp
+    · congr; simp only [List.map_id]; rw [map_reverse]; simp
     · simp
 #align multiset.antidiagonal_cons Multiset.antidiagonal_cons
 

Mathlib/Data/Multiset/Pi.lean

@@ -88,7 +88,7 @@ def pi (m : Multiset α) (t : ∀ a, Multiset (β a)) : Multiset (∀ a ∈ m, 
       intro a a' m n
       by_cases eq : a = a'
       · subst eq; rfl
-      · simp [map_bind, bind_bind (t a') (t a)]
+      · simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]
         apply bind_hcongr
         · rw [cons_swap a a']
         intro b _
@@ -122,8 +122,8 @@ protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} :
   Multiset.induction_on s (fun _ _ => nodup_singleton _)
     (by
       intro a s ih hs ht
-      have has : a ∉ s := by simp at hs; exact hs.1
-      have hs : Nodup s := by simp at hs; exact hs.2
+      have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
+      have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
       simp only [pi_cons, nodup_bind]
       refine'
         ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),