Coq's inversion

Stream: Is there code for X?

[Thomas Vigouroux]

The inversion tactic seems very useful when doing Coq proofs about inductive predicates.
I wonder if there is a version of this tactic implemented in lean ?

There are people in my lab working on _small_ inversions which seems a little simpler to implement but I lack some knowledge about metaprogramming before attempting to do so.

Is there people working on this already ?

[Shreyas Srinivas]

cases does inversion for you

[Thomas Vigouroux]

hmmm
I have a Coq proof that I am attempting to reproduce, but for some reason cases does not help me...

[Yury G. Kudryashov]

What does this tactic do in Coq?

[Henrik Böving]

It's used when you have some h : InductivePredicate a b c and you want to do cases h to show that a b and c are of a certain form + some additional assumptions (potentially in multiple cases).

[Yury G. Kudryashov]

@Thomas Vigouroux Do you have an #mwe for the case when inversion works but cases fails?

[Thomas Vigouroux]

Unfortunately not, the example I have is very big
I'll try a to find a different formulation of my inductive to see if that helps

[Mario Carneiro]

what is the error message?