resolve match trivially to one arm

Stream: lean4

[Bhakti Shah]

I have a goal like

(none !=
    match h == h with
    | true => some h
    | false => sorry =
  true

h : α where there is a BEq instance for α. How do i resolve the match statement to just some h? Thanks!

[James Gallicchio]

This is only true if it's LawfulBEq I think. Once that's in context the simp lemmas should clean it up?

[Bhakti Shah]

James Gallicchio said:

This is only true if it's LawfulBEq I think. Once that's in context the simp lemmas should clean it up?

Ahh i don't have that instance, that makes sense. Thanks :)

[James Gallicchio]

btw, you might find it more ergonomic to just use DecidableEq instead of BEq. You can usually auto-derive DecidableEq for new types.

[Bhakti Shah]

That is what I decided to do! Unfortunately I can't autoderive, I need to use my own definition and I think that's where most of my problems are stemming from (even with the BEq stuff)