chore: big combination of things

grunweg · grunweg · commit d6cfca709dd3 · 2025-05-01T13:18:01.000+02:00
diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean
@@ -828,11 +828,11 @@ instance subsingleton_gcdMonoid_of_unique_units : Subsingleton (GCDMonoid α) :=
     have hgcd : g₁.gcd = g₂.gcd := by
       ext a b
       refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
-      apply_rules (config := { allowSynthFailures := true }) [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
+      apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
     have hlcm : g₁.lcm = g₂.lcm := by
       ext a b
       refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
-      apply_rules (config := { allowSynthFailures := true }) [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
+      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
     cases g₁
     cases g₂
     dsimp only at hgcd hlcm
diff --git a/Mathlib/Algebra/Group/Equiv/Opposite.lean b/Mathlib/Algebra/Group/Equiv/Opposite.lean
@@ -15,7 +15,7 @@ variable {α : Type*}
 namespace MulOpposite
 
 /-- The function `MulOpposite.op` is an additive equivalence. -/
-@[simps! (config := { fullyApplied := false, simpRhs := true }) apply symm_apply]
+@[simps! -fullyApplied +simpRhs apply symm_apply]
 def opAddEquiv [Add α] : α ≃+ αᵐᵒᵖ where
   toEquiv := opEquiv
   map_add' _ _ := rfl
@@ -27,7 +27,7 @@ end MulOpposite
 namespace AddOpposite
 
 /-- The function `AddOpposite.op` is a multiplicative equivalence. -/
-@[simps! (config := { fullyApplied := false, simpRhs := true })]
+@[simps! -fullyApplied +simpRhs]
 def opMulEquiv [Mul α] : α ≃* αᵃᵒᵖ where
   toEquiv := opEquiv
   map_mul' _ _ := rfl
@@ -40,7 +40,7 @@ open MulOpposite
 
 /-- Inversion on a group is a `MulEquiv` to the opposite group. When `G` is commutative, there is
 `MulEquiv.inv`. -/
-@[to_additive (attr := simps! (config := { fullyApplied := false, simpRhs := true }))
+@[to_additive (attr := simps! -fullyApplied +simpRhs)
       "Negation on an additive group is an `AddEquiv` to the opposite group. When `G`
       is commutative, there is `AddEquiv.inv`."]
 def MulEquiv.inv' (G : Type*) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ :=
diff --git a/Mathlib/CategoryTheory/Comma/Over/Pullback.lean b/Mathlib/CategoryTheory/Comma/Over/Pullback.lean
@@ -49,7 +49,7 @@ variable [HasPullbacks C]
 
 /-- In a category with pullbacks, a morphism `f : X ⟶ Y` induces a functor `Over Y ⥤ Over X`,
 by pulling back a morphism along `f`. -/
-@[simps! (config := { simpRhs := true}) obj_left obj_hom map_left]
+@[simps! +simpRhs obj_left obj_hom map_left]
 def pullback {X Y : C} (f : X ⟶ Y) : Over Y ⥤ Over X where
   obj g := Over.mk (pullback.snd g.hom f)
   map := fun g {h} {k} =>
diff --git a/Mathlib/Data/List/SplitLengths.lean b/Mathlib/Data/List/SplitLengths.lean
@@ -81,7 +81,7 @@ theorem length_splitLengths_getElem_eq {i : ℕ} (hi : i < sz.length)
   simp only [take_splitLength]
   conv_rhs =>
     rw [List.getElem_take' (hj := i.lt_add_one)]
-    simp (config := {singlePass := true}) only [← map_splitLengths_length l _ h]
+    simp +singlePass only [← map_splitLengths_length l _ h]
     rw [getElem_map]
 
 theorem splitLengths_length_getElem {α : Type*} (l : List α) (sz : List ℕ)
diff --git a/Mathlib/Geometry/Euclidean/Circumcenter.lean b/Mathlib/Geometry/Euclidean/Circumcenter.lean
@@ -61,7 +61,7 @@ theorem existsUnique_dist_eq_of_insert {s : AffineSubspace ℝ P}
   let cc₂ := (ycc₂ / y) • (p -ᵥ orthogonalProjection s p : V) +ᵥ cc
   let cr₂ := √(cr * cr + ycc₂ * ycc₂)
   use ⟨cc₂, cr₂⟩
-  simp (config := { zeta := false, proj := false }) only
+  simp -zeta -proj only
   have hpo : p = (1 : ℝ) • (p -ᵥ orthogonalProjection s p : V) +ᵥ (orthogonalProjection s p : P) :=
     by simp
   constructor
diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
@@ -477,7 +477,7 @@ theorem ModelWithCorners.range_eq_univ {𝕜 : Type*} [NontriviallyNormedField 
     range I = univ := ModelWithCorners.Boundaryless.range_eq_univ
 
 /-- If `I` is a `ModelWithCorners.Boundaryless` model, then it is a homeomorphism. -/
-@[simps (config := {simpRhs := true})]
+@[simps +simpRhs]
 def ModelWithCorners.toHomeomorph {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
     (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] : H ≃ₜ E where
diff --git a/Mathlib/LinearAlgebra/Pi.lean b/Mathlib/LinearAlgebra/Pi.lean
@@ -541,7 +541,7 @@ theorem sumArrowLequivProdArrow_symm_apply_inr {α β} (f : α → M) (g : β 
   rfl
 
 /-- If `ι` has a unique element, then `ι → M` is linearly equivalent to `M`. -/
-@[simps (config := { simpRhs := true, fullyApplied := false }) symm_apply]
+@[simps +simpRhs -fullyAppliedsymm_apply]
 def funUnique (ι R M : Type*) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] :
     (ι → M) ≃ₗ[R] M :=
   { Equiv.funUnique ι M with
@@ -555,7 +555,7 @@ theorem funUnique_apply (ι R M : Type*) [Unique ι] [Semiring R] [AddCommMonoid
 variable (R M)
 
 /-- Linear equivalence between dependent functions `(i : Fin 2) → M i` and `M 0 × M 1`. -/
-@[simps (config := { simpRhs := true, fullyApplied := false }) symm_apply]
+@[simps +simpRhs -fullyApplied symm_apply]
 def piFinTwo (M : Fin 2 → Type v)
     [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
     ((i : Fin 2) → M i) ≃ₗ[R] M 0 × M 1 :=
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean
@@ -53,7 +53,7 @@ noncomputable def isometryEquivSumSquares (w' : ι → ℂ) :
   split_ifs with h
   · simp only [h, zero_smul, zero_mul]
   have hww' : w' j = w j := by simp only [w, dif_neg h, Units.val_mk0]
-  simp (config := {zeta := false}) only [one_mul, Units.val_mk0, smul_eq_mul]
+  simp -zeta only [one_mul, Units.val_mk0, smul_eq_mul]
   rw [hww']
   suffices v j * v j = w j ^ (-(1 / 2 : ℂ)) * w j ^ (-(1 / 2 : ℂ)) * w j * v j * v j by
     rw [this]; ring
diff --git a/Mathlib/Logic/Embedding/Basic.lean b/Mathlib/Logic/Embedding/Basic.lean
@@ -148,7 +148,7 @@ theorem equiv_symm_toEmbedding_trans_toEmbedding {α β : Sort*} (e : α ≃ β)
   simp
 
 /-- Transfer an embedding along a pair of equivalences. -/
-@[simps! (config := { fullyApplied := false, simpRhs := true })]
+@[simps! -fullyApplied +simpRhs]
 protected def congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α ≃ β) (e₂ : γ ≃ δ)
     (f : α ↪ γ) : β ↪ δ :=
   (Equiv.toEmbedding e₁.symm).trans (f.trans e₂.toEmbedding)
diff --git a/Mathlib/MeasureTheory/Covering/Differentiation.lean b/Mathlib/MeasureTheory/Covering/Differentiation.lean
@@ -94,7 +94,7 @@ measure. (This is a nontrivial result, following from the covering property of V
 theorem ae_eventually_measure_pos [SecondCountableTopology α] :
     ∀ᵐ x ∂μ, ∀ᶠ a in v.filterAt x, 0 < μ a := by
   set s := {x | ¬∀ᶠ a in v.filterAt x, 0 < μ a} with hs
-  simp (config := { zeta := false }) only [not_lt, not_eventually, nonpos_iff_eq_zero] at hs
+  simp -zeta only [not_lt, not_eventually, nonpos_iff_eq_zero] at hs
   change μ s = 0
   let f : α → Set (Set α) := fun _ => {a | μ a = 0}
   have h : v.FineSubfamilyOn f s := by
diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean
@@ -238,7 +238,7 @@ theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt [SecondCou
   obtain ⟨q, hq⟩ : ∃ q, F q = (n, z, p) := hF _
   -- then `x` belongs to `t q`.
   apply mem_iUnion.2 ⟨q, _⟩
-  simp (config := { zeta := false }) only [K, hq, mem_inter_iff, hp, and_true]
+  simp -zeta only [K, hq, mem_inter_iff, hp, and_true]
   exact subset_closure hnz
 
 variable [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ]
diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDense.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
@@ -152,9 +152,9 @@ theorem tendsto_approxOn {f : β → α} (hf : Measurable f) {s : Set α} {y₀
     Tendsto (fun n => approxOn f hf s y₀ h₀ n x) atTop (𝓝 <| f x) := by
   haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
   rw [← @Subtype.range_coe _ s, ← image_univ, ← (denseRange_denseSeq s).closure_eq] at hx
-  simp (config := { iota := false }) only [approxOn, coe_comp]
+  simp -iota only [approxOn, coe_comp]
   refine tendsto_nearestPt (closure_minimal ?_ isClosed_closure hx)
-  simp (config := { iota := false }) only [Nat.range_casesOn, closure_union, range_comp]
+  simp -iota only [Nat.range_casesOn, closure_union, range_comp]
   exact
     Subset.trans (image_closure_subset_closure_image continuous_subtype_val)
       subset_union_right
diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean
@@ -303,7 +303,7 @@ theorem mem_generatePiSystem_iUnion_elim' {α β} {g : β → Set (Set α)} {s :
       Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩
   · ext a
     constructor <;>
-      · simp (config := { proj := false }) only
+      · simp -proj only
           [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
         intro h1 b h_b h_b_in_T
         have h2 := h1 b h_b h_b_in_T
diff --git a/Mathlib/RingTheory/LittleWedderburn.lean b/Mathlib/RingTheory/LittleWedderburn.lean
@@ -99,7 +99,7 @@ private theorem center_eq_top [Finite D] (hD : InductionHyp D) : Subring.center
   rw [Nat.cast_sum]
   apply Finset.dvd_sum
   rintro ⟨x⟩ hx
-  simp (config := {zeta := false}) only [ConjClasses.quot_mk_eq_mk, Set.mem_toFinset] at hx ⊢
+  simp -zeta only [ConjClasses.quot_mk_eq_mk, Set.mem_toFinset] at hx ⊢
   set Zx := Subring.centralizer ({↑x} : Set D)
   -- The key thing is then to note that for all conjugacy classes `x`, `|x|` is given by
   -- `|Dˣ| / |Zxˣ|`, where `Zx` is the centralizer of `x`; but `Zx` is an algebra over `Z`, and
diff --git a/Mathlib/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean
@@ -185,13 +185,13 @@ elab (name := liftable_prefixes) "liftable_prefixes" : tactic => do
   withOptions (fun opts => synthInstance.maxSize.set opts
     (max 256 (synthInstance.maxSize.get opts))) do
   evalTactic (← `(tactic|
-    (simp (config := {failIfUnchanged := false}) only
+    (simp -failIfUnchanged only
       [monoidalComp, bicategoricalComp, Category.assoc, BicategoricalCoherence.iso,
       MonoidalCoherence.iso, Iso.trans, Iso.symm, Iso.refl,
       MonoidalCategory.whiskerRightIso, MonoidalCategory.whiskerLeftIso,
       Bicategory.whiskerRightIso, Bicategory.whiskerLeftIso]) <;>
     (apply (cancel_epi (𝟙 _)).1 <;> try infer_instance) <;>
-    (simp (config := {failIfUnchanged := false}) only
+    (simp -failIfUnchanged only
       [assoc_liftHom, Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂])))
 
 lemma insert_id_lhs {C : Type*} [Category C] {X Y : C} (f g : X ⟶ Y) (w : f ≫ 𝟙 _ = g) :
@@ -289,9 +289,9 @@ syntax (name := coherence) "coherence" : tactic
 elab_rules : tactic
 | `(tactic| coherence) => do
   evalTactic (← `(tactic|
-    (simp (config := {failIfUnchanged := false}) only [bicategoricalComp, monoidalComp]);
-    whisker_simps (config := {failIfUnchanged := false});
-    monoidal_simps (config := {failIfUnchanged := false})))
+    (simp -failIfUnchanged only [bicategoricalComp, monoidalComp]);
+    whisker_simps -failIfUnchanged;
+    monoidal_simps -failIfUnchanged))
   coherence_loop
 
 end Coherence
diff --git a/Mathlib/Tactic/Lift.lean b/Mathlib/Tactic/Lift.lean
@@ -147,9 +147,8 @@ def Lift.main (e t : TSyntax `term) (hUsing : Option (TSyntax `term))
     for decl in ← getLCtx do
       if decl.userName != newEqName then
         let declIdent := mkIdent decl.userName
-        evalTactic (← `(tactic| simp (config := {failIfUnchanged := false})
-          only [← $newEqIdent] at $declIdent:ident))
-    evalTactic (← `(tactic| simp (config := {failIfUnchanged := false}) only [← $newEqIdent]))
+        evalTactic (← `(tactic| simp -failIfUnchanged only [← $newEqIdent] at $declIdent:ident))
+    evalTactic (← `(tactic| simp -failIfUnchanged only [← $newEqIdent]))
   -- Clear the temporary hypothesis used for the new variable name if applicable
   if isNewVar && !isNewEq then
     evalTactic (← `(tactic| clear $newEqIdent))
