not some implies none

Stream: Is there code for X?

[Marcus Rossel]

Is there a lemma for solving: ?

example {α : Type*} (a : option α) (h : ∀ b, ¬(a = some b)) : a = none := sorry

Or is this only true when α is inhabited?

[Eric Wieser]

Does library_search help?

[Eric Wieser]

cases a should make quick progress

[Eric Rodriguez]

by tidy solves it

[Kevin Buzzard]

I should think the first thing you should do with such a proof is replace it by by tidy? and see what it actually did, and then remove all the stuff that it did which it didn't need to do

[Scott Morrison]

Maybe someone should work on tidy again: presumably one could generate better output for tidy? by detecting some common useless steps.