Bootstrapping theorems for Option

These are theorems used in the definitions of Std.Data.List.Basic. New theorems should be added to Std.Data.Option.Lemmas if they are not needed by the bootstrap.

@[simp]

theorem Option.getD_none : ∀ {α : Type u_1} {a : α}, Option.getD none a = a

@[simp]

theorem Option.getD_some : ∀ {α : Type u_1} {a b : α}, Option.getD (some a) b = a

@[simp]

theorem Option.map_none' {α : Type u_1} {β : Type u_2} (f : α → β) : Option.map f none = none

@[simp]

theorem Option.map_some' {α : Type u_1} {β : Type u_2} (a : α) (f : α → β) : Option.map f (some a) = some (f a)

@[simp]

theorem Option.none_bind {α : Type u_1} {β : Type u_2} (f : α → Option β) : Option.bind none f = none

@[simp]

theorem Option.some_bind {α : Type u_1} {β : Type u_2} (a : α) (f : α → Option β) : Option.bind (some a) f = f a