chore: fix nonterminal simps (#7497)

Fixes the nonterminal simps identified by #7496

Mathlib/Algebra/Hom/Centroid.lean

@@ -395,7 +395,7 @@ instance : Semiring (CentroidHom α) :=
     toEnd_nat_cast
 
 theorem comp_mul_comm (T S : CentroidHom α) (a b : α) : (T ∘ S) (a * b) = (S ∘ T) (a * b) := by
-  simp
+  simp only [Function.comp_apply]
   rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]
 #align centroid_hom.comp_mul_comm CentroidHom.comp_mul_comm
 

Mathlib/Algebra/Homology/Single.lean

@@ -437,7 +437,7 @@ def fromSingle₀Equiv (C : CochainComplex V ℕ) (X : V) :
           simp
         · exact hf
         · rw [C.shape, comp_zero]
-          simp
+          simp only [Nat.zero_eq, ComplexShape.up_Rel, zero_add]
           exact j.succ_succ_ne_one.symm }
   left_inv f := by
     ext i

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -600,7 +600,8 @@ theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g
   refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_
   -- Porting note: `reducible` cannot be `local` so the proof gets more complex.
   unfold MonoidAlgebra
-  simp
+  simp only [AddMonoidHom.coe_comp, Function.comp_apply, singleAddHom_apply, smulAddHom_apply,
+    smul_single, smul_eq_mul, AddMonoidHom.coe_mulLeft]
   rw [liftNC_single, liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
 #align monoid_algebra.lift_nc_smul MonoidAlgebra.liftNC_smul
 
@@ -1117,7 +1118,9 @@ protected noncomputable def opRingEquiv [Monoid G] :
       refine AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₁ => AddMonoidHom.ext fun r₁ =>
         AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₂ => AddMonoidHom.ext fun r₂ => ?_
       -- Porting note: `reducible` cannot be `local` so proof gets long.
-      simp
+      simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, opAddEquiv_apply,
+        Function.comp_apply, singleAddHom_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.coe_mul,
+        AddMonoidHom.coe_mulLeft, AddMonoidHom.compl₂_apply]
       rw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply,
         AddEquiv.trans_apply, AddEquiv.trans_apply,
         MulOpposite.opAddEquiv_symm_apply, MulOpposite.unop_mul (α := MonoidAlgebra k G)]

Mathlib/Algebra/Order/Floor.lean

@@ -304,7 +304,7 @@ theorem le_ceil (a : α) : a ≤ ⌈a⌉₊ :=
 theorem ceil_intCast {α : Type*} [LinearOrderedRing α] [FloorSemiring α] (z : ℤ) :
     ⌈(z : α)⌉₊ = z.toNat :=
   eq_of_forall_ge_iff fun a => by
-    simp
+    simp only [ceil_le, Int.toNat_le]
     norm_cast
 #align nat.ceil_int_cast Nat.ceil_intCast
 

Mathlib/Algebra/Order/LatticeGroup.lean

@@ -276,7 +276,7 @@ theorem mul_inf_eq_mul_inf_mul [CovariantClass α α (· * ·) (· ≤ ·)] (a b
     c * (a ⊓ b) = c * a ⊓ c * b := by
   refine' le_antisymm _ _
   rw [le_inf_iff, mul_le_mul_iff_left, mul_le_mul_iff_left]
-  simp
+  simp only [inf_le_left, inf_le_right, and_self]
   rw [← mul_le_mul_iff_left c⁻¹, ← mul_assoc, inv_mul_self, one_mul, le_inf_iff,
     inv_mul_le_iff_le_mul, inv_mul_le_iff_le_mul]
   simp

Mathlib/Analysis/NormedSpace/AddTorsor.lean

@@ -298,7 +298,7 @@ def AffineMap.ofMapMidpoint (f : P → Q) (h : ∀ x y, f (midpoint ℝ x y) = m
   AffineMap.mk' f (↑((AddMonoidHom.ofMapMidpoint ℝ ℝ
     ((AffineEquiv.vaddConst ℝ (f <| c)).symm ∘ f ∘ AffineEquiv.vaddConst ℝ c) (by simp)
     fun x y => by -- Porting note: was `by simp [h]`
-      simp
+      simp only [Function.comp_apply, AffineEquiv.vaddConst_apply, AffineEquiv.vaddConst_symm_apply]
       conv_lhs => rw [(midpoint_self ℝ (Classical.arbitrary P)).symm, midpoint_vadd_midpoint, h, h,
           midpoint_vsub_midpoint]).toRealLinearMap <| by
         apply_rules [Continuous.vadd, Continuous.vsub, continuous_const, hfc.comp, continuous_id]))

