Commit 2022-12-13 21:55 1a6a60e0

fix: ignore aux decls in casesMatching (#991) Adds a check so that we ignore auxiliary declarations in casesMatching. Adds a testcase that fails when the fix is not applied. This prevents errors of the form

failed to revert foo, it is an auxiliary declaration created to represent recursive definitions

See Zulip discussion here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/tactic.20'cases'.20failed.20nested.20error