@[simp]

theorem monadLift_self {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : m α) : monadLift x = x

class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop

• map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
• id_map : ∀ {α : Type u} (x : f α), id <$> x = x
• comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

@[simp]

theorem id_map' {m : Type u_1 → Type u_2} {α : Type u_1} [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x

class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor : Prop

• map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
• id_map : ∀ {α : Type u} (x : f α), id <$> x = x
• comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq : ∀ {α β : Type u} (x : f α) (y : f β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
• seqRight_eq : ∀ {α β : Type u} (x : f α) (y : f β), (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
• pure_seq : ∀ {α β : Type u} (g : α → β) (x : f α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
• map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
• seq_pure : ∀ {α β : Type u} (g : f (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
• seq_assoc : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x

@[simp]

theorem pure_id_seq {f : Type u_1 → Type u_2} {α : Type u_1} [Applicative f] [LawfulApplicative f] (x : f α) : (Seq.seq (pure id) fun x => x) = x

class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative : Prop

• map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
• id_map : ∀ {α : Type u} (x : m α), id <$> x = x
• comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
• seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
• pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
• map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
• seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
• seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x
• bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let a ← x pure (f a)) = f <$> x
• bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun x_1 => x
• pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
• bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

@[simp]

theorem bind_pure {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x

theorem map_eq_pure_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = do let a ← x pure (f a)

theorem seq_eq_bind_map {m : Type u → Type u_1} {α : Type u} {β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : (Seq.seq f fun x => x) = do let x ← f x <$> x

theorem bind_congr {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Bind m] {x : m α} {f : α → m β} {g : α → m β} (h : ∀ (a : α), f a = g a) : x >>= f = x >>= g

@[simp]

theorem bind_pure_unit {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {x : m PUnit} : (do x pure PUnit.unit) = x

theorem map_congr {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Functor m] {x : m α} {f : α → β} {g : α → β} (h : ∀ (a : α), f a = g a) : f <$> x = g <$> x

theorem seq_eq_bind {m : Type u → Type u_1} {α : Type u} {β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : (Seq.seq mf fun x => x) = do let f ← mf f <$> x

theorem seqRight_eq_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (y : m β) : (SeqRight.seqRight x fun x => y) = do let _ ← x y

theorem seqLeft_eq_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (y : m β) : (SeqLeft.seqLeft x fun x => y) = do let a ← x let _ ← y pure a

Id

@[simp]

theorem Id.map_eq {α : Type u_1} {β : Type u_1} (x : Id α) (f : α → β) : f <$> x = f x

@[simp]

theorem Id.bind_eq {α : Type u_1} {β : Type u_1} (x : Id α) (f : α → id β) : x >>= f = f x

@[simp]

theorem Id.pure_eq {α : Type u_1} (a : α) : pure a = a

instance Id.instLawfulMonadIdInstMonadId : LawfulMonad Id

ExceptT

theorem ExceptT.ext {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} [Monad m] {x : ExceptT ε m α} {y : ExceptT ε m α} (h : ExceptT.run x = ExceptT.run y) : x = y

@[simp]

theorem ExceptT.run_pure {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} [Monad m] (x : α) : ExceptT.run (pure x) = pure (Except.ok x)

@[simp]

theorem ExceptT.run_lift {m : Type u → Type v} {α : Type u} {ε : Type u} [Monad m] (x : m α) : ExceptT.run (ExceptT.lift x) = Except.ok <$> x

@[simp]

theorem ExceptT.run_throw {m : Type u_1 → Type u_2} {ε : Type u_1} {β : Type u_1} {e : ε} [Monad m] : ExceptT.run (throw e) = pure (Except.error e)

@[simp]

theorem ExceptT.run_bind_lift {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : ExceptT.run (ExceptT.lift x >>= f) = do let a ← x ExceptT.run (f a)

@[simp]

theorem ExceptT.bind_throw {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} {β : Type u_1} {e : ε} [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : throw e >>= f = throw e

theorem ExceptT.run_bind {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} {f : α → ExceptT ε m β} [Monad m] (x : ExceptT ε m α) : ExceptT.run (x >>= f) = do let x ← ExceptT.run x match x with | Except.ok x => ExceptT.run (f x) | Except.error e => pure (Except.error e)

@[simp]

theorem ExceptT.lift_pure {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = pure a

@[simp]

theorem ExceptT.run_map {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ε : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : ExceptT.run (f <$> x) = Except.map f <$> ExceptT.run x

theorem ExceptT.seq_eq {m : Type u → Type u_1} {α : Type u} {β : Type u} {ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : (Seq.seq mf fun x => x) = do let f ← mf f <$> x

theorem ExceptT.bind_pure_comp {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ε : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x

theorem ExceptT.seqLeft_eq {α : Type u} {β : Type u} {ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y

theorem ExceptT.seqRight_eq {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y

instance ExceptT.instLawfulMonadExceptTInstMonadExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m)

ReaderT

theorem ReaderT.ext {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : ReaderT ρ m α} {y : ReaderT ρ m α} (h : ∀ (ctx : ρ), ReaderT.run x ctx = ReaderT.run y ctx) : x = y

@[simp]

theorem ReaderT.run_pure {m : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_1} [Monad m] (a : α) (ctx : ρ) : ReaderT.run (pure a) ctx = pure a

@[simp]

theorem ReaderT.run_bind {m : Type u_1 → Type u_2} {ρ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ) : ReaderT.run (x >>= f) ctx = do let a ← ReaderT.run x ctx ReaderT.run (f a) ctx

@[simp]

theorem ReaderT.run_mapConst {m : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_1} {β : Type u_1} [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ) : ReaderT.run (Functor.mapConst a x) ctx = Functor.mapConst a (ReaderT.run x ctx)

@[simp]

theorem ReaderT.run_map {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ρ : Type u_1} [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ) : ReaderT.run (f <$> x) ctx = f <$> ReaderT.run x ctx

@[simp]

theorem ReaderT.run_monadLift {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {α : Type u_1} {ρ : Type u_1} [MonadLiftT n m] (x : n α) (ctx : ρ) : ReaderT.run (monadLift x) ctx = monadLift x

@[simp]

theorem ReaderT.run_monadMap {n : Type u → Type u_1} {m : Type u → Type u_2} {ρ : Type u} {α : Type u} [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ) : ReaderT.run (monadMap f x) ctx = monadMap f (ReaderT.run x ctx)

@[simp]

theorem ReaderT.run_read {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] (ctx : ρ) : ReaderT.run ReaderT.read ctx = pure ctx

@[simp]

theorem ReaderT.run_seq {m : Type u → Type u_1} {ρ : Type u} {α : Type u} {β : Type u} [Monad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ) : ReaderT.run (Seq.seq f fun x => x) ctx = Seq.seq (ReaderT.run f ctx) fun x => ReaderT.run x ctx

@[simp]

theorem ReaderT.run_seqRight {m : Type u_1 → Type u_2} {ρ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : ReaderT.run (SeqRight.seqRight x fun x => y) ctx = SeqRight.seqRight (ReaderT.run x ctx) fun x => ReaderT.run y ctx

@[simp]

theorem ReaderT.run_seqLeft {m : Type u_1 → Type u_2} {ρ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : ReaderT.run (SeqLeft.seqLeft x fun x => y) ctx = SeqLeft.seqLeft (ReaderT.run x ctx) fun x => ReaderT.run y ctx

instance ReaderT.instLawfulFunctorReaderTInstFunctorReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulFunctor m] : LawfulFunctor (ReaderT ρ m)

instance ReaderT.instLawfulApplicativeReaderTInstApplicativeReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulApplicative m] : LawfulApplicative (ReaderT ρ m)

instance ReaderT.instLawfulMonadReaderTInstMonadReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m)

StateRefT

instance instLawfulMonadStateRefT'InstMonadStateRefT' {m : Type → Type} {ω : Type} {σ : Type} [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m)

StateT

theorem StateT.ext {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : StateT σ m α} {y : StateT σ m α} (h : ∀ (s : σ), StateT.run x s = StateT.run y s) : x = y

@[simp]

theorem StateT.run'_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} [Monad m] (x : StateT σ m α) (s : σ) : StateT.run' x s = (fun x => x.fst) <$> StateT.run x s

@[simp]

theorem StateT.run_pure {m : Type u_1 → Type u_2} {α : Type u_1} {σ : Type u_1} [Monad m] (a : α) (s : σ) : StateT.run (pure a) s = pure (a, s)

@[simp]

theorem StateT.run_bind {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ) : StateT.run (x >>= f) s = do let p ← StateT.run x s StateT.run (f p.fst) p.snd

@[simp]

theorem StateT.run_map {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : StateT.run (f <$> x) s = (fun p => (f p.fst, p.snd)) <$> StateT.run x s

@[simp]

theorem StateT.run_get {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (s : σ) : StateT.run get s = pure (s, s)

@[simp]

theorem StateT.run_set {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (s : σ) (s' : σ) : StateT.run (set s') s = pure (PUnit.unit, s')

@[simp]

theorem StateT.run_modify {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (f : σ → σ) (s : σ) : StateT.run (modify f) s = pure (PUnit.unit, f s)

@[simp]

theorem StateT.run_modifyGet {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} [Monad m] (f : σ → α × σ) (s : σ) : StateT.run (modifyGet f) s = pure ((f s).fst, (f s).snd)

@[simp]

theorem StateT.run_lift {m : Type u → Type u_1} {α : Type u} {σ : Type u} [Monad m] (x : m α) (s : σ) : StateT.run (StateT.lift x) s = do let a ← x pure (a, s)

@[simp]

theorem StateT.run_bind_lift {m : Type u → Type u_1} {β : Type u} {α : Type u} {σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : StateT.run (StateT.lift x >>= f) s = do let a ← x StateT.run (f a) s

@[simp]

theorem StateT.run_monadLift {m : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u} {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : StateT.run (monadLift x) s = do let a ← monadLift x pure (a, s)

@[simp]

theorem StateT.run_monadMap {m : Type u → Type u_1} {n : Type u → Type u_2} {σ : Type u} {α : Type u} [Monad m] [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) : StateT.run (monadMap f x) s = monadMap f (StateT.run x s)

@[simp]

theorem StateT.run_seq {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : StateT.run (Seq.seq f fun x => x) s = do let fs ← StateT.run f s (fun p => (Prod.fst (α → β) σ fs p.fst, p.snd)) <$> StateT.run x fs.snd

@[simp]

theorem StateT.run_seqRight {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : StateT.run (SeqRight.seqRight x fun x => y) s = do let p ← StateT.run x s StateT.run y p.snd

@[simp]

theorem StateT.run_seqLeft {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : StateT.run (SeqLeft.seqLeft x fun x => y) s = do let p ← StateT.run x s let p' ← StateT.run y p.snd pure (p.fst, p'.snd)

theorem StateT.seqRight_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y

theorem StateT.seqLeft_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y

instance StateT.instLawfulMonadStateTInstMonadStateT {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m)