@[simp]

theorem Option.forM_none {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : α → m PUnit) : none.forM f = pure PUnit.unit

@[simp]

theorem Option.forM_some {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : α → m PUnit) (a : α) : (some a).forM f = f a

@[simp]

theorem Option.forM_map {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → m PUnit) : (Option.map g o).forM f = o.forM fun (a : α) => f (g a)

theorem Option.forIn'_congr {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as bs : Option α} (w : as = bs) {b b' : β} (hb : b = b') {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)} (h : ∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) : forIn' as b f = forIn' bs b' g

theorem Option.forIn'_eq_pelim {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : (a : α) → a ∈ o → β → m (ForInStep β)) (b : β) : forIn' o b f = o.pelim (pure b) fun (a : α) (h : a ∈ o) => ForInStep.value <$> f a h b

@[simp]

theorem Option.forIn'_yield_eq_pelim {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : (a : α) → a ∈ o → β → m γ) (g : (a : α) → a ∈ o → β → γ → β) (b : β) : (forIn' o b fun (a : α) (m_1 : a ∈ o) (b : β) => (fun (c : γ) => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = o.pelim (pure b) fun (a : α) (h : a ∈ o) => g a h b <$> f a h b

theorem Option.forIn'_pure_yield_eq_pelim {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) : (forIn' o b fun (a : α) (m_1 : a ∈ o) (b : β) => pure (ForInStep.yield (f a m_1 b))) = pure (o.pelim b fun (a : α) (h : a ∈ o) => f a h b)

@[simp]

theorem Option.forIn'_id_yield_eq_pelim {α : Type u_1} {β : Type u_2} (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) : (forIn' o b fun (a : α) (m : a ∈ o) (b : β) => ForInStep.yield (f a m b)) = o.pelim b fun (a : α) (h : a ∈ o) => f a h b

@[simp]

theorem Option.forIn'_map {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : (b : β) → b ∈ Option.map g o → γ → m (ForInStep γ)) : forIn' (Option.map g o) init f = forIn' o init fun (a : α) (h : a ∈ o) (y : γ) => f (g a) ⋯ y

theorem Option.forIn_eq_elim {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → m (ForInStep β)) (b : β) : forIn o b f = o.elim (pure b) fun (a : α) => ForInStep.value <$> f a b

@[simp]

theorem Option.forIn_yield_eq_elim {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → m γ) (g : α → β → γ → β) (b : β) : (forIn o b fun (a : α) (b : β) => (fun (c : γ) => ForInStep.yield (g a b c)) <$> f a b) = o.elim (pure b) fun (a : α) => g a b <$> f a b

theorem Option.forIn_pure_yield_eq_elim {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → β) (b : β) : (forIn o b fun (a : α) (b : β) => pure (ForInStep.yield (f a b))) = pure (o.elim b fun (a : α) => f a b)

@[simp]

theorem Option.forIn_id_yield_eq_elim {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β → β) (b : β) : (forIn o b fun (a : α) (b : β) => ForInStep.yield (f a b)) = o.elim b fun (a : α) => f a b

@[simp]

theorem Option.forIn_map {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) : forIn (Option.map g o) init f = forIn o init fun (a : α) (y : γ) => f (g a) y