Coq equivalent to eapply/erewrite

Stream: new members

[Vincent Siles]

Hi ! I'm slowly getting to know Lean, from a Coq background, and I'm wondering if there's equivalent to Coq's Evar (introduced by eapply/erewrite/refine/ ...) ?

[Johan Commelin]

We have erw and refine. But I don't know Evar, so I don't know if it's what you are looking for (@Vincent Siles)

[Pedro Minicz]

It has been a while since I've used Coq, but, as far as I remember, erewrite/eapply etc add the existential goals when it can't resolve arguments. As far as my experience goes, Lean's default rw/apply mostly behaves like the existential variants in Coq.