Un-getting an Option

Stream: Is there code for X?

[hatzka]

Newbie question: My goal is of the form¬opt.get _ = val, and I can prove ¬opt = some val. How do I bridge the gap?

[Weiyi Wang]

contrapose! then prove the other direction by rw + simp?

[hatzka]

Oh, sorry, I actually found a simpler way right after posting. Isn't that always the way. Anyway, for anyone else reading this, rw [← Option.some_inj, Option.some_get]