Lean4
/-- Attempt to prove that a finset is nonempty using the `finsetNonempty` aesop rule-set.
You can add lemmas to the rule-set by tagging them with either:
* `aesop safe apply (rule_sets := [finsetNonempty])` if they are always a good idea to follow or
* `aesop unsafe apply (rule_sets := [finsetNonempty])` if they risk directing the search to a blind
alley.
TODO: should some of the lemmas be `aesop safe simp` instead?
-/
def proveFinsetNonempty {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) : MetaM (Option Q(Finset.Nonempty $s)) := do
-- Aesop expects to operate on goals, so we're going to make a new goal.
let goal ← Lean.Meta.mkFreshExprMVar q(Finset.Nonempty $s)
let mvar := goal.mvarId!
let rulesets ← Aesop.Frontend.getGlobalRuleSets #[`builtin, `finsetNonempty]
let options : Aesop.Options' :=
{ terminal := true
generateScript := false
useDefaultSimpSet := false
warnOnNonterminal := false
forwardMaxDepth? := none }
let rules ← Aesop.mkLocalRuleSet rulesets options
let (remainingGoals, _) ←
try
Aesop.search (options := options.toOptions) mvar (.some rules)
catch _ =>
return none
if remainingGoals.size > 0 then
return none
Lean.getExprMVarAssignment? mvar
