@[simp]

theorem Option.bindM_none {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Pure m] (f : α → m (Option β)) : Option.bindM f none = pure none

@[simp]

theorem Option.bindM_some {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Pure m] (a : α) (f : α → m (Option β)) : Option.bindM f (some a) = f a

@[simp]

theorem Option.forM_eq_forM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] : Option.forM = forM

@[simp]

theorem Option.forM_none {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : α → m PUnit) : forM none 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 : α) : forM (some a) 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) : forM (Option.map g o) f = forM o fun (a : α) => f (g a)

theorem Option.forM_join {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α → m PUnit) : forM o.join f = forM o fun (x : Option α) => forM x f

@[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] [LawfulMonad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) : forIn' (some a) b f = do let r ← f a ⋯ b pure r.value

@[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] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) : forIn (some a) b f = do let r ← f a b pure r.value

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 : o = some a) => 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 : o = some a) => g a h b <$> f a h b

@[simp]

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 : o = some a) => f a h b)

@[simp]

theorem Option.idRun_forIn'_yield_eq_pelim {α : Type u_1} {β : Type u_2} (o : Option α) (f : (a : α) → a ∈ o → β → Id β) (b : β) : (forIn' o b fun (a : α) (m : a ∈ o) (b : β) => ForInStep.yield <$> f a m b).run = o.pelim b fun (a : α) (h : o = some a) => (f a h b).run

@[deprecated Option.idRun_forIn'_yield_eq_pelim (since := "2025-05-21")]

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 : o = some a) => 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'_join {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] (b : β) (o : Option (Option α)) (f : (a : α) → a ∈ o.join → β → m (ForInStep β)) : forIn' o.join b f = forIn' o b fun (o' : Option α) (ho' : o' ∈ o) (b : β) => ForInStep.yield <$> forIn' o' b fun (a : α) (ha : a ∈ o') (b' : β) => f a ⋯ b'

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

@[simp]

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.idRun_forIn_yield_eq_elim {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β → Id β) (b : β) : (forIn o b fun (a : α) (b : β) => ForInStep.yield <$> f a b).run = o.elim b fun (a : α) => (f a b).run

@[deprecated Option.idRun_forIn_yield_eq_elim (since := "2025-05-21")]

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

theorem Option.forIn_join {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α → β → m (ForInStep β)) : forIn o.join init f = forIn o init fun (o' : Option α) (b : β) => ForInStep.yield <$> forIn o' b f

@[simp]

theorem Option.elimM_pure {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α → m β) : elimM (pure x) y z = x.elim y z

@[simp]

theorem Option.elimM_bind {m : Type u_1 → Type u_2} {α β γ : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → m (Option β)) (y : m γ) (z : β → m γ) : elimM (x >>= f) y z = do let __do_lift ← x elimM (f __do_lift) y z

@[simp]

theorem Option.elimM_map {m : Type u_1 → Type u_2} {α β γ : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → Option β) (y : m γ) (z : β → m γ) : elimM (f <$> x) y z = do let __do_lift ← x (f __do_lift).elim y z

@[simp]

theorem Option.tryCatch_eq_or {α : Type u_1} (o : Option α) (alternative : Unit → Option α) : tryCatch o alternative = o.or (alternative ())

@[simp]

theorem Option.throw_eq_none {α : Type u_1} : throw () = none

@[simp]

theorem Option.filterM_none {m : Type → Type u_1} {α : Type} [Applicative m] (p : α → m Bool) : Option.filterM p none = pure none

theorem Option.filterM_some {m : Type → Type u_1} {α : Type} [Applicative m] (p : α → m Bool) (a : α) : Option.filterM p (some a) = (fun (b : Bool) => if b = true then some a else none) <$> p a

theorem Option.sequence_join {m : Type u_1 → Type u_2} {α : Type u_1} [Applicative m] [LawfulApplicative m] {o : Option (Option (m α))} : o.join.sequence = join <$> (Option.map sequence o).sequence

theorem Option.bindM_join {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Pure m] {f : α → m (Option β)} {o : Option (Option α)} : Option.bindM f o.join = Option.bindM (fun (x : Option α) => Option.bindM f x) o

theorem Option.mapM_join {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] [LawfulApplicative m] {f : α → m β} {o : Option (Option α)} : Option.mapM f o.join = join <$> Option.mapM (Option.mapM f) o

theorem Option.mapM_guard {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] {x : α} {p : α → Bool} {f : α → m β} : Option.mapM f (guard p x) = if p x = true then some <$> f x else pure none