apply and refine up to syntactic equality

Stream: mathlib4

[Sky Wilshaw]

Is there a way to limit apply and/or refine to only work up to syntactic equality? This would improve the speed of a parser combinator I'm writing, since it would fail faster.

[Yaël Dillies]

Use a with_something combinator

[Yaël Dillies]

Something like with_reducible_and_instances apply your_lemma

[Sky Wilshaw]

I can't find any references online for these sorts of things - can you point me to an example?

[Yaël Dillies]

I have never used it myself but there are examples on Zulip

[Kyle Miller]

There's no option for just syntactic equality, but the most restrictive one is with_reducible apply foo, which does unification unfolding only reducible definitions (so those with the @[reducible] attribute, which includes abbrevs)

[Kyle Miller]

with_reducible_and_instances will additionally unfold instances

[Kyle Miller]

Then, to unfold more than what is normally unfolded, there's with_unfolding_all