[Merged by Bors] - chore: use modern config syntax more

Mathlib/Analysis/Analytic/Composition.lean

@@ -159,7 +159,7 @@ theorem applyComposition_update (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
 theorem compContinuousLinearMap_applyComposition {n : ℕ} (p : FormalMultilinearSeries 𝕜 F G)
     (f : E →L[𝕜] F) (c : Composition n) (v : Fin n → E) :
     (p.compContinuousLinearMap f).applyComposition c v = p.applyComposition c (f ∘ v) := by
-  simp (config := {unfoldPartialApp := true}) [applyComposition]; rfl
+  simp +unfoldPartialApp [applyComposition]; rfl
 
 end FormalMultilinearSeries
 

Mathlib/Analysis/NormedSpace/Alternating/Basic.lean

@@ -286,7 +286,7 @@ section
   NNReal.eq <| norm_ofSubsingleton i f
 
 /-- `ContinuousAlternatingMap.ofSubsingleton` as a linear isometry. -/
-@[simps (config := {simpRhs := true})]
+@[simps +simpRhs]
 def ofSubsingletonLIE [Subsingleton ι] (i : ι) : (E →L[𝕜] F) ≃ₗᵢ[𝕜] (E [⋀^ι]→L[𝕜] F) where
   __ := ofSubsingleton 𝕜 E F i
   map_add' _ _ := rfl
@@ -406,7 +406,7 @@ def compContinuousAlternatingMapCLM : (F →L[𝕜] G) →L[𝕜] (E [⋀^ι]→
     simpa using f.norm_compContinuousAlternatingMap_le g
 
 /-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled continuous linear equiv. -/
-@[simps (config := {simpRhs := true}) apply]
+@[simps +simpRhs apply]
 def _root_.ContinuousLinearEquiv.continuousAlternatingMapCongrRight (g : F ≃L[𝕜] G) :
     (E [⋀^ι]→L[𝕜] F) ≃L[𝕜] (E [⋀^ι]→L[𝕜] G) where
   __ := g.continuousAlternatingMapCongrRightEquiv

Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

@@ -136,7 +136,7 @@ lemma binEntropy_lt_log_two : binEntropy p < log 2 ↔ p ≠ 2⁻¹ := by
     simp at h
   wlog hp : p < 2⁻¹
   · have hp : 1 - p < 2⁻¹ := by
-      rw [sub_lt_comm]; norm_num at *; linarith (config := { splitNe := true })
+      rw [sub_lt_comm]; norm_num at *; linarith +splitNe
     rw [← binEntropy_one_sub]
     exact this hp.ne hp
   obtain hp₀ | hp₀ := le_or_lt p 0

Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean

@@ -92,7 +92,7 @@ def flipFunctorToInterchange : (functorToInterchange A K).flip ≅
   Iso.refl _
 
 /-- (Implementation) A natural isomorphism we will need to construct `iso`. -/
-@[simps! (config := { fullyApplied := false }) hom_app]
+@[simps! -fullyApplied hom_app]
 noncomputable def isoAux :
     (CostructuredArrow.proj yoneda A ⋙ yoneda ⋙ (evaluation Cᵒᵖ (Type u)).obj (limit K)) ≅
       ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj

Mathlib/Data/Matrix/Kronecker.lean

@@ -539,7 +539,7 @@ theorem det_kroneckerTMul [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n
     (A : Matrix m m α) (B : Matrix n n β) :
     det (A ⊗ₖₜ[R] B) = (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m) := by
   refine (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans ?_
-  simp (config := { eta := false }) only [mk_apply, ← includeLeft_apply (S := R),
+  simp -zeta only [mk_apply, ← includeLeft_apply (S := R),
     ← includeRight_apply]
   simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
   simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow,

Mathlib/Data/Set/Prod.lean

@@ -807,7 +807,7 @@ lemma eval_image_pi_of_not_mem [Decidable (s.pi t).Nonempty] (hi : i ∉ s) :
     exact ⟨x, hx⟩
   · rintro ⟨x, hx⟩
     refine ⟨Function.update x i xᵢ, ?_⟩
-    simpa (config := { contextual := true }) [(ne_of_mem_of_not_mem · hi)]
+    simpa +contextual [(ne_of_mem_of_not_mem · hi)]
 
 @[simp]
 theorem eval_image_univ_pi (ht : (pi univ t).Nonempty) :

Mathlib/Order/Filter/Defs.lean

@@ -430,7 +430,7 @@ elab_rules : tactic
       return [m.mvarId!]
   liftMetaTactic fun goal => do
     goal.apply (← mkConstWithFreshMVarLevels ``Filter.univ_mem') config
-  evalTactic <|← `(tactic| dsimp (config := {zeta := false}) only [Set.mem_setOf_eq])
+  evalTactic <|← `(tactic| dsimp -zeta only [Set.mem_setOf_eq])
   if let some l := wth then
     evalTactic <|← `(tactic| intro $[$l]*)
   if let some e := usingArg then

Mathlib/Tactic/Algebraize.lean

@@ -239,7 +239,7 @@ See the `algebraize` tag for instructions on what properties can be added.
 The tactic also comes with a configuration option `properties`. If set to `true` (default), the
 tactic searches through the local context for `RingHom` properties that can be converted to
 `Algebra` properties. The macro `algebraize_only` calls
-`algebraize (config := {properties := false})`,
+`algebraize -properties`,
 so in other words it only adds `Algebra` and `IsScalarTower` instances. -/
 syntax "algebraize " optConfig (algebraizeTermSeq)? : tactic
 

Mathlib/Tactic/GeneralizeProofs.lean

@@ -488,7 +488,7 @@ and furthermore if `h` duplicates a preceding local hypothesis then it is elimin
 
 The tactic is able to abstract proofs from under binders, creating universally quantified
 proofs in the local context.
-To disable this, use `generalize_proofs (config := { abstract := false })`.
+To disable this, use `generalize_proofs -abstract`.
 The tactic is also set to recursively abstract proofs from the types of the generalized proofs.
 This can be controlled with the `maxDepth` configuration option,
 with `generalize_proofs (config := { maxDepth := 0 })` turning this feature off.

MathlibTest/GeneralizeProofs.lean

@@ -89,7 +89,7 @@ example (x : ℕ) (h : x < 2) (H : Classical.choose (⟨x, h⟩ : ∃ x, x < 2)
 
 example (H : ∀ y, ∃ (x : ℕ) (h : x < y), Classical.choose (⟨x, h⟩ : ∃ x, x < y) < y) :
     ∀ y, ∃ (x : ℕ) (h : x < y), Classical.choose (⟨x, h⟩ : ∃ x, x < y) < y := by
-  generalize_proofs (config := { abstract := false })
+  generalize_proofs -abstract
   guard_target =ₛ ∀ y, ∃ (x : ℕ) (h : x < y), Classical.choose (⟨x, h⟩ : ∃ x, x < y) < y
   generalize_proofs a at H ⊢
   guard_hyp a :ₛ ∀ (y w : ℕ), w < y → ∃ x, x < y

MathlibTest/congr.lean

@@ -98,7 +98,7 @@ example {ι κ : Type u} (f : ι → α) (g : κ → α) :
     Set.image f Set.univ = Set.image g Set.univ := by
   congr!
   guard_target = Set.image f Set.univ = Set.image g Set.univ
-  congr! (config := {typeEqs := true})
+  congr! +typeEqs
   · guard_target = ι = κ
     exact test_sorry
   · guard_target = HEq f g
@@ -132,7 +132,7 @@ example (α β) [inst1 : Add α] [inst2 : Add β] (x : α) (y : β) : HEq (x + x
   -- But with typeEqs we can get it to generate the congruence anyway:
   have : α = β := test_sorry
   have : HEq inst1 inst2 := test_sorry
-  congr! (config := { typeEqs := true })
+  congr! +typeEqs
   guard_target = HEq x y
   exact test_sorry
   guard_target = HEq x y
@@ -148,7 +148,7 @@ example (prime : Nat → Prop) (n : Nat) :
 
 example (prime : Nat → Prop) (n : Nat) :
     prime (2 * n + 1) = prime (n + n + 1) := by
-  congr! (config := {etaExpand := true})
+  congr! +etaExpand
   · guard_target =ₛ (fun (x y : Nat) => x * y) = (fun (x y : Nat) => x + y)
     exact test_sorry
   · guard_target = 2 = n
@@ -287,22 +287,22 @@ example : n = m → 3 + n = m + 3 := by
   apply add_comm
 
 example (x y x' y' : Nat) (hx : x = x') (hy : y = y') : x + y = x' + y' := by
-  congr! (config := { closePre := false, closePost := false })
+  congr! -closePre -closePost
   exact hx
   exact hy
 
 example (x y x' : Nat) (hx : id x = id x') : x + y = x' + y := by
   congr!
 
 example (x y x' : Nat) (hx : id x = id x') : x + y = x' + y := by
-  congr! (config := { closePost := false })
+  congr! -closePost
   exact hx
 
 set_option linter.unusedTactic false in
 example : { f : Nat → Nat // f = id } :=
   ⟨?_, by
     -- prevents `rfl` from solving for `?m` in `?m = id`:
-    congr! (config := { closePre := false, closePost := false })
+    congr! -closePre -closePost
     ext x
     exact Nat.zero_add x⟩
 
@@ -343,7 +343,7 @@ x : α
 example
     {α : Type} (inst1 : BEq α) [LawfulBEq α] (inst2 : BEq α) [LawfulBEq α] (xs : List α) (x : α) :
     @List.erase _ inst1 xs x = @List.erase _ inst2 xs x := by
-  congr! (config := { beqEq := false })
+  congr! -beqEq
 
 
 /-!

MathlibTest/convert.lean

@@ -114,7 +114,7 @@ set_option linter.unusedTactic false in
 example {α β : Type u} [Fintype α] [Fintype β] : Fintype.card α = Fintype.card β := by
   congr!
   guard_target = Fintype.card α = Fintype.card β
-  congr! (config := {typeEqs := true})
+  congr! +typeEqs
   · guard_target = α = β
     exact test_sorry
   · rename_i inst1 inst2 h

MathlibTest/fail_if_no_progress.lean

@@ -64,7 +64,7 @@ h : x = true
 -/
 #guard_msgs in
 example (x : Bool) (h : x = true) : x = true := by
-  fail_if_no_progress simp (config := {failIfUnchanged := false})
+  fail_if_no_progress simp -failIfUnchanged
 
 /--
 error: no progress made on
@@ -74,7 +74,7 @@ h : x = true
 -/
 #guard_msgs in
 example (x : Bool) (h : x = true) : True := by
-  fail_if_no_progress simp (config := {failIfUnchanged := false}) at h
+  fail_if_no_progress simp -failIfUnchanged at h
 
 /--
 error: no progress made on

MathlibTest/linarith.lean

@@ -206,14 +206,13 @@ example (a b c : Rat) (h2 : b > 0) (h3 : b < 0) : Nat.prime 10 := by
   linarith
 
 example (a b c : Rat) (h2 : (2 : Rat) > 3) : a + b - c ≥ 3 := by
-  linarith (config := {exfalso := false})
+  linarith -exfalso
 
 -- Verify that we split conjunctions in hypotheses.
 example (x y : Rat)
     (h : 6 + ((x + 4) * x + (6 + 3 * y) * y) = 3 ∧ (x + 4) * x ≥ 0 ∧ (6 + 3 * y) * y ≥ 0) :
     False := by
-  fail_if_success
-    linarith (config := {splitHypotheses := false})
+  fail_if_success linarith -splitHypotheses
   linarith
 
 example (h : 1 < 0) (g : ¬ 37 < 42) (k : True) (l : (-7 : ℤ) < 5) : 3 < 7 := by
@@ -518,33 +517,33 @@ lemma works {a b : ℕ} (hab : a ≤ b) (h : b < a) : false := by
 end T
 
 example (a b c : ℚ) (h : a ≠ b) (h3 : b ≠ c) (h2 : a ≥ b) : b ≠ c := by
-  linarith (config := {splitNe := true})
+  linarith +splitNe
 
 example (a b c : ℚ) (h : a ≠ b) (h2 : a ≥ b) (h3 : b ≠ c) : a > b := by
-  linarith (config := {splitNe := true})
+  linarith +splitNe
 
 example (a b : ℕ) (h1 : b ≠ a) (h2 : b ≤ a) : b < a := by
-  linarith (config := {splitNe := true})
+  linarith +splitNe
 
 example (a b : ℕ) (h1 : b ≠ a) (h2 : ¬a < b) : b < a := by
-  linarith (config := {splitNe := true})
+  linarith +splitNe
 
 section
 -- Regression test for issue that splitNe didn't see `¬ a = b`
 
 example (a b : Nat) (h1 : a < b + 1) (h2 : a ≠ b) : a < b := by
-  linarith (config := {splitNe := true})
+  linarith +splitNe
 
 example (a b : Nat) (h1 : a < b + 1) (h2 : ¬ a = b) : a < b := by
-  linarith (config := {splitNe := true})
+  linarith +splitNe
 
 end
 
 -- Checks that splitNe handles metavariables and also that conjunction splitting occurs
 -- before splitNe splitting
 example (r : ℚ) (h' : 1 = r * 2) : 1 = 0 ∨ r = 1 / 2 := by
   by_contra! h''
-  linarith (config := {splitNe := true})
+  linarith +splitNe
 
 example (x y : ℚ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x * x := by nlinarith
 

MathlibTest/norm_num_ext.lean

@@ -110,7 +110,7 @@ set_option maxRecDepth 8000 in
 example : Nat.Prime (2 ^ 25 - 39) := by norm_num1
 example : ¬ Nat.Prime ((2 ^ 19 - 1) * (2 ^ 25 - 39)) := by norm_num1
 
-example : Nat.Prime 317 := by norm_num (config := {decide := false})
+example : Nat.Prime 317 := by norm_num -decide
 
 example : Nat.minFac 0 = 2 := by norm_num1
 example : Nat.minFac 1 = 1 := by norm_num1
@@ -346,19 +346,19 @@ variable {α : Type _} [CommRing α]
 
 -- Lists:
 -- `by decide` closes the three goals below.
-example : ([1, 2, 1, 3]).sum = 7 := by norm_num (config := {decide := true}) only
-example : (List.range 10).sum = 45 := by norm_num (config := {decide := true}) only
-example : (List.finRange 10).sum = 45 := by norm_num (config := {decide := true}) only
+example : ([1, 2, 1, 3]).sum = 7 := by norm_num +decide only
+example : (List.range 10).sum = 45 := by norm_num +decide only
+example : (List.finRange 10).sum = 45 := by norm_num +decide only
 
 example : (([1, 2, 1, 3] : List ℚ).map (fun i => i^2)).sum = 15 := by norm_num
 
 -- Multisets:
 -- `by decide` closes the three goals below.
-example : (1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).sum = 7 := by norm_num (config := {decide := true}) only
+example : (1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).sum = 7 := by norm_num +decide only
 example : ((1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).map (fun i => i^2)).sum = 15 := by
-  norm_num (config := {decide := true}) only
-example : (Multiset.range 10).sum = 45 := by norm_num (config := {decide := true}) only
-example : (↑[1, 2, 1, 3] : Multiset ℕ).sum = 7 := by norm_num (config := {decide := true}) only
+  norm_num +decide only
+example : (Multiset.range 10).sum = 45 := by norm_num +decide only
+example : (↑[1, 2, 1, 3] : Multiset ℕ).sum = 7 := by norm_num +decide only
 
 example : (({1, 2, 1, 3} : Multiset ℚ).map (fun i => i^2)).sum = 15 := by
   norm_num

MathlibTest/solve_by_elim/basic.lean

@@ -56,20 +56,20 @@ example (P₁ P₂ : α → Prop) (f : ∀ (a : α), P₁ a → P₂ a → β)
   solve_by_elim
 
 example {X : Type} (x : X) : x = x := by
-  fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `rfl` lemma
+  fail_if_success solve_by_elim -constructor only -- needs the `rfl` lemma
   solve_by_elim
 
 -- Needs to apply `rfl` twice, with different implicit arguments each time.
 -- A naive implementation of solve_by_elim would get stuck.
 example {X : Type} (x y : X) (p : Prop) (h : x = x → y = y → p) : p := by solve_by_elim
 
 example : True := by
-  fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `trivial` lemma
+  fail_if_success solve_by_elim -constructor only -- needs the `trivial` lemma
   solve_by_elim
 
 example : True := by
   -- uses the `trivial` lemma, which should now be removed from the default set:
-  solve_by_elim (config := {constructor := false})
+  solve_by_elim -constructor
 
 example : True := by
   solve_by_elim only -- uses the constructor discharger.
@@ -82,11 +82,11 @@ example (P₁ P₂ : α → Prop) (f : ∀ (a: α), P₁ a → P₂ a → β)
   solve_by_elim
 
 example {α : Type} {a b : α → Prop} (h₀ : b = a) (y : α) : a y = b y := by
-  fail_if_success solve_by_elim (config := {symm := false})
+  fail_if_success solve_by_elim -symm
   solve_by_elim
 
 example (P : True → False) : 3 = 7 := by
-  fail_if_success solve_by_elim (config := {exfalso := false})
+  fail_if_success solve_by_elim -exfalso
   solve_by_elim
 
 -- Verifying that `solve_by_elim` acts only on the main goal.
@@ -126,7 +126,7 @@ example (f g : Nat → Prop) : (∃ k : Nat, f k) ∨ (∃ k : Nat, g k) ↔ ∃
 
 -- Test that we can disable the `intro` discharger.
 example (P : Prop) : P → P := by
-  fail_if_success solve_by_elim (config := {intro := false})
+  fail_if_success solve_by_elim -intro
   solve_by_elim
 
 example (P Q : Prop) : P ∧ Q → P ∧ Q := by
@@ -143,12 +143,12 @@ example {α : Type} {p : α → Prop} (h₀ : ∀ x, p x) (y : α) : p y := by
 
 -- Check that `apply_assumption` uses `symm`.
 example (a b : α) (h : b = a) : a = b := by
-  fail_if_success apply_assumption (config := {symm := false})
+  fail_if_success apply_assumption -symm
   apply_assumption
 
 -- Check that `apply_assumption` uses `exfalso`.
 example {P Q : Prop} (p : P) (q : Q) (h : P → ¬ Q) : Nat := by
-  fail_if_success apply_assumption (config := {exfalso := false})
+  fail_if_success apply_assumption -exfalso
   apply_assumption <;> assumption
 
 end apply_assumption