Mathlib/Analysis/NormedSpace/Banach.lean

@@ -110,7 +110,7 @@ theorem exists_approx_preimage_norm_le (surj : Surjective f) :
       rw [← xz₁] at h₁
       rw [mem_ball, dist_eq_norm, sub_zero] at hx₁
       have : a ∈ ball a ε := by
-        simp
+        simp only [mem_ball, dist_self]
         exact εpos
       rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₂, z₂im, h₂⟩
       rcases(mem_image _ _ _).1 z₂im with ⟨x₂, hx₂, xz₂⟩

Mathlib/Analysis/NormedSpace/Multilinear.lean

@@ -215,7 +215,7 @@ theorem norm_image_sub_le_of_bound {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m
         · intro j _
           by_cases h : j = i
           · rw [h]
-            simp
+            simp only [ite_true, Function.update_same]
             exact norm_le_pi_norm (m₁ - m₂) i
           · simp [h, -le_max_iff, -max_le_iff, max_le_max, norm_le_pi_norm (_ : ∀ i, E i)]
       _ = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -269,7 +269,7 @@ theorem hasSum_geometric_two' (a : ℝ) : HasSum (fun n : ℕ => a / 2 / 2 ^ n)
   convert HasSum.mul_left (a / 2)
       (hasSum_geometric_of_lt_1 (le_of_lt one_half_pos) one_half_lt_one) using 1
   · funext n
-    simp
+    simp only [one_div, inv_pow]
     rfl
   · norm_num
 #align has_sum_geometric_two' hasSum_geometric_two'

Mathlib/CategoryTheory/Equivalence.lean

@@ -258,7 +258,7 @@ def adjointifyη : 𝟭 C ≅ F ⋙ G := by
 theorem adjointify_η_ε (X : C) :
     F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) := by
   dsimp [adjointifyη,Trans.trans]
-  simp
+  simp only [comp_id, assoc, map_comp]
   have := ε.hom.naturality (F.map (η.inv.app X)); dsimp at this; rw [this]; clear this
   rw [← assoc _ _ (F.map _)]
   have := ε.hom.naturality (ε.inv.app <| F.obj X); dsimp at this; rw [this]; clear this

Mathlib/CategoryTheory/Monoidal/Limits.lean

@@ -81,7 +81,9 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where
     dsimp; simp
   left_unitality X := by
     ext j; dsimp
-    simp
+    simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt,
+      Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj,
+      Monoidal.tensorUnit_obj, Monoidal.leftUnitor_hom_app]
     conv_rhs => rw [← tensor_id_comp_id_tensor (limit.π X j)]
     slice_rhs 1 2 =>
       rw [← comp_tensor_id]
@@ -91,7 +93,9 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where
     simp
   right_unitality X := by
     ext j; dsimp
-    simp
+    simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt,
+      Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj,
+      Monoidal.tensorUnit_obj, Monoidal.rightUnitor_hom_app]
     conv_rhs => rw [← id_tensor_comp_tensor_id _ (limit.π X j)]
     slice_rhs 1 2 =>
       rw [← id_tensor_comp]

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -380,7 +380,7 @@ variable {C}
 theorem one_associator {M N P : Mon_ C} :
     ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom =
       (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)) := by
-  simp
+  simp only [Category.assoc, Iso.cancel_iso_inv_left]
   slice_lhs 1 3 => rw [← Category.id_comp P.one, tensor_comp]
   slice_lhs 2 3 => rw [associator_naturality]
   slice_rhs 1 2 => rw [← Category.id_comp M.one, tensor_comp]
@@ -449,7 +449,7 @@ theorem mul_associator {M N P : Mon_ C} :
       ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
         tensor_μ C (M.X, N.X ⊗ P.X) (M.X, N.X ⊗ P.X) ≫
           (M.mul ⊗ tensor_μ C (N.X, P.X) (N.X, P.X) ≫ (N.mul ⊗ P.mul)) := by
