chore: bump Aesop (#9905)

Mathlib/CategoryTheory/Category/Basic.lean

@@ -116,16 +116,16 @@ use in auto-params.
 -/
 macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  aesop $c* (options := { introsTransparency? := some .default, terminal := true })
-            (simp_options := { decide := true })
+  aesop $c* (config := { introsTransparency? := some .default, terminal := true })
+            (simp_config := { decide := true })
   (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
 
 /--
 We also use `aesop_cat?` to pass along a `Try this` suggestion when using `aesop_cat`
 -/
 macro (name := aesop_cat?) "aesop_cat?" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  aesop? $c* (options := { introsTransparency? := some .default, terminal := true })
+  aesop? $c* (config := { introsTransparency? := some .default, terminal := true })
   (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
 /--
 A variant of `aesop_cat` which does not fail when it is unable to solve the
@@ -134,7 +134,7 @@ nonterminal `simp`.
 -/
 macro (name := aesop_cat_nonterminal) "aesop_cat_nonterminal" c:Aesop.tactic_clause* : tactic =>
   `(tactic|
-    aesop $c* (options := { introsTransparency? := some .default, warnOnNonterminal := false })
+    aesop $c* (config := { introsTransparency? := some .default, warnOnNonterminal := false })
     (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
 
 

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -95,7 +95,7 @@ to standard `aesop`:
 macro (name := aesop_graph) "aesop_graph" c:Aesop.tactic_clause* : tactic =>
   `(tactic|
     aesop $c*
-      (options := { introsTransparency? := some .default, terminal := true })
+      (config := { introsTransparency? := some .default, terminal := true })
       (rule_sets [$(Lean.mkIdent `SimpleGraph):ident]))
 
 /--
@@ -104,7 +104,7 @@ Use `aesop_graph?` to pass along a `Try this` suggestion when using `aesop_graph
 macro (name := aesop_graph?) "aesop_graph?" c:Aesop.tactic_clause* : tactic =>
   `(tactic|
     aesop $c*
-      (options := { introsTransparency? := some .default, terminal := true })
+      (config := { introsTransparency? := some .default, terminal := true })
       (rule_sets [$(Lean.mkIdent `SimpleGraph):ident]))
 
 /--
@@ -115,7 +115,7 @@ nonterminal `simp`.
 macro (name := aesop_graph_nonterminal) "aesop_graph_nonterminal" c:Aesop.tactic_clause* : tactic =>
   `(tactic|
     aesop $c*
-      (options := { introsTransparency? := some .default, warnOnNonterminal := false })
+      (config := { introsTransparency? := some .default, warnOnNonterminal := false })
       (rule_sets [$(Lean.mkIdent `SimpleGraph):ident]))
 
 open Finset Function

Mathlib/Data/Matroid/Basic.lean

@@ -293,7 +293,7 @@ section aesop
   It uses a `[Matroid]` ruleset, and is allowed to fail. -/
 macro (name := aesop_mat) "aesop_mat" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  aesop $c* (options := { terminal := true })
+  aesop $c* (config := { terminal := true })
   (rule_sets [$(Lean.mkIdent `Matroid):ident]))
 
 /- We add a number of trivial lemmas (deliberately specialized to statements in terms of the

Mathlib/Data/Nat/WithBot.lean

@@ -35,7 +35,7 @@ theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := b
 theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
   any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
-              aesop (simp_options := { decide := true })
+              aesop (simp_config := { decide := true })
   repeat' erw [WithBot.coe_eq_coe]
   exact Nat.add_eq_one_iff
 #align nat.with_bot.add_eq_one_iff Nat.WithBot.add_eq_one_iff
@@ -44,7 +44,7 @@ theorem add_eq_two_iff {n m : WithBot ℕ} :
     n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
   any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
-              aesop (simp_options := { decide := true })
+              aesop (simp_config := { decide := true })
   repeat' erw [WithBot.coe_eq_coe]
   exact Nat.add_eq_two_iff
 #align nat.with_bot.add_eq_two_iff Nat.WithBot.add_eq_two_iff
@@ -53,7 +53,7 @@ theorem add_eq_three_iff {n m : WithBot ℕ} :
     n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
   any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
-              aesop (simp_options := { decide := true })
+              aesop (simp_config := { decide := true })
   repeat' erw [WithBot.coe_eq_coe]
   exact Nat.add_eq_three_iff
 #align nat.with_bot.add_eq_three_iff Nat.WithBot.add_eq_three_iff

Mathlib/Tactic/Continuity.lean

@@ -22,13 +22,14 @@ macro "continuity" : attr =>
 The tactic `continuity` solves goals of the form `Continuous f` by applying lemmas tagged with the
 `continuity` user attribute. -/
 macro "continuity" : tactic =>
-  `(tactic| aesop (options := { terminal := true }) (rule_sets [$(Lean.mkIdent `Continuous):ident]))
+  `(tactic| aesop (config := { terminal := true })
+     (rule_sets [$(Lean.mkIdent `Continuous):ident]))
 
 /--
 The tactic `continuity` solves goals of the form `Continuous f` by applying lemmas tagged with the
 `continuity` user attribute. -/
 macro "continuity?" : tactic =>
-  `(tactic| aesop? (options := { terminal := true })
+  `(tactic| aesop? (config := { terminal := true })
     (rule_sets [$(Lean.mkIdent `Continuous):ident]))
 
 -- Todo: implement `continuity!` and `continuity!?` and add configuration, original

Mathlib/Tactic/Measurability.lean

@@ -30,15 +30,16 @@ The tactic `measurability` solves goals of the form `Measurable f`, `AEMeasurabl
 `StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
 with the `measurability` user attribute. -/
 macro "measurability" (config)? : tactic =>
-  `(tactic| aesop (options := { terminal := true }) (rule_sets [$(Lean.mkIdent `Measurable):ident]))
+  `(tactic| aesop (config := { terminal := true })
+    (rule_sets [$(Lean.mkIdent `Measurable):ident]))
 
 /--
 The tactic `measurability?` solves goals of the form `Measurable f`, `AEMeasurable f`,
 `StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
 with the `measurability` user attribute, and suggests a faster proof script that can be substituted
 for the tactic call in case of success. -/
 macro "measurability?" (config)? : tactic =>
-  `(tactic| aesop? (options := { terminal := true })
+  `(tactic| aesop? (config := { terminal := true })
     (rule_sets [$(Lean.mkIdent `Measurable):ident]))
 
 -- Todo: implement `measurability!` and `measurability!?` and add configuration,

Mathlib/Topology/Sheaves/Presheaf.lean

@@ -81,16 +81,20 @@ attribute [sheaf_restrict] bot_le le_top le_refl inf_le_left inf_le_right
 /-- `restrict_tac` solves relations among subsets (copied from `aesop cat`) -/
 macro (name := restrict_tac) "restrict_tac" c:Aesop.tactic_clause* : tactic =>
 `(tactic| first | assumption |
-  aesop $c* (options :=
-    { terminal := true, assumptionTransparency := .reducible })
-    (simp_options := { enabled := false })
-  (rule_sets [-default, -builtin, $(Lean.mkIdent `Restrict):ident]))
+  aesop $c*
+    (config := { terminal := true
+                 assumptionTransparency := .reducible
+                 enableSimp := false })
+    (rule_sets [-default, -builtin, $(Lean.mkIdent `Restrict):ident]))
 
 /-- `restrict_tac?` passes along `Try this` from `aesop` -/
 macro (name := restrict_tac?) "restrict_tac?" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  aesop? $c* (options :=
-    { terminal := true, assumptionTransparency := .reducible, maxRuleApplications := 300 })
+  aesop? $c*
+    (config := { terminal := true
+                 assumptionTransparency := .reducible
+                 enableSimp := false
+                 maxRuleApplications := 300 })
   (rule_sets [-default, -builtin, $(Lean.mkIdent `Restrict):ident]))
 
 attribute[aesop 10% (rule_sets [Restrict])] le_trans

lake-manifest.json

@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "1c638703ed1c0c42aed2687acbeda67cec801454",
+   "rev": "82679d0151fc73db692399ae21818ebd1e66de9f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",