Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: inversion

Rui Li (Jul 14 2022 at 17:12):

Hi, is there any Lean tactic known to be equivalent to "inversion" in Coq?

Rui Li (Jul 14 2022 at 17:13):

Hi, is there any Lean tactic known to be equivalent to "inversion" in Coq?

Eric Rodriguez (Jul 14 2022 at 17:13):

injection or cases maybe?

Eric Rodriguez (Jul 14 2022 at 17:13):

tactic#injection, tactic#cases

Rui Li (Jul 14 2022 at 17:15):

Yes, perfect, thank you!

Alex J. Best (Jul 14 2022 at 17:15):

You might find https://github.com/jldodds/coq-lean-cheatsheet useful, it's a little old now so probably doesn't contain all the more recent mathlib tactics, but the basics should be there

Last updated: Dec 20 2023 at 11:08 UTC