-  simp
+  simp only [tensor_obj, prodMonoidal_tensorObj, Category.assoc]
   slice_lhs 2 3 => rw [← Category.id_comp P.mul, tensor_comp]
   slice_lhs 3 4 => rw [associator_naturality]
   slice_rhs 3 4 => rw [← Category.id_comp M.mul, tensor_comp]

Mathlib/Computability/Halting.lean

@@ -180,7 +180,7 @@ protected theorem not {p : α → Prop} (hp : ComputablePred p) : ComputablePred
   exact
     ⟨by infer_instance,
       (cond hf (const false) (const true)).of_eq fun n => by
-        simp
+        simp only [Bool.not_eq_true]
         cases f n <;> rfl⟩
 #align computable_pred.not ComputablePred.not
 
@@ -253,7 +253,8 @@ theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] :
           cases hy.1 hx.1)
       · refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _
         rw [hk]
-        simp
+        simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
+          Bool.true_eq_decide_iff, and_self, exists_const, Bool.false_eq_decide_iff]
         apply Decidable.em⟩⟩
 #align computable_pred.computable_iff_re_compl_re ComputablePred.computable_iff_re_compl_re
 

Mathlib/Computability/Partrec.lean

@@ -224,7 +224,8 @@ theorem ppred : Partrec fun n => ppred n :=
         eq_none_iff.2 fun a ⟨⟨m, h, _⟩, _⟩ => by
           simp [show 0 ≠ m.succ by intro h; injection h] at h
     · refine' eq_some_iff.2 _
-      simp
+      simp only [mem_rfind, not_true, IsEmpty.forall_iff, decide_True, mem_some_iff,
+        Bool.false_eq_decide_iff, true_and]
       intro m h
       simp [ne_of_gt h]
 #align nat.partrec.ppred Nat.Partrec.ppred

Mathlib/Computability/PartrecCode.lean

@@ -1125,7 +1125,7 @@ theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a
         rw [hg (Nat.pair_lt_pair_right _ lf)]
         cases n.unpair.2
         · rfl
-        simp
+        simp only [decode_eq_ofNat, Option.some.injEq]
         rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]
         cases evaln k' _ _
         · rfl
@@ -1134,7 +1134,7 @@ theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a
         rw [hg (Nat.pair_lt_pair_right _ lf)]
         cases' evaln k cf n with x
         · rfl
-        simp
+        simp only [decode_eq_ofNat, Option.some.injEq, Option.some_bind]
         cases x <;> simp [Nat.succ_ne_zero]
         rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]
   (Primrec.option_bind

Mathlib/Computability/Primrec.lean

@@ -343,7 +343,7 @@ theorem fst {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.fst α β
               (pair right ((@Primcodable.prim β).comp left)))).comp
         (pair right ((@Primcodable.prim α).comp left))).of_eq
     fun n => by
-    simp
+    simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
     cases @decode α _ n.unpair.1 <;> simp
     cases @decode β _ n.unpair.2 <;> simp
 #align primrec.fst Primrec.fst
@@ -354,7 +354,7 @@ theorem snd {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.snd α β
               (pair right ((@Primcodable.prim β).comp left)))).comp
         (pair right ((@Primcodable.prim α).comp left))).of_eq
     fun n => by
-    simp
+    simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
     cases @decode α _ n.unpair.1 <;> simp
     cases @decode β _ n.unpair.2 <;> simp
 #align primrec.snd Primrec.snd
@@ -568,7 +568,8 @@ theorem nat_rec {f : α → β} {g : α → ℕ × β → β} (hf : Primrec f) (
                 Nat.Primrec.right.pair <| Nat.Primrec.right.comp Nat.Primrec.left).comp <|
           Nat.Primrec.id.pair <| (@Primcodable.prim α).comp Nat.Primrec.left).of_eq
       fun n => by
-      simp
+      simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat,
+        Option.some_bind, Option.map_map, Option.map_some']
       cases' @decode α _ n.unpair.1 with a; · rfl
       simp [encodek]
       induction' n.unpair.2 with m <;> simp [encodek]
@@ -911,7 +912,7 @@ private theorem list_foldl' {f : α → List β} {g : α → σ} {h : α → σ
   generalize g a = x
   induction' n with n IH generalizing l x
   · rfl
