chore: remove nonterminal simp (#7580)

Removes nonterminal simps on lines looking like `simp [...]`

Mathlib/Algebra/Associated.lean

@@ -599,7 +599,7 @@ protected theorem Associated.prime [CommMonoidWithZero α] {p q : α} (h : p ~
     let ⟨u, hu⟩ := h
     ⟨fun ⟨v, hv⟩ => hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
       hu ▸ by
-        simp [Units.mul_right_dvd]
+        simp only [IsUnit.mul_iff, Units.isUnit, and_true, IsUnit.mul_right_dvd]
         intro a b
         exact hp.dvd_or_dvd⟩⟩
 #align associated.prime Associated.prime
@@ -832,8 +832,7 @@ instance instMul : Mul (Associates α) :=
     (Quotient.liftOn₂ a' b' fun a b => ⟦a * b⟧) fun a₁ a₂ b₁ b₂ ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ =>
       Quotient.sound <| ⟨c₁ * c₂, by
         rw [← h₁, ← h₂]
-        simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]
-        ⟩⟩
+        simp only [Units.val_mul, mul_left_comm, mul_comm]⟩⟩
 
 theorem mk_mul_mk {x y : α} : Associates.mk x * Associates.mk y = Associates.mk (x * y) :=
   rfl

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -253,7 +253,8 @@ theorem get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero {ifp_n : IntFract
     (of v).s.get? n = some ⟨1, (IntFractPair.of ifp_n.fr⁻¹).b⟩ :=
   have : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹) := by
     cases ifp_n
-    simp [IntFractPair.stream, stream_nth_eq, nth_fr_ne_zero]
+    simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind,
+      ite_eq_right_iff]
     intro; contradiction
   get?_of_eq_some_of_succ_get?_intFractPair_stream this
 #align generalized_continued_fraction.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero GeneralizedContinuedFraction.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero

Mathlib/Algebra/DirectSum/Ring.lean

@@ -643,7 +643,7 @@ def liftRingHom :
       rfl,
       by
       intros i j ai aj
-      simp [AddMonoidHom.comp_apply]
+      simp only [AddMonoidHom.comp_apply, AddMonoidHom.coe_coe]
       rw [← F.map_mul (of A i ai), of_mul_of ai]⟩
   left_inv f := by
     ext xi xv

Mathlib/Algebra/Group/Basic.lean

@@ -910,8 +910,7 @@ theorem eq_mul_of_div_eq' (h : a / b = c) : a = b * c := by simp [h.symm]
 
 @[to_additive]
 theorem mul_eq_of_eq_div' (h : b = c / a) : a * b = c := by
-  simp [h]
-  rw [mul_comm c, mul_inv_cancel_left]
+  rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]
 #align mul_eq_of_eq_div' mul_eq_of_eq_div'
 #align add_eq_of_eq_sub' add_eq_of_eq_sub'
 

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -167,7 +167,7 @@ set_option linter.deprecated false
 theorem zpow_bit0 (a : α) : ∀ n : ℤ, a ^ bit0 n = a ^ n * a ^ n
   | (n : ℕ) => by simp only [zpow_ofNat, ← Int.ofNat_bit0, pow_bit0]
   | -[n+1] => by
-    simp [← mul_inv_rev, ← pow_bit0]
+    simp only [zpow_negSucc, <-mul_inv_rev, <-pow_bit0]
     rw [negSucc_eq, bit0_neg, zpow_neg]
     norm_cast
 #align zpow_bit0 zpow_bit0

Mathlib/Algebra/Order/Field/Basic.lean

