@[simp]

theorem Option.mem_toList {α : Type u_1} {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o

@[simp]

theorem Option.forIn'_none {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) : forIn' none b f = pure b

@[simp]

theorem Option.forIn'_some {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) : forIn' (some a) b f = do let x ← f a ⋯ b match x with | ForInStep.done r => pure r | ForInStep.yield r => pure r

@[simp]

theorem Option.forIn_none {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (b : β) (f : α → β → m (ForInStep β)) : forIn none b f = pure b

@[simp]

theorem Option.forIn_some {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) : forIn (some a) b f = do let x ← f a b match x with | ForInStep.done r => pure r | ForInStep.yield r => pure r

@[simp]

theorem Option.forIn'_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) : forIn' o.toList b f = forIn' o b fun (a : α) (m : a ∈ o) (b : β) => f a ⋯ b

@[simp]

theorem Option.forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) : forIn o.toList b f = forIn o b f