Option seq/bind lemmas

[joehendrix]

This adds a few simplification theorems to simplify Option seq and bind expressions.

It builds on the commits from #330.

[digama0]

My preference is to merge #330 and rebase this on top, as the author of #330 is a new contributor and we shouldn't be poaching their work without (github) attribution.

[joehendrix]

I don't agree with labeling this as "poaching", but I am merging in their request now.

[digama0]

Suggested change

	@[simp] theorem none_bind (f : α → Option β) : Option.bind none f = none := rfl
	@[simp] theorem some_bind (x : α) (f : α → Option β): Option.bind (some x) f = f x := rfl
	@[simp] theorem bind_none (x : Option α)
	: Option.bind x (fun _ => (none : Option β)) = none := by
	cases x <;> rfl
	@[simp] theorem bind_some (x : Option α) : Option.bind x some = x := by cases x <;> rfl
	@[simp] theorem none_bind (f : α → Option β) : none.bind f = none := rfl
	@[simp] theorem some_bind (x : α) (f : α → Option β): (some x).bind f = f x := rfl
	@[simp] theorem bind_none (x : Option α)
	: x.bind (fun _ => (none : Option β)) = none := by
	cases x <;> rfl
	@[simp] theorem bind_some (x : Option α) : x.bind some = x := by cases x <;> rfl