@[simp]

theorem liftM_failure {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [Alternative m] [Alternative n] [MonadLift m n] [LawfulAlternativeLift m n] : liftM failure = failure

@[simp]

theorem liftM_orElse {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [Alternative m] [Alternative n] [MonadLift m n] [LawfulAlternativeLift m n] (x y : m α) : liftM (x <|> y) = (liftM x <|> liftM y)

theorem monadLift_guard {m : Type → Type u_1} {n : Type → Type u_2} [AlternativeMonad m] [AlternativeMonad n] [MonadLift m n] [LawfulAlternativeLift m n] [LawfulMonadLift m n] (p : Prop) [Decidable p] : monadLift (guard p) = guard p

@[simp]

theorem liftM_guard {m : Type → Type u_1} {n : Type → Type u_2} [AlternativeMonad m] [AlternativeMonad n] [MonadLift m n] [LawfulAlternativeLift m n] [LawfulMonadLift m n] (p : Prop) [Decidable p] : liftM (guard p) = guard p

theorem monadLift_optional {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [AlternativeMonad m] [AlternativeMonad n] [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulAlternativeLift m n] [LawfulMonadLift m n] (x : m α) : monadLift (optional x) = optional (monadLift x)

@[simp]

theorem liftM_optional {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [AlternativeMonad m] [AlternativeMonad n] [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulAlternativeLift m n] [LawfulMonadLift m n] (x : m α) : liftM (optional x) = optional (liftM x)

theorem Option.monadLift_elimM {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β : Type u_1} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulMonadLift m n] (x : m (Option α)) (y : m β) (z : α → m β) : monadLift (elimM x y z) = elimM (monadLift x) (monadLift y) fun (x : α) => monadLift (z x)

@[simp]

theorem Option.liftM_elimM {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β : Type u_1} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulMonadLift m n] (x : m (Option α)) (y : m β) (z : α → m β) : liftM (elimM x y z) = elimM (liftM x) (liftM y) fun (x : α) => liftM (z x)