-  simp
+  simp only [iterate_succ, comp_apply]
   cases' l with b l <;> simp [IH]
 
 private theorem list_cons' : (haveI := prim H; Primrec₂ (@List.cons β)) :=

Mathlib/Computability/TMToPartrec.lean

@@ -1356,7 +1356,7 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁
     · rw [Function.update_noteq h₁.symm]
       rfl
     refine' TransGen.head' rfl _
-    simp
+    simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq]
     revert e; cases' S k₁ with a Sk <;> intro e
     · cases e
       rfl
@@ -1366,7 +1366,7 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁
     · simp only [e]
       rfl
   · refine' TransGen.head rfl _
-    simp
+    simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq, List.reverseAux_cons]
     cases' e₁ : S k₁ with a' Sk <;> rw [e₁, splitAtPred] at e
     · cases e
     cases e₂ : p a' <;> simp only [e₂, cond] at e
@@ -1392,7 +1392,7 @@ theorem move₂_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k
     Reaches₁ (TM2.step tr) ⟨some (move₂ p k₁ k₂ q), s, S⟩
       ⟨some q, none, update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂)⟩ := by
   refine' (move_ok h₁.1 e).trans (TransGen.head rfl _)
-  simp
+  simp only [TM2.step, Option.mem_def, TM2.stepAux, id_eq, ne_eq, Option.elim]
   cases o <;> simp only [Option.elim, id.def]
   · simp only [TM2.stepAux, Option.isSome, cond_false]
     convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2
@@ -1414,7 +1414,7 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p
     Reaches₁ (TM2.step tr) ⟨some (Λ'.clear p k q), s, S⟩ ⟨some q, o, update S k L₂⟩ := by
   induction' L₁ with a L₁ IH generalizing S s
   · refine' TransGen.head' rfl _
-    simp
+    simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
     revert e; cases' S k with a Sk <;> intro e
     · cases e
       rfl
@@ -1424,7 +1424,7 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p
     · rcases e with ⟨e₁, e₂⟩
       rw [e₁, e₂]
   · refine' TransGen.head rfl _
-    simp
+    simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
     cases' e₁ : S k with a' Sk <;> rw [e₁, splitAtPred] at e
     · cases e
     cases e₂ : p a' <;> simp only [e₂, cond] at e
@@ -1444,7 +1444,9 @@ theorem copy_ok (q s a b c d) :
   · refine' TransGen.single _
     simp
   refine' TransGen.head rfl _
-  simp
+  simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
+    List.tail_cons, elim_update_rev, ne_eq, Function.update_noteq, elim_main, elim_update_main,
+    elim_stack, elim_update_stack, cond_true, List.reverseAux_cons]
   exact IH _ _ _
 #align turing.partrec_to_TM2.copy_ok Turing.PartrecToTM2.copy_ok
 
@@ -1483,7 +1485,8 @@ theorem head_main_ok {q s L} {c d : List Γ'} :
           (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) _)).trans
       (TransGen.head rfl (TransGen.head rfl _))
   · cases L <;> simp
-  simp
+  simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_update_main, elim_rev, elim_update_rev,
+    Function.update_same, trList]
   rw [if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp)]
   refine' (clear_ok (splitAtPred_eq _ _ _ none [] _ ⟨rfl, rfl⟩)).trans _
   · exact fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)
@@ -1500,7 +1503,9 @@ theorem head_stack_ok {q s L₁ L₂ L₃} :
         (move_ok (by decide)
           (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩))
         (TransGen.head rfl (TransGen.head rfl _))
-    simp
+    simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append,
+      elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_same,
+      List.headI_nil, trNat_default]
     convert unrev_ok using 2
     simp
   · refine'
@@ -1509,7 +1514,9 @@ theorem head_stack_ok {q s L₁ L₂ L₃} :
           (splitAtPred_eq _ _ (trNat a) (some Γ'.cons) (trList L₂ ++ Γ'.consₗ :: L₃)
             (trNat_natEnd _) ⟨rfl, by simp⟩))
         (TransGen.head rfl (TransGen.head rfl _))
-    simp
+    simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_false, trList, List.append_assoc,
+      List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_same,
+      List.headI_cons]
     refine'
       TransGen.trans
         (clear_ok
@@ -1526,9 +1533,11 @@ theorem succ_ok {q s n} {c d : List Γ'} :
   simp [trNat, Num.add_one]
   cases' (n : Num) with a
   · refine' TransGen.head rfl _
-    simp
+    simp only [Option.mem_def, TM2.stepAux, elim_main, decide_False, elim_update_main, ne_eq,
+      Function.update_noteq, elim_rev, elim_update_rev, decide_True, Function.update_same,
+      cond_true, cond_false]
     convert unrev_ok using 2
-    simp
+    simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main]
     rfl
   simp [Num.succ, trNum, Num.succ']
   suffices ∀ l₁, ∃ l₁' l₂' s',
@@ -1548,7 +1557,8 @@ theorem succ_ok {q s n} {c d : List Γ'} :
     simp [PosNum.succ, trPosNum]
     rfl
   · refine' ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single _⟩
-    simp
+    simp only [TM2.step, TM2.stepAux, elim_main, elim_update_main, ne_eq, Function.update_noteq,
+      elim_rev, elim_update_rev, Function.update_same, Option.mem_def, Option.some.injEq]
     rfl
 #align turing.partrec_to_TM2.succ_ok Turing.PartrecToTM2.succ_ok
 
@@ -1567,7 +1577,9 @@ theorem pred_ok (q₁ q₂ s v) (c d : List Γ') : ∃ s',
   cases' (n : Num) with a
   · simp [trPosNum, trNum, show Num.zero.succ' = PosNum.one from rfl]
     refine' TransGen.head rfl _
-    simp
+    simp only [Option.mem_def, TM2.stepAux, elim_main, List.head?_cons, Option.some.injEq,
+      decide_False, List.tail_cons, elim_update_main, ne_eq, Function.update_noteq, elim_rev,
+      elim_update_rev, natEnd, Function.update_same,  cond_true, cond_false]
     convert unrev_ok using 2
     simp
   simp [trNum, Num.succ']
@@ -1641,14 +1653,17 @@ theorem tr_ret_respects (k v s) : ∃ b₂,
     obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none
     refine' ⟨s', h₁, TransGen.head rfl _⟩; simp
     refine' (move₂_ok (by decide) _ (splitAtPred_false _)).trans _; · rfl
-    simp
+    simp only [TM2.step, Option.mem_def, Option.elim, id_eq, elim_update_main, elim_main, elim_aux,
+      List.append_nil, elim_update_aux]
     refine' (move₂_ok (by decide) _ _).trans _; pick_goal 4; · rfl
     pick_goal 4;
     · exact
         splitAtPred_eq _ _ _ (some Γ'.consₗ) _
           (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, rfl⟩
     refine' (move₂_ok (by decide) _ (splitAtPred_false _)).trans _; · rfl
-    simp
+    simp only [TM2.step, Option.mem_def, Option.elim, elim_update_stack, elim_main,
+      List.append_nil, elim_update_main,  id_eq, elim_update_aux, ne_eq, Function.update_noteq,
+      elim_aux, elim_stack]
     exact h₂
   case cons₂ ns k IH =>
     obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none
@@ -1734,13 +1749,13 @@ theorem trStmts₁_trans {q q'} : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trSt
   iterate 4 exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
   · simp
     intro s h x h'
-    simp
+    simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]
     exact Or.inr ⟨_, q_ih s h h'⟩
   · constructor
     · rintro rfl
       apply Finset.subset_insert
     · intro h x h'
-      simp
+      simp only [Finset.mem_insert]
       exact Or.inr (Or.inr <| q_ih h h')
   · refine' ⟨fun h x h' => _, fun _ x h' => _, fun h x h' => _⟩ <;> simp
     · exact Or.inr (Or.inr <| Or.inl <| q₁_ih h h')

Mathlib/Computability/TuringMachine.lean

@@ -1840,7 +1840,7 @@ theorem stepAux_read (f : Γ → Stmt'₁) (v : σ) (L R : ListBlank Γ) :
     stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
       (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))
   · dsimp [readAux, stepAux]
-    simp
+    simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]
     cases a <;> rfl
   rw [← ListBlank.append, IH]
   rfl