@@ -228,7 +228,7 @@ theorem inv_pos_lt_iff_one_lt_mul' (ha : 0 < a) : a⁻¹ < b ↔ 1 < a * b := by
 /-- One direction of `div_le_iff` where `b` is allowed to be `0` (but `c` must be nonnegative) -/
 theorem div_le_of_nonneg_of_le_mul (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a / b ≤ c := by
   rcases eq_or_lt_of_le hb with (rfl | hb')
-  simp [hc]
+  simp only [div_zero, hc]
   rwa [div_le_iff hb']
 #align div_le_of_nonneg_of_le_mul div_le_of_nonneg_of_le_mul
 

Mathlib/Algebra/Order/Floor.lean

@@ -1022,7 +1022,7 @@ theorem fract_fract (a : α) : fract (fract a) = fract a :=
 theorem fract_add (a b : α) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
   ⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by
     unfold fract
-    simp [sub_eq_add_neg]
+    simp only [sub_eq_add_neg, neg_add_rev, neg_neg, cast_add, cast_neg]
     abel⟩
 #align int.fract_add Int.fract_add
 

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -185,7 +185,7 @@ private theorem distrib' (a b c : WithTop α) : (a + b) * c = a * c + b * c := b
   · by_cases ha : a = 0 <;> simp [ha]
   · by_cases hc : c = 0
     · simp [hc]
-    simp [mul_coe hc]
+    simp only [mul_coe hc]
     cases a <;> cases b
     repeat' first | rfl |exact congr_arg some (add_mul _ _ _)
 

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -142,10 +142,14 @@ theorem leadingCoeff_multiset_prod' (h : (t.map leadingCoeff).prod ≠ 0) :
     t.prod.leadingCoeff = (t.map leadingCoeff).prod := by
   induction' t using Multiset.induction_on with a t ih; · simp
   simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢
-  rw [Polynomial.leadingCoeff_mul'] <;>
-    · rw [ih]
-      simp [*]
-      apply right_ne_zero_of_mul h
+  rw [Polynomial.leadingCoeff_mul']
+  · rw [ih]
+    simp only [ne_eq]
+    apply right_ne_zero_of_mul h
+  · rw [ih]
+    exact h
+    simp only [ne_eq, not_false_eq_true]
+    apply right_ne_zero_of_mul h
 #align polynomial.leading_coeff_multiset_prod' Polynomial.leadingCoeff_multiset_prod'
 
 /-- The leading coefficient of a product of polynomials is equal to

Mathlib/Algebra/QuaternionBasis.lean

@@ -119,7 +119,7 @@ theorem lift_one : q.lift (1 : ℍ[R,c₁,c₂]) = 1 := by simp [lift]
 #align quaternion_algebra.basis.lift_one QuaternionAlgebra.Basis.lift_one
 
 theorem lift_add (x y : ℍ[R,c₁,c₂]) : q.lift (x + y) = q.lift x + q.lift y := by
-  simp [lift, add_smul]
+  simp only [lift, add_re, map_add, add_imI, add_smul, add_imJ, add_imK]
   abel
 #align quaternion_algebra.basis.lift_add QuaternionAlgebra.Basis.lift_add
 
@@ -132,7 +132,7 @@ theorem lift_mul (x y : ℍ[R,c₁,c₂]) : q.lift (x * y) = q.lift x * q.lift y
   simp only [mul_comm _ c₁, mul_right_comm _ _ c₁]
   simp only [mul_comm _ c₂, mul_right_comm _ _ c₂]
   simp only [← mul_comm c₁ c₂, ← mul_assoc]
-  simp [sub_eq_add_neg, add_smul, ← add_assoc]
+  simp only [mul_re, sub_eq_add_neg, add_smul, neg_smul, mul_imI, ← add_assoc, mul_imJ, mul_imK]
   abel
 #align quaternion_algebra.basis.lift_mul QuaternionAlgebra.Basis.lift_mul
 

Mathlib/Algebra/RingQuot.lean

@@ -426,7 +426,7 @@ theorem mkRingHom_rel {r : R → R → Prop} {x y : R} (w : r x y) : mkRingHom r
 #align ring_quot.mk_ring_hom_rel RingQuot.mkRingHom_rel
 
 theorem mkRingHom_surjective (r : R → R → Prop) : Function.Surjective (mkRingHom r) := by
-  simp [mkRingHom_def]
+  simp only [mkRingHom_def, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
   rintro ⟨⟨⟩⟩
   simp
 #align ring_quot.mk_ring_hom_surjective RingQuot.mkRingHom_surjective

Mathlib/Algebra/Tropical/Lattice.lean

@@ -76,15 +76,15 @@ instance [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder
     csSup_of_not_bddAbove := by
       intro s hs
       have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
-      simp [sSup, this]
+      simp only [sSup, Set.image_empty, trop_inj_iff]
       apply csSup_of_not_bddAbove
       contrapose! hs
       change BddAbove (tropOrderIso.symm '' s) at hs
       exact tropOrderIso.symm.bddAbove_image.1 hs
     csInf_of_not_bddBelow := by
       intro s hs
       have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
-      simp [sInf, this]
+      simp only [sInf, Set.image_empty, trop_inj_iff]
       apply csInf_of_not_bddBelow
       contrapose! hs
       change BddBelow (tropOrderIso.symm '' s) at hs

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -261,7 +261,8 @@ theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.
   ext ⟨k, hk⟩
   simp at H hk
   dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
-  simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
+  simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le,
+    Fin.coe_castLT, dite_eq_ite, Fin.coe_castSucc, Fin.val_succ]
   split_ifs
   all_goals try simp <;> linarith
   all_goals cases k <;> simp at * <;> linarith
@@ -275,7 +276,8 @@ theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
   ext ⟨j, hj⟩
   simp at hj
   dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
-  simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
+  simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le,
+    Fin.coe_castLT, dite_eq_ite]
   split_ifs
   any_goals simp
   all_goals linarith
@@ -314,7 +316,8 @@ theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSu
   rcases j with ⟨j, hj⟩
   simp at H hk
   dsimp [δ, σ, Fin.predAbove, Fin.succAbove]
-  simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
+  simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le,
+    Fin.coe_castLT, dite_eq_ite, Fin.coe_castSucc, Fin.val_succ]
   split_ifs
   all_goals try simp <;> linarith
   all_goals cases k <;> simp at * <;> linarith
@@ -339,7 +342,8 @@ theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
   rcases j with ⟨j, hj⟩
   simp at H hk
   dsimp [σ, Fin.predAbove]
-  simp [Fin.lt_iff_val_lt_val, Fin.ite_val]
+  simp only [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, dite_eq_ite,
+    Fin.coe_castLT]
   split_ifs
   all_goals try linarith
   all_goals cases k <;> simp at *; linarith

Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean

@@ -65,7 +65,8 @@ theorem IsBoundedBilinearMap.hasStrictFDerivAt (h : IsBoundedBilinearMap 𝕜 b)
     _ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) := by
       ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
       rcases p with ⟨x, y⟩
-      simp [h.add_left, h.add_right, h.deriv_apply, h.map_sub_left, h.map_sub_right]
+      simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
+        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
       abel
     -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
     --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp

Mathlib/Analysis/Complex/Isometry.lean

@@ -155,7 +155,10 @@ theorem toMatrix_rotation (a : circle) :
     LinearMap.toMatrix basisOneI basisOneI (rotation a).toLinearEquiv =
       Matrix.planeConformalMatrix (re a) (im a) (by simp [pow_two, ← normSq_apply]) := by
   ext i j
-  simp [LinearMap.toMatrix_apply]
+  simp only [LinearMap.toMatrix_apply, coe_basisOneI, LinearEquiv.coe_coe,
+    LinearIsometryEquiv.coe_toLinearEquiv, rotation_apply, coe_basisOneI_repr, mul_re, mul_im,
+    Matrix.val_planeConformalMatrix, Matrix.of_apply, Matrix.cons_val', Matrix.empty_val',
+    Matrix.cons_val_fin_one]
   fin_cases i <;> fin_cases j <;> simp
 #align to_matrix_rotation toMatrix_rotation
 

Mathlib/Analysis/Convex/Between.lean

@@ -561,7 +561,7 @@ theorem Wbtw.sameRay_vsub {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x)
   rcases ht0.lt_or_eq with (ht0' | rfl); swap; · simp
   rcases ht1.lt_or_eq with (ht1' | rfl); swap; · simp
   refine' Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', _⟩)
-  simp [vsub_vadd_eq_vsub_sub, smul_sub, smul_smul, ← sub_smul]
+  simp only [vadd_vsub, smul_smul, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul]
   ring_nf
 #align wbtw.same_ray_vsub Wbtw.sameRay_vsub
 

Mathlib/Analysis/Normed/Order/UpperLower.lean

@@ -119,8 +119,8 @@ theorem IsUpperSet.exists_subset_ball (hs : IsUpperSet s) (hx : x ∈ closure s)
   refine' ⟨x + const _ (3 / 4 * δ), closedBall_subset_closedBall' _, _⟩
   · rw [dist_self_add_left]
     refine' (add_le_add_left (pi_norm_const_le <| 3 / 4 * δ) _).trans_eq _
-    simp [Real.norm_of_nonneg, hδ.le, zero_le_three]
-    simp [abs_of_pos, abs_of_pos hδ]
+    simp only [norm_mul, norm_div, Real.norm_eq_abs]
+    simp only [gt_iff_lt, zero_lt_three, abs_of_pos, zero_lt_four, abs_of_pos hδ]
     ring
   obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
   refine' fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => _
@@ -138,7 +138,8 @@ theorem IsLowerSet.exists_subset_ball (hs : IsLowerSet s) (hx : x ∈ closure s)
   refine' ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' _, _⟩
   · rw [dist_self_sub_left]
     refine' (add_le_add_left (pi_norm_const_le <| 3 / 4 * δ) _).trans_eq _
-    simp [abs_of_pos, abs_of_pos hδ]
+    simp only [norm_mul, norm_div, Real.norm_eq_abs, gt_iff_lt, zero_lt_three, abs_of_pos,
+      zero_lt_four, abs_of_pos hδ]
     ring
   obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
   refine' fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => _

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

@@ -253,7 +253,7 @@ theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear (g : G →L[𝕜
       apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
       exact Finset.prod_le_prod (fun i _ => norm_nonneg _) fun i _ => g.le_op_norm _
     _ = ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ i, ‖m i‖ := by
-      simp [Finset.prod_mul_distrib, Finset.card_univ]
+      simp only [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_univ]
       ring
 
 #align is_bounded_linear_map_continuous_multilinear_map_comp_linear isBoundedLinearMap_continuousMultilinearMap_comp_linear

Mathlib/Analysis/NormedSpace/Pointwise.lean

@@ -414,7 +414,9 @@ theorem NormedSpace.sphere_nonempty [Nontrivial E] {x : E} {r : ℝ} :
   refine' ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr =>
     ⟨r • ‖y - x‖⁻¹ • (y - x) + x, _⟩⟩
   have : ‖y - x‖ ≠ 0 := by simpa [sub_eq_zero]
-  simp [norm_smul, this, Real.norm_of_nonneg hr]
+  simp only [mem_sphere_iff_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, norm_inv, norm_norm,
+    ne_eq, norm_eq_zero]
+  simp only [abs_norm, ne_eq, norm_eq_zero]
   rw [inv_mul_cancel this, mul_one, abs_eq_self.mpr hr]
 #align normed_space.sphere_nonempty NormedSpace.sphere_nonempty
 

Mathlib/Analysis/NormedSpace/RieszLemma.lean

@@ -51,7 +51,7 @@ theorem riesz_lemma {F : Subspace 𝕜 E} (hFc : IsClosed (F : Set E)) (hF : ∃
         hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
     let r' := max r 2⁻¹
     have hr' : r' < 1 := by
-      simp [hr]
+      simp only [ge_iff_le, max_lt_iff, hr, true_and]
       norm_num
     have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹)
     have hdlt : d < d / r' := (lt_div_iff hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
@@ -101,7 +101,7 @@ theorem riesz_lemma_of_norm_lt {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖
     1 = ‖c‖ / R * (R / ‖c‖) := by field_simp [Rpos.ne', (zero_lt_one.trans hc).ne']
     _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
     _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
-      simp [norm_smul]
+      simp only [norm_smul]
       ring
     _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [Submodule.smul_mem _ _ hy])
     _ = ‖d • x - y‖ := by rw [yy', ←smul_sub, norm_smul]

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -524,7 +524,7 @@ def adjunctionOfEquivLeft : leftAdjointOfEquiv e he ⊣ G :=
       homEquiv_naturality_left_symm := fun {X'} {X} {Y} f g => by
         have := @he' C _ D _ G F_obj e he
         erw [← this, ← Equiv.apply_eq_iff_eq (e X' Y)]
-        simp [(he X' (F_obj X) Y (e X Y |>.symm g) (leftAdjointOfEquiv e he |>.map f)).symm]
+        simp only [leftAdjointOfEquiv_obj, Equiv.apply_symm_apply, assoc]
         congr
         rw [← he]
         simp

Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

@@ -326,7 +326,7 @@ lemma isZero₂_iff : IsZero T.obj₂ ↔ (T.mor₁ = 0 ∧ T.mor₂ = 0) := by
 lemma isZero₁_iff : IsZero T.obj₁ ↔ (T.mor₁ = 0 ∧ T.mor₃ = 0) := by
   refine' (isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans _
   dsimp
-  simp [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]
+  simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]
   tauto
 
 lemma isZero₃_iff : IsZero T.obj₃ ↔ (T.mor₂ = 0 ∧ T.mor₃ = 0) := by

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -2028,12 +2028,16 @@ def mapEdgeSet : G.edgeSet ≃ G'.edgeSet
   invFun := Hom.mapEdgeSet f.symm
   left_inv := by
     rintro ⟨e, h⟩
-    simp [Hom.mapEdgeSet, Sym2.map_map, RelEmbedding.toRelHom]
+    simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Embedding.toFun_eq_coe,
+      RelEmbedding.coe_toEmbedding, RelIso.coe_toRelEmbedding, Sym2.map_map, comp_apply,
+      Subtype.mk.injEq]
     convert congr_fun Sym2.map_id e
     exact RelIso.symm_apply_apply _ _
   right_inv := by
     rintro ⟨e, h⟩
-    simp [Hom.mapEdgeSet, Sym2.map_map, RelEmbedding.toRelHom]
+    simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Embedding.toFun_eq_coe,
+      RelEmbedding.coe_toEmbedding, RelIso.coe_toRelEmbedding, Sym2.map_map, comp_apply,
+      Subtype.mk.injEq]
     convert congr_fun Sym2.map_id e
     exact RelIso.apply_symm_apply _ _
 #align simple_graph.iso.map_edge_set SimpleGraph.Iso.mapEdgeSet

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -1612,7 +1612,8 @@ theorem map_isPath_of_injective (hinj : Function.Injective f) (hp : p.IsPath) :
   | nil => simp
   | cons _ _ ih =>
     rw [Walk.cons_isPath_iff] at hp
-    simp [ih hp.1]
+    simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
+      true_and]
     intro x hx hf
     cases hinj hf
     exact hp.2 hx

Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

@@ -157,7 +157,8 @@ theorem incMatrix_transpose_mul_diag [DecidableRel G.Adj] :
       refine' e.ind _
       intro v w h
       rw [← Nat.cast_two, ← card_doubleton (G.ne_of_adj h)]
-      simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h]
+      simp only [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h, true_and, mem_univ, forall_true_left,
+        forall_eq_or_imp, forall_eq, and_self, mem_singleton, ne_eq]
       congr 2
       ext u
       simp

Mathlib/Computability/Partrec.lean

@@ -568,7 +568,7 @@ theorem rfind {p : α → ℕ →. Bool} (hp : Partrec₂ p) : Partrec fun a =>
     fun n => by
     cases' e : decode (α := α) n with a <;> simp [e, Nat.rfind_zero_none, map_id']
     congr; funext n
-    simp [Part.map_map, (· ∘ ·)]
+    simp only [map_map, Function.comp]
     refine map_id' (fun b => ?_) _
     cases b <;> rfl
 #align partrec.rfind Partrec.rfind
@@ -607,7 +607,7 @@ theorem vector_mOfFn :
       (∀ i, Partrec (f i)) → Partrec fun a : α => Vector.mOfFn fun i => f i a
   | 0, _, _ => const _
   | n + 1, f, hf => by
-    simp [Vector.mOfFn]
+    simp only [Vector.mOfFn, Nat.add_eq, Nat.add_zero, pure_eq_some, bind_eq_bind]
     exact
       (hf 0).bind
         (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
@@ -744,7 +744,7 @@ theorem list_ofFn :
       (∀ i, Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
   | 0, _, _ => const []
   | n + 1, f, hf => by
-    simp [List.ofFn_succ]
+    simp only [List.ofFn_succ]
     exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)
 #align computable.list_of_fn Computable.list_ofFn