list.nth is either none

Stream: Is there code for X?

[Marcus Rossel]

I'm not sure if this is two specific, but is there some lemma in the direction of?:

example {α : Type*} (l : list (option α)) (n : ℕ) :
  (l.nth n).join = none → (l.nth n = (some none) ∨ l.nth n = none)

Thanks

[Floris van Doorn]

If you generalize l.nth n to an arbitary element of option (option α), this should be added to mathlib as option.join_eq_none. Contrast docs#option.join_ne_none

[Floris van Doorn]

import data.option.basic

namespace option

lemma join_eq_none {α : Type*} (o : option (option α)) : o.join = none ↔ o = none ∨ o = some none :=
by rcases o with _|_|_; simp

end option

[Floris van Doorn]

#6269

[Marcus Rossel]

This community is just so awesome :blush:
Thanks!