Trigger CI for leanprover/lean4#3082

Mathlib/Algebra/Associated.lean

@@ -230,9 +230,11 @@ theorem irreducible_or_factor {α} [Monoid α] (x : α) (h : ¬IsUnit x) :
     Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x := by
   haveI := Classical.dec
   refine' or_iff_not_imp_right.2 fun H => _
-  simp [h, irreducible_iff] at H ⊢
+  simp? [h, irreducible_iff] at H ⊢ says
+    simp only [exists_and_left, not_exists, not_and, irreducible_iff, h, not_false_eq_true,
+      true_and] at H ⊢
   refine' fun a b h => by_contradiction fun o => _
-  simp [not_or] at o
+  simp? [not_or] at o says simp only [not_or] at o
   exact H _ o.1 _ o.2 h.symm
 #align irreducible_or_factor irreducible_or_factor
 
@@ -324,7 +326,7 @@ protected theorem Prime.irreducible (hp : Prime p) : Irreducible p :=
           (isUnit_iff_dvd_one.2
             ⟨x,
               mul_right_cancel₀ (show a ≠ 0 from fun h => by
-                simp [Prime] at *
+                simp only [Prime, ne_eq, IsUnit.mul_iff] at *
                 rw [h, zero_mul] at hab
                 have := hp.left
                 contradiction
@@ -339,7 +341,7 @@ protected theorem Prime.irreducible (hp : Prime p) : Irreducible p :=
         (isUnit_iff_dvd_one.2
           ⟨x,
             mul_right_cancel₀ (show b ≠ 0 from fun h => by
-            simp [Prime] at *
+            simp only [Prime, ne_eq, IsUnit.mul_iff] at *
             rw [h, mul_zero] at hab
             have := hp.left
             contradiction

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -120,7 +120,7 @@ theorem colimitMulAux_eq_of_rel_left {x x' y : Σ j, F.obj j}
     colimitMulAux.{v, u} F x y = colimitMulAux.{v, u} F x' y := by
   cases' x with j₁ x; cases' y with j₂ y; cases' x' with j₃ x'
   obtain ⟨l, f, g, hfg⟩ := hxx'
-  simp at hfg
+  simp? at hfg says simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg
   obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
     IsFiltered.tulip (IsFiltered.leftToMax j₁ j₂) (IsFiltered.rightToMax j₁ j₂)
       (IsFiltered.rightToMax j₃ j₂) (IsFiltered.leftToMax j₃ j₂) f g
@@ -145,7 +145,7 @@ theorem colimitMulAux_eq_of_rel_right {x y y' : Σ j, F.obj j}
     colimitMulAux.{v, u} F x y = colimitMulAux.{v, u} F x y' := by
   cases' y with j₁ y; cases' x with j₂ x; cases' y' with j₃ y'
   obtain ⟨l, f, g, hfg⟩ := hyy'
-  simp at hfg
+  simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg
   obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
     IsFiltered.tulip (IsFiltered.rightToMax j₂ j₁) (IsFiltered.leftToMax j₂ j₁)
       (IsFiltered.leftToMax j₂ j₃) (IsFiltered.rightToMax j₂ j₃) f g

Mathlib/Algebra/Group/Freiman.lean

@@ -495,7 +495,8 @@ theorem map_prod_eq_map_prod_of_le [FreimanHomClass F A β n] (f : F) {s t : Mul
   obtain rfl | hm := m.eq_zero_or_pos
   · rw [card_eq_zero] at hs ht
     rw [hs, ht]
-  simp [← hs, card_pos_iff_exists_mem] at hm
+  simp? [← hs, card_pos_iff_exists_mem] at hm says
+    simp only [← hs, gt_iff_lt, card_pos_iff_exists_mem] at hm
   obtain ⟨a, ha⟩ := hm
   suffices
     ((s + Multiset.replicate (n - m) a).map f).prod =

Mathlib/Algebra/Homology/Augment.lean

@@ -237,7 +237,7 @@ def augment (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d
     | i + 1, j + 1 => C.d i j
     | _, _ => 0
   shape i j s := by
-    simp at s
+    simp? at s says simp only [ComplexShape.up_Rel] at s
     rcases j with (_ | _ | j) <;> cases i <;> try simp
     · contradiction
     · rw [C.shape]

Mathlib/Algebra/Lie/DirectSum.lean

@@ -170,7 +170,7 @@ def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
         -- with `simp [of, singleAddHom]`
         simp only [of, singleAddHom, bracket_apply]
         erw [AddHom.coe_mk, single_apply, single_apply]
-        simp [h]
+        simp? [h] says simp only [h, dite_eq_ite, ite_true, single_apply]
         intros
         erw [single_add]
       · -- This used to be the end of the proof before leanprover/lean4#2644

Mathlib/Algebra/RingQuot.lean

@@ -195,7 +195,7 @@ private irreducible_def npow (n : ℕ) : RingQuot r → RingQuot r
             -- mysteriously doesn't work
             have := congr_arg₂ (fun x y ↦ mul r ⟨x⟩ ⟨y⟩) (Quot.sound h) ih
             dsimp only at this
-            simp [mul_def] at this
+            simp? [mul_def] at this says simp only [mul_def, Quot.map₂_mk, mk.injEq] at this
             exact this)
         a⟩
 

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -259,7 +259,7 @@ theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.
   rcases i with ⟨i, hi⟩
   rcases j with ⟨j, hj⟩
   ext ⟨k, hk⟩
-  simp at H hk
+  simp? at H hk says simp only [Fin.castSucc_mk, Fin.mk_le_mk, len_mk] at H hk
   dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
   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]
@@ -274,7 +274,7 @@ theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
     δ (Fin.castSucc i) ≫ σ i = 𝟙 ([n] : SimplexCategory) := by
   rcases i with ⟨i, hi⟩
   ext ⟨j, hj⟩
-  simp at hj
+  simp? at hj says simp only [len_mk] at hj
   dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
   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]
@@ -314,7 +314,7 @@ theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSu
   ext ⟨k, hk⟩
   rcases i with ⟨i, hi⟩
   rcases j with ⟨j, hj⟩
-  simp at H hk
+  simp? at H hk says simp only [Fin.castSucc_mk, Fin.mk_lt_mk, len_mk] at H hk
   dsimp [δ, σ, Fin.predAbove, Fin.succAbove]
   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]
@@ -340,7 +340,7 @@ theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
   ext ⟨k, hk⟩
   rcases i with ⟨i, hi⟩
   rcases j with ⟨j, hj⟩
-  simp at H hk
+  simp? at H hk says simp only [Fin.mk_le_mk, len_mk] at H hk
   dsimp [σ, Fin.predAbove]
   simp only [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, dite_eq_ite,
     Fin.coe_castLT]

Mathlib/Analysis/Convex/Function.lean

@@ -834,7 +834,9 @@ theorem neg_convexOn_iff : ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f := by
   constructor
   · rintro ⟨hconv, h⟩
     refine' ⟨hconv, fun x hx y hy a b ha hb hab => _⟩
-    simp [neg_apply, neg_le, add_comm] at h
+    simp? [neg_apply, neg_le, add_comm] at h says
+      simp only [Pi.neg_apply, smul_neg, le_add_neg_iff_add_le, add_comm,
+        add_neg_le_iff_le_add] at h
     exact h hx hy ha hb hab
   · rintro ⟨hconv, h⟩
     refine' ⟨hconv, fun x hx y hy a b ha hb hab => _⟩
@@ -855,7 +857,8 @@ theorem neg_strictConvexOn_iff : StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn
   constructor
   · rintro ⟨hconv, h⟩
     refine' ⟨hconv, fun x hx y hy hxy a b ha hb hab => _⟩
-    simp [neg_apply, neg_lt, add_comm] at h
+    simp only [ne_eq, Pi.neg_apply, smul_neg, lt_add_neg_iff_add_lt, add_comm,
+      add_neg_lt_iff_lt_add] at h
     exact h hx hy hxy ha hb hab
   · rintro ⟨hconv, h⟩
     refine' ⟨hconv, fun x hx y hy hxy a b ha hb hab => _⟩

Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean

@@ -61,7 +61,7 @@ theorem Finset.prod_nonneg_of_card_nonpos_even {α β : Type*} [LinearOrderedCom
       Finset.prod_nonneg fun x _ => by
         split_ifs with hx
         · simp [hx]
-        simp at hx ⊢
+        simp? at hx ⊢ says simp only [not_le, one_mul] at hx ⊢
         exact le_of_lt hx
     _ = _ := by
       rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -726,13 +726,13 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
         skip
         have A := hF (Function.update v i (x + y))
         have B := (hF (Function.update v i x)).add (hF (Function.update v i y))
-        simp at A B
+        simp? at A B says simp only [map_add] at A B
         exact tendsto_nhds_unique A B
       map_smul' := fun v i c x => by
         skip
         have A := hF (Function.update v i (c • x))
         have B := Filter.Tendsto.smul (@tendsto_const_nhds _ ℕ _ c _) (hF (Function.update v i x))
-        simp at A B
+        simp? at A B says simp only [map_smul] at A B
         exact tendsto_nhds_unique A B }
   -- and that `F` has norm at most `(b 0 + ‖f 0‖)`.
   have Fnorm : ∀ v, ‖F v‖ ≤ (b 0 + ‖f 0‖) * ∏ i, ‖v i‖ := by

Mathlib/Analysis/SpecialFunctions/Bernstein.lean

@@ -108,7 +108,8 @@ local postfix:90 "/ₙ" => z
 theorem probability (n : ℕ) (x : I) : (∑ k : Fin (n + 1), bernstein n k x) = 1 := by
   have := bernsteinPolynomial.sum ℝ n
   apply_fun fun p => Polynomial.aeval (x : ℝ) p at this
-  simp [AlgHom.map_sum, Finset.sum_range] at this
+  simp? [AlgHom.map_sum, Finset.sum_range] at this says
+    simp only [Finset.sum_range, map_sum, Polynomial.coe_aeval_eq_eval, map_one] at this
   exact this
 #align bernstein.probability bernstein.probability
 
@@ -122,7 +123,9 @@ theorem variance {n : ℕ} (h : 0 < (n : ℝ)) (x : I) :
   conv_rhs => rw [div_mul_cancel _ h']
   have := bernsteinPolynomial.variance ℝ n
   apply_fun fun p => Polynomial.aeval (x : ℝ) p at this
-  simp [AlgHom.map_sum, Finset.sum_range, ← Polynomial.nat_cast_mul] at this
+  simp? [AlgHom.map_sum, Finset.sum_range, ← Polynomial.nat_cast_mul] at this says
+    simp only [nsmul_eq_mul, Finset.sum_range, map_sum, map_mul, map_pow, map_sub, map_natCast,
+      Polynomial.aeval_X, Polynomial.coe_aeval_eq_eval, map_one] at this
   convert this using 1
   · congr 1; funext k
     rw [mul_comm _ (n : ℝ), mul_comm _ (n : ℝ), ← mul_assoc, ← mul_assoc]

Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

@@ -94,7 +94,9 @@ theorem betaIntegral_symm (u v : ℂ) : betaIntegral v u = betaIntegral u v := b
   have := intervalIntegral.integral_comp_mul_add (a := 0) (b := 1) (c := -1)
     (fun x : ℝ => (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1)) neg_one_lt_zero.ne 1
   rw [inv_neg, inv_one, neg_one_smul, ← intervalIntegral.integral_symm] at this
-  simp at this
+  simp? at this says
+    simp only [neg_mul, one_mul, ofReal_add, ofReal_neg, ofReal_one, sub_add_cancel'', neg_neg,
+      mul_one, add_left_neg, mul_zero, zero_add] at this
   conv_lhs at this => arg 1; intro x; rw [add_comm, ← sub_eq_add_neg, mul_comm]
   exact this
 #align complex.beta_integral_symm Complex.betaIntegral_symm

Mathlib/CategoryTheory/Abelian/Transfer.lean

@@ -57,7 +57,8 @@ variable (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F)
 theorem hasKernels [PreservesFiniteLimits G] : HasKernels C :=
   { has_limit := fun f => by
       have := NatIso.naturality_1 i f
-      simp at this
+      simp? at this says
+        simp only [Functor.id_obj, Functor.comp_obj, Functor.comp_map, Functor.id_map] at this
       rw [← this]
       haveI : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
       apply Limits.hasKernel_iso_comp }
@@ -68,7 +69,8 @@ theorem hasCokernels : HasCokernels C :=
   { has_colimit := fun f => by
       have : PreservesColimits G := adj.leftAdjointPreservesColimits
       have := NatIso.naturality_1 i f
-      simp at this
+      simp? at this says
+        simp only [Functor.id_obj, Functor.comp_obj, Functor.comp_map, Functor.id_map] at this
       rw [← this]
       haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
       apply Limits.hasCokernel_epi_comp }

Mathlib/CategoryTheory/GradedObject.lean

@@ -255,7 +255,7 @@ instance : Faithful (total β C) where
     ext i
     replace w := Sigma.ι (fun i : β => X i) i ≫= w
     erw [colimit.ι_map, colimit.ι_map] at w
-    simp at *
+    simp? at * says simp only [Discrete.functor_obj, Discrete.natTrans_app] at *
     exact Mono.right_cancellation _ _ w
 
 end GradedObject

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

@@ -76,7 +76,9 @@ theorem colimitLimitToLimitColimit_injective :
     replace h := fun j => congr_arg (limit.π (curry.obj F ⋙ colim) j) h
     -- and they are equations in a filtered colimit,
     -- so for each `j` we have some place `k j` to the right of both `kx` and `ky`
-    simp [colimit_eq_iff.{v, v}] at h
+    simp? [colimit_eq_iff.{v, v}] at h says
+      simp only [Functor.comp_obj, colim_obj, ι_colimitLimitToLimitColimit_π_apply,
+        colimit_eq_iff.{v, v}, curry_obj_obj_obj, curry_obj_obj_map] at h
     let k j := (h j).choose
     let f : ∀ j, kx ⟶ k j := fun j => (h j).choose_spec.choose
     let g : ∀ j, ky ⟶ k j := fun j => (h j).choose_spec.choose_spec.choose

Mathlib/CategoryTheory/Limits/Shapes/Images.lean

@@ -109,7 +109,7 @@ theorem ext {F F' : MonoFactorisation f} (hI : F.I = F'.I)
     (hm : F.m = eqToHom hI ≫ F'.m) : F = F' := by
   cases' F with _ Fm _ _ Ffac; cases' F' with _ Fm' _ _ Ffac'
   cases' hI
-  simp at hm
+  simp? at hm says simp only [eqToHom_refl, Category.id_comp] at hm
   congr
   · apply (cancel_mono Fm).1
     rw [Ffac, hm, Ffac']

Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean

@@ -52,7 +52,8 @@ def pullback_of_mono {X Y Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [Mono a] [Mono b] :
   HasLimit.mk
     { cone :=
         PullbackCone.mk a' b' <| by
-          simp at ha' hb'
+          simp? at ha' hb' says
+            simp only [parallelPair_obj_zero, Fork.ofι_pt, Fork.ι_ofι] at ha' hb'
           rw [ha', hb']
       isLimit :=
         PullbackCone.IsLimit.mk _

Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean

@@ -152,11 +152,15 @@ def IsLimit.assoc {X Y Z : C} {sXY : BinaryFan X Y} (P : IsLimit sXY) {sYZ : Bin
     rintro ⟨⟨⟩⟩ <;> simp
     · exact w ⟨WalkingPair.left⟩
     · specialize w ⟨WalkingPair.right⟩
-      simp at w
+      simp? at w says
+        simp only [pair_obj_right, BinaryFan.π_app_right, BinaryFan.assoc_snd,
+          Functor.const_obj_obj, pair_obj_left] at w
       rw [← w]
       simp
     · specialize w ⟨WalkingPair.right⟩
-      simp at w
+      simp? at w says
+        simp only [pair_obj_right, BinaryFan.π_app_right, BinaryFan.assoc_snd,
+          Functor.const_obj_obj, pair_obj_left] at w
       rw [← w]
       simp
 #align category_theory.limits.is_limit.assoc CategoryTheory.Limits.IsLimit.assoc

Mathlib/CategoryTheory/Products/Basic.lean

@@ -66,7 +66,7 @@ theorem isIso_prod_iff {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} :
     IsIso f ↔ IsIso f.1 ∧ IsIso f.2 := by
   constructor
   · rintro ⟨g, hfg, hgf⟩
-    simp at hfg hgf
+    simp? at hfg hgf says simp only [prod_Hom, prod_comp, prod_id, Prod.mk.injEq] at hfg hgf
     rcases hfg with ⟨hfg₁, hfg₂⟩
     rcases hgf with ⟨hgf₁, hgf₂⟩
     exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩

Mathlib/Combinatorics/Composition.lean

@@ -800,13 +800,15 @@ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1)
       · convert hj1
     · simp only [or_iff_not_imp_left]
       intro i_mem i_ne_zero i_ne_last
-      simp [Fin.ext_iff] at i_ne_zero i_ne_last
+      simp? [Fin.ext_iff] at i_ne_zero i_ne_last says
+        simp only [Fin.ext_iff, Fin.val_zero, Fin.val_last] at i_ne_zero i_ne_last
       have A : (1 + (i - 1) : ℕ) = (i : ℕ) := by
         rw [add_comm]
         exact Nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr i_ne_zero)
       refine' ⟨⟨i - 1, _⟩, _, _⟩
       · have : (i : ℕ) < n + 1 := i.2
-        simp [Nat.lt_succ_iff_lt_or_eq, i_ne_last] at this
+        simp? [Nat.lt_succ_iff_lt_or_eq, i_ne_last] at this says
+          simp only [Nat.lt_succ_iff_lt_or_eq, i_ne_last, or_false] at this
         exact Nat.pred_lt_pred i_ne_zero this
       · convert i_mem
         simp only [ge_iff_le]

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -175,7 +175,8 @@ theorem cells_bot : (⊥ : YoungDiagram).cells = ∅ :=
 theorem coe_bot : (⊥ : YoungDiagram).cells = (∅ : Set (ℕ × ℕ)) := by
   refine' Set.eq_of_subset_of_subset _ _
   intros x h
-  simp [mem_mk, Finset.coe_empty, Set.mem_empty_iff_false] at h
+  simp? [mem_mk, Finset.coe_empty, Set.mem_empty_iff_false] at h says
+    simp only [cells_bot, Finset.coe_empty, Set.mem_empty_iff_false] at h
   simp only [cells_bot, Finset.coe_empty, Set.empty_subset]
 #align young_diagram.coe_bot YoungDiagram.coe_bot
 

Mathlib/Computability/Halting.lean

@@ -202,7 +202,7 @@ theorem rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => eval c ∈ C)
     fixed_point₂
       (Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂
           ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂
-  simp at e
+  simp? at e says simp only [Bool.cond_decide] at e
   by_cases H : eval c ∈ C
   · simp only [H, if_true] at e
     change (fun b => g b) ∈ C
@@ -252,7 +252,8 @@ theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] :
         Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
         (by
           intro a x hx y hy
-          simp at hx hy
+          simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
+            and_true, exists_const] at hx hy
           cases hy.1 hx.1)
       · refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _
         rw [hk]

Mathlib/Computability/Partrec.lean

@@ -138,7 +138,7 @@ theorem rfindOpt_dom {α} {f : ℕ → Option α} : (rfindOpt f).Dom ↔ ∃ n a
       ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩
     refine' ⟨fd, _⟩
     have := rfind_spec (get_mem fd)
-    simp at this ⊢
+    simp? at this ⊢ says simp only [coe_some, mem_some_iff, ofOption_dom] at this ⊢
     cases' Option.isSome_iff_exists.1 this.symm with a e
     rw [e]; trivial⟩
 #align nat.rfind_opt_dom Nat.rfindOpt_dom

Mathlib/Computability/PartrecCode.lean

@@ -792,15 +792,17 @@ theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c
         exists_const, and_imp]
       introv h h₁ h₂ h₃
       exact ⟨le_trans h₂ h, h₁ h₃⟩
-    simp at h ⊢
+    simp? at h ⊢ says simp only [Option.mem_def] at h ⊢
     induction' c with cf cg hf hg cf cg hf hg cf cg hf hg cf hf generalizing x n <;>
       rw [evaln] at h ⊢ <;> refine' this hl' (fun h => _) h
     iterate 4 exact h
     · -- pair cf cg
-      simp [Seq.seq] at h ⊢
+      simp? [Seq.seq] at h ⊢ says
+        simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some,
+          Option.map_eq_some', exists_exists_and_eq_and] at h ⊢
       exact h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)
     · -- comp cf cg
-      simp [Bind.bind] at h ⊢
+      simp? [Bind.bind] at h ⊢ says simp only [bind, Option.mem_def, Option.bind_eq_some] at h ⊢
       exact h.imp fun a => And.imp (hg _ _) (hf _ _)
     · -- prec cf cg
       revert h
@@ -809,7 +811,8 @@ theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c
       · apply hf
       · exact fun y h₁ h₂ => ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩
     · -- rfind' cf
-      simp [Bind.bind] at h ⊢
+      simp? [Bind.bind] at h ⊢ says
+        simp only [unpaired, bind, pair_unpair, Option.mem_def, Option.bind_eq_some] at h ⊢
       refine' h.imp fun x => And.imp (hf _ _) _
       by_cases x0 : x = 0 <;> simp [x0]
       exact evaln_mono hl'
@@ -1102,7 +1105,7 @@ theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a
       · simp [evaln]
       let k := k' + 1
       simp only [show k'.succ = k from rfl]
-      simp [Nat.lt_succ_iff] at nk
+      simp? [Nat.lt_succ_iff] at nk says simp only [List.mem_range, lt_succ_iff] at nk
       have hg :
         ∀ {k' c' n},
           Nat.pair k' (encode c') < Nat.pair k (encode c) →