diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean index a296950f21840..870f1226d5ae8 100644 --- a/Mathlib/CategoryTheory/Category/Basic.lean +++ b/Mathlib/CategoryTheory/Category/Basic.lean @@ -119,6 +119,13 @@ macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic => (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 }) + (rule_sets [$(Lean.mkIdent `CategoryTheory):ident])) +/-- A variant of `aesop_cat` which does not fail when it is unable to solve the goal. Use this only for exploration! Nonterminal `aesop` is even worse than nonterminal `simp`. diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index 8ac40eb500a78..af220f38239ca 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -98,6 +98,15 @@ macro (name := aesop_graph) "aesop_graph" c:Aesop.tactic_clause* : tactic => (options := { introsTransparency? := some .default, terminal := true }) (rule_sets [$(Lean.mkIdent `SimpleGraph):ident])) +/-- +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 }) + (rule_sets [$(Lean.mkIdent `SimpleGraph):ident])) + /-- A variant of `aesop_graph` which does not fail if it is unable to solve the goal. Use this only for exploration! Nonterminal Aesop is even worse than diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean index ce24e1ae89438..79a3fe75f7d9f 100644 --- a/Mathlib/Topology/Sheaves/Presheaf.lean +++ b/Mathlib/Topology/Sheaves/Presheaf.lean @@ -79,6 +79,12 @@ macro (name := restrict_tac) "restrict_tac" c:Aesop.tactic_clause* : tactic => aesop $c* (options := { introsTransparency? := some .default, terminal := true }) (rule_sets [$(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 := { introsTransparency? := some .default, terminal := true }) + (rule_sets [$(Lean.mkIdent `Restrict):ident])) + example {X : TopCat} {v w x y z : Opens X} (h₀ : v ≤ x) (h₁ : x ≤ z ⊓ w) (h₂ : x ≤ y ⊓ z) : v ≤ y := by restrict_tac