diff --git a/library/init/category/cont.lean b/library/init/category/cont.lean
index b30b0d60c9..673221dc9e 100644
--- a/library/init/category/cont.lean
+++ b/library/init/category/cont.lean
@@ -33,7 +33,7 @@ section
   instance : monad (cont_t r m) :=
   { pure := @pure, bind := @bind }
 
-  protected def call_cc {α β : Type u} (f : ((α → cont_t r m β) → cont_t r m α)) : cont_t r m α :=
+  protected def call_cc {α β : Type u} (f : (α → cont_t r m β) → cont_t r m α) : cont_t r m α :=
   ⟨λ cc, (f (λ a, ⟨λ _, cc a⟩)).run cc⟩
 
   instance : monad_cont (cont_t r m) :=
diff --git a/library/init/category/default.lean b/library/init/category/default.lean
index bf78322b3d..0a97af71b5 100644
--- a/library/init/category/default.lean
+++ b/library/init/category/default.lean
@@ -5,6 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.category.applicative init.category.functor init.category.alternative
-import init.category.monad init.category.state init.category.lift
-import init.category.lawful init.category.id init.category.except init.category.reader
+import init.category.monad init.category.lift init.category.lawful
+import init.category.state init.category.id init.category.except init.category.reader
 import init.category.cont
diff --git a/library/init/category/except.lean b/library/init/category/except.lean
index 747dca28a1..d5cd514061 100644
--- a/library/init/category/except.lean
+++ b/library/init/category/except.lean
@@ -2,6 +2,8 @@
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jared Roesch, Sebastian Ullrich
+
+The except monad transformer.
 -/
 
 prelude
@@ -22,8 +24,8 @@ variables {ε : Type u} {m : Type v → Type w}
 protected def orelse [monad_except ε m] {α : Type v} (t₁ t₂ : m α) : m α :=
 catch t₁ $ λ _, t₂
 
-/- Alternative orelse operator that allows to select which exception should be used.
-   The default is to use the first exception since the standard `orelse` uses the second. -/
+/-- Alternative orelse operator that allows to select which exception should be used.
+    The default is to use the first exception since the standard `orelse` uses the second. -/
 meta def orelse' [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex := tt) : m α :=
 catch t₁ $ λ e₁, catch t₂ $ λ e₂, throw (if use_first_ex then e₁ else e₂)
 end monad_except
@@ -73,17 +75,17 @@ namespace except_t
 section
   parameters {ε : Type u} {m : Type u → Type v} [monad m]
 
-  protected def return {α : Type u} (a : α) : except_t ε m α :=
+  @[inline] protected def return {α : Type u} (a : α) : except_t ε m α :=
   ⟨pure $ except.ok a⟩
 
-  protected def bind_cont {α β : Type u} (f : α → except_t ε m β) : except ε α → m (except ε β)
+  @[inline] protected def bind_cont {α β : Type u} (f : α → except_t ε m β) : except ε α → m (except ε β)
   | (except.ok a)    := (f a).run
   | (except.error e) := pure (except.error e)
 
-  protected def bind {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) : except_t ε m β :=
+  @[inline] protected def bind {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) : except_t ε m β :=
   ⟨ma.run >>= bind_cont f⟩
 
-  protected def lift {α : Type u} (t : m α) : except_t ε m α :=
+  @[inline] protected def lift {α : Type u} (t : m α) : except_t ε m α :=
   ⟨except.ok <$> t⟩
 
   instance : has_monad_lift m (except_t ε m) :=
@@ -95,7 +97,7 @@ section
    | except.error e := (handle e).run
    end⟩
 
-  protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : except_t ε m α → except_t ε m' α :=
+  @[inline] protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : except_t ε m α → except_t ε m' α :=
   λ x, ⟨f x.run⟩
 
   instance (m') [monad m'] : monad_functor m m' (except_t ε m) (except_t ε m') :=
diff --git a/library/init/category/id.lean b/library/init/category/id.lean
index 5f562c90e9..da84fa9cd1 100644
--- a/library/init/category/id.lean
+++ b/library/init/category/id.lean
@@ -2,6 +2,8 @@
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
+
+The identity monad.
 -/
 prelude
 import init.category.lift
diff --git a/library/init/category/lawful.lean b/library/init/category/lawful.lean
index 776cc92439..b1896ff171 100644
--- a/library/init/category/lawful.lean
+++ b/library/init/category/lawful.lean
@@ -62,17 +62,15 @@ attribute [simp] pure_bind
 @[simp] theorem bind_pure {α : Type u} {m : Type u → Type v} [monad m] [is_lawful_monad m] (x : m α) : x >>= pure = x :=
 show x >>= pure ∘ id = x, by rw bind_pure_comp_eq_map; simp [id_map]
 
-lemma bind_ext_congr {α β} {m : Type u → Type v} [has_bind m] {x : m α} {f : α → m β} (g : α → m β) :
+lemma bind_ext_congr {α β} {m : Type u → Type v} [has_bind m] {x : m α} {f g : α → m β} :
   (∀ a, f a = g a) →
   x >>= f = x >>= g :=
-λ h, have f = g, from funext h,
-     by simp [this]
+λ h, by simp [show f = g, from funext h]
 
-lemma map_ext_congr {α β} {m : Type u → Type v} [has_map m] {x : m α} {f : α → β} (g : α → β) :
+lemma map_ext_congr {α β} {m : Type u → Type v} [has_map m] {x : m α} {f g : α → β} :
   (∀ a, f a = g a) →
   (f <$> x : m β) = g <$> x :=
-λ h, have f = g, from funext h,
-     by simp [this]
+λ h, by simp [show f = g, from funext h]
 
 -- instances of previously defined monads
 
@@ -84,32 +82,41 @@ variables {α β : Type}
 end id
 
 instance : is_lawful_monad id :=
-by refine { id_map := _, bind_assoc := _, pure_bind := _ };
-   intros; refl
+by refine { .. }; intros; refl
+
 
 namespace state_t
 section
   variable  {σ : Type u}
   variable  {m : Type u → Type v}
-  variable  [monad m]
   variables {α β : Type u}
   variables (x : state_t σ m α) (st : σ)
 
   lemma ext {x x' : state_t σ m α} (h : ∀ st, x.run st = x'.run st) : x = x' :=
-  by cases_type* state_t; simp [show x = x', from funext h]
+  by cases x; cases x'; simp [show x = x', from funext h]
+
+  variable  [monad m]
 
   @[simp] lemma run_pure (a) : (pure a : state_t σ m α).run st = pure (a, st) := rfl
-  @[simp] lemma run_bind (f : α → state_t σ m β) : (x >>= f).run st = x.run st >>= λ p, (f p.1).run p.2 :=
-  by simp [bind, state_t.bind, state_t.run]; rw bind_ext_congr; intro a; cases a; simp [state_t.bind, state_t.run]
-  @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run st = (λ p : α × σ, (f (prod.fst p), prod.snd p)) <$> x.run st :=
+  @[simp] lemma run_bind (f : α → state_t σ m β) :
+    (x >>= f).run st = x.run st >>= λ p, (f p.1).run p.2 :=
+  by apply bind_ext_congr; intro a; cases a; simp [state_t.bind, state_t.run]
+  @[simp] lemma run_map (f : α → β) [is_lawful_monad m] :
+    (f <$> x).run st = (λ p : α × σ, (f (prod.fst p), prod.snd p)) <$> x.run st :=
   begin
     rw ←bind_pure_comp_eq_map m,
     change (x >>= pure ∘ f).run st = _,
     simp
   end
-  @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) : (monad_lift x : state_t σ m α).run st = do a ← (monad_lift x : m α), pure (a, st) := rfl
-  @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) : (monad_map @f x : state_t σ m' α).run st = monad_map @f (x.run st) := rfl
-  @[simp] lemma run_zoom {σ'} (st get set) : (state_t.zoom get set x : state_t σ' m α).run st = (λ p : α × σ, (p.1, set p.2 st)) <$> x.run (get st) := rfl
+  @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) :
+    (monad_lift x : state_t σ m α).run st = do a ← (monad_lift x : m α), pure (a, st) := rfl
+  @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) :
+    (monad_map @f x : state_t σ m' α).run st = monad_map @f (x.run st) := rfl
+  @[simp] lemma run_zoom {σ'} (st get set) :
+    (state_t.zoom get set x : state_t σ' m α).run st =
+    do (a, st') ← x.run (get st),
+       pure (a, set st' st) :=
+  by delta state_t.zoom; refl
   @[simp] lemma run_get : (state_t.get : state_t σ m σ).run st = pure (st, st) := rfl
   @[simp] lemma run_put (st') : (state_t.put st' : state_t σ m _).run st = pure (punit.star, st') := rfl
 end
@@ -117,45 +124,49 @@ end state_t
 
 instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (σ : Type u) : is_lawful_monad (state_t σ m) :=
 { id_map := by intros; apply state_t.ext; intro; simp; erw id_map,
-  pure_bind := by intros; apply state_t.ext; intro; simp,
-  bind_assoc := by intros; apply state_t.ext; intro; simp [bind_assoc] }
+  pure_bind := by intros; apply state_t.ext; simp,
+  bind_assoc := by intros; apply state_t.ext; simp [bind_assoc] }
 
 
 namespace except_t
-  variables {α β ε : Type u} {m : Type u → Type v} [monad m] (x : except_t ε m α)
+  variables {α β ε : Type u} {m : Type u → Type v} (x : except_t ε m α)
 
   lemma ext {x x' : except_t ε m α} (h : x.run = x'.run) : x = x' :=
-  by cases_type* except_t; simp * at *
+  by cases x; cases x'; simp * at *
+
+  variable [monad m]
 
   @[simp] lemma run_pure (a) : (pure a : except_t ε m α).run = pure (@except.ok ε α a) := rfl
-  @[simp] lemma run_bind (f : α → except_t ε m β) : (x >>= f).run = x.run >>= except_t.bind_cont f := rfl
+  @[simp] lemma run_bind (f : α → except_t ε m β) : (x >>= f).run = x.run >>= except_t.bind_cont f :=
+  rfl
   @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run = except.map f <$> x.run :=
   begin
     rw ←bind_pure_comp_eq_map m,
-    change (x >>= pure ∘ f).run = _,
-    simp,
-    rw [bind_ext_congr],
+    change x.run >>= except_t.bind_cont (pure ∘ f) = _,
+    apply bind_ext_congr,
     intro a; cases a; simp [except_t.bind_cont, except.map]
   end
-  @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) : (@monad_lift _ _ _ _ x : except_t ε m α).run = except.ok <$> (monad_lift x : m α) := rfl
-  @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) : (monad_map @f x : except_t ε m' α).run = monad_map @f x.run := rfl
+  @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) :
+    (monad_lift x : except_t ε m α).run = except.ok <$> (monad_lift x : m α) := rfl
+  @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) :
+    (monad_map @f x : except_t ε m' α).run = monad_map @f x.run := rfl
 end except_t
 
 instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (ε : Type u) : is_lawful_monad (except_t ε m) :=
 { id_map := begin
-    intros, apply except_t.ext, simp,
+    intros, apply except_t.ext, simp only [except_t.run_map],
     rw [map_ext_congr, id_map],
     intro a, cases a; refl
   end,
   bind_pure_comp_eq_map := begin
-    intros, apply except_t.ext, simp,
+    intros, apply except_t.ext, simp only [except_t.run_map, except_t.run_bind],
     rw [bind_ext_congr, bind_pure_comp_eq_map],
     intro a, cases a; refl
   end,
   bind_assoc := begin
-    intros, apply except_t.ext, simp [bind_assoc],
+    intros, apply except_t.ext, simp only [except_t.run_bind, bind_assoc],
     rw [bind_ext_congr],
-    { intro a, cases a; simp [except_t.bind_cont] }
+    intro a, cases a; simp [except_t.bind_cont]
   end,
   pure_bind := by intros; apply except_t.ext; simp [except_t.bind_cont] }
 
@@ -164,19 +175,23 @@ namespace reader_t
 section
   variable  {r : Type u}
   variable  {m : Type u → Type v}
-  variable  [monad m]
   variables {α β : Type u}
   variables (x : reader_t r m α) (cfg : r)
 
   lemma ext {x x' : reader_t r m α} (h : ∀ cfg, x.run cfg = x'.run cfg) : x = x' :=
-  by cases_type* reader_t; simp [show x = x', from funext h]
+  by cases x; cases x'; simp [show x = x', from funext h]
+
+  variable  [monad m]
 
   @[simp] lemma run_pure (a) : (pure a : reader_t r m α).run cfg = pure a := rfl
-  @[simp] lemma run_bind (f : α → reader_t r m β) : (x >>= f).run cfg = x.run cfg >>= λ a, (f a).run cfg := rfl
+  @[simp] lemma run_bind (f : α → reader_t r m β) :
+    (x >>= f).run cfg = x.run cfg >>= λ a, (f a).run cfg := rfl
   @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run cfg = f <$> x.run cfg :=
   by rw ←bind_pure_comp_eq_map m; refl
-  @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) : (@monad_lift _ _ _ _ x : reader_t r m α).run cfg = (monad_lift x : m α) := rfl
-  @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) : (monad_map @f x : reader_t r m' α).run cfg = monad_map @f (x.run cfg) := rfl
+  @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) :
+    (monad_lift x : reader_t r m α).run cfg = (monad_lift x : m α) := rfl
+  @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) :
+    (monad_map @f x : reader_t r m' α).run cfg = monad_map @f (x.run cfg) := rfl
   @[simp] lemma run_read : (reader_t.read : reader_t r m r).run cfg = pure cfg := rfl
 end
 end reader_t
@@ -197,7 +212,8 @@ namespace cont_t
   by cases x; cases x'; simp [show x = x', from funext h]
 
   @[simp] lemma run_pure (a : α) (cc : α → m r) : (pure a : cont_t r m α).run cc = cc a := rfl
-  @[simp] lemma run_bind (f : α → cont_t r m β) (cc : β → m r) : (x >>= f).run cc = x.run (λ a, (f a).run cc) := rfl
+  @[simp] lemma run_bind (f : α → cont_t r m β) (cc : β → m r) :
+    (x >>= f).run cc = x.run (λ a, (f a).run cc) := rfl
   @[simp] lemma run_map (f : α → β) (cc : β → m r) : (f <$> x).run cc = x.run (cc ∘ f) := rfl
 end cont_t
 
diff --git a/library/init/category/monad.lean b/library/init/category/monad.lean
index 097647cafb..59329a71a9 100644
--- a/library/init/category/monad.lean
+++ b/library/init/category/monad.lean
@@ -24,7 +24,7 @@ class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (ma
 (map := λ α β f x, x >>= pure ∘ f)
 (seq := λ α β f x, f >>= (<$> x))
 
-@[reducible] def return {m : Type u → Type v} [monad m] {α : Type u} : α → m α :=
+@[reducible, inline] def return {m : Type u → Type v} [monad m] {α : Type u} : α → m α :=
 pure
 
 /- Identical to has_bind.and_then, but it is not inlined. -/
diff --git a/library/init/category/monad_fail.lean b/library/init/category/monad_fail.lean
index b82c1b987a..052cf81bc7 100644
--- a/library/init/category/monad_fail.lean
+++ b/library/init/category/monad_fail.lean
@@ -18,5 +18,5 @@ def match_failed {α : Type u} {m : Type u → Type v} [monad_fail m] : m α :=
 monad_fail.fail "match failed"
 
 -- TODO(Sebastian): Could take `has_monad_lift_t`, except that the refl instances will make it loop
-instance monad_fail_lift (m n : Type u → Type v) [has_monad_lift m n] [monad_fail m] [monad_n : monad n] : monad_fail n :=
-{ fail := λ α s, monad_lift (monad_fail.fail s : m α), ..monad_n }
+instance monad_fail_lift (m n : Type u → Type v) [has_monad_lift m n] [monad_fail m] [monad n] : monad_fail n :=
+{ fail := λ α s, monad_lift (monad_fail.fail s : m α) }
diff --git a/library/init/category/reader.lean b/library/init/category/reader.lean
index cf7ef2c75e..945e81d9a1 100644
--- a/library/init/category/reader.lean
+++ b/library/init/category/reader.lean
@@ -2,6 +2,8 @@
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
+
+The reader monad transformer for passing immutable state.
 -/
 
 prelude
@@ -13,6 +15,8 @@ structure reader_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (ma
 
 @[reducible] def reader (r : Type u) := reader_t r id
 
+attribute [pp_using_anonymous_constructor] reader_t
+
 namespace reader_t
 section
   variable  {r : Type u}
@@ -47,6 +51,8 @@ section
 end
 end reader_t
 
+
+/-- A specialization of `monad_lift` to `reader_t` that allows `r` to be inferred. -/
 class monad_reader_lift (r : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
 [has_lift : has_monad_lift_t (reader_t r m) n]
 
@@ -57,6 +63,8 @@ def monad_reader_lift.read {r : Type u} {m : Type u → Type v} {n : Type u →
 @monad_lift _ _ _ _ (reader_t.read : reader_t r m _)
 export monad_reader_lift (read)
 
+
+/-- A specialization of `monad_map` to `reader_t` that allows `r` to be inferred. -/
 class monad_reader_functor (r r' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
 [functor {} : monad_functor_t (reader_t r m) (reader_t r' m) n n']
 
@@ -69,5 +77,6 @@ def with_reader_t {r r' m} [monad m] {α} (f : r' → r) : reader_t r m α → r
 def with_reader {r r'} {m n n'} [monad m] [monad_reader_functor r r' m n n'] {α : Type u} (f : r' → r) : n α → n' α :=
 monad_map $ λ α, (with_reader_t f : reader_t r m α → reader_t r' m α)
 
+
 instance (r : Type u) (m out) [monad_run out m] : monad_run (λ α, r → out α) (reader_t r m) :=
 ⟨λ α x, run ∘ x.run, λ α a, reader_t.mk (unrun ∘ a)⟩
diff --git a/library/init/category/state.lean b/library/init/category/state.lean
index 8287f78182..26c8d785f3 100644
--- a/library/init/category/state.lean
+++ b/library/init/category/state.lean
@@ -2,6 +2,8 @@
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
+
+The state monad transformer.
 -/
 prelude
 import init.category.alternative init.category.lift
@@ -17,60 +19,62 @@ attribute [pp_using_anonymous_constructor] state_t
 
 namespace state_t
 section
-  variable  {σ : Type u}
-  variable  {m : Type u → Type v}
+  variables {σ : Type u} {m : Type u → Type v}
 
+  -- swap `st` and `x`
   @[inline] protected def run {α : Type u} (st : σ) (x : state_t σ m α) : m (α × σ) :=
   state_t.run' x st
 
   variable  [monad m]
   variables {α β : Type u}
 
-  protected def pure (a : α) : state_t σ m α :=
+  @[inline] protected def pure (a : α) : state_t σ m α :=
   ⟨λ s, pure (a, s)⟩
 
-  protected def bind (act₁ : state_t σ m α) (act₂ : α → state_t σ m β) : state_t σ m β :=
-  ⟨λ s, do (a, new_s) ← act₁.run s,
-           (act₂ a).run new_s⟩
+  @[inline] protected def bind (x : state_t σ m α) (f : α → state_t σ m β) : state_t σ m β :=
+  ⟨λ s, do (a, s') ← x.run s,
+           (f a).run s'⟩
 
   instance : monad (state_t σ m) :=
-  { pure := @state_t.pure σ m _, bind := @state_t.bind σ m _ }
+  { pure := @state_t.pure _ _ _, bind := @state_t.bind _ _ _ }
 
-  protected def orelse [alternative m] (α : Type u) (act₁ act₂ : state_t σ m α) : state_t σ m α :=
-  ⟨λ s, act₁.run s <|> act₂.run s⟩
+  protected def orelse [alternative m] {α : Type u} (x₁ x₂ : state_t σ m α) : state_t σ m α :=
+  ⟨λ s, x₁.run s <|> x₂.run s⟩
 
-  protected def failure [alternative m] (α : Type u) : state_t σ m α :=
+  protected def failure [alternative m] {α : Type u} : state_t σ m α :=
   ⟨λ s, failure⟩
 
   instance [alternative m] : alternative (state_t σ m) :=
-  { failure := @state_t.failure σ m _ _,
-    orelse  := @state_t.orelse σ m _ _,
-    ..state_t.monad }
+  { failure := @state_t.failure _ _ _ _,
+    orelse  := @state_t.orelse _ _ _ _ }
 
-  protected def get : state_t σ m σ :=
-  ⟨λ s, return (s, s)⟩
+  @[inline] protected def get : state_t σ m σ :=
+  ⟨λ s, pure (s, s)⟩
 
-  protected def put : σ → state_t σ m punit :=
-  λ s', ⟨λ s, return (punit.star, s')⟩
+  @[inline] protected def put : σ → state_t σ m punit :=
+  λ s', ⟨λ s, pure (punit.star, s')⟩
 
-  protected def modify (f : σ → σ) : state_t σ m punit :=
-  ⟨λ s, return (punit.star, f s)⟩
+  @[inline] protected def modify (f : σ → σ) : state_t σ m punit :=
+  ⟨λ s, pure (punit.star, f s)⟩
 
-  protected def lift {α : Type u} (t : m α) : state_t σ m α :=
-  ⟨λ s, do a ← t, return (a, s)⟩
+  @[inline] protected def lift {α : Type u} (t : m α) : state_t σ m α :=
+  ⟨λ s, do a ← t, pure (a, s)⟩
 
   instance : has_monad_lift m (state_t σ m) :=
   ⟨@state_t.lift σ m _⟩
 
-  protected def monad_map {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : state_t σ m α → state_t σ m' α :=
+  @[inline] protected def monad_map {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) :
+    state_t σ m α → state_t σ m' α :=
   λ x, ⟨λ st, f (x.run st)⟩
 
   instance (σ m m') [monad m] [monad m'] : monad_functor m m' (state_t σ m) (state_t σ m') :=
   ⟨@state_t.monad_map σ m m' _ _⟩
 
   -- TODO(Sebastian): uses lenses as in https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Zoom ?
-  protected def zoom {σ σ' α : Type u} {m : Type u → Type v} [monad m] (get : σ → σ') (set : σ' → σ → σ) (x : state_t σ' m α) : state_t σ m α :=
-  ⟨λ st, (λ p : α × σ', (p.fst, set p.snd st)) <$> x.run (get st)⟩
+  protected def zoom {σ σ' α : Type u} {m : Type u → Type v} [monad m] (get : σ → σ')
+    (set : σ' → σ → σ) (x : state_t σ' m α) : state_t σ m α :=
+  ⟨λ st, do (a, st') ← x.run (get st),
+            pure (a, set st' st)⟩
 
   instance (ε) [monad_except ε m] : monad_except ε (state_t σ m) :=
   { throw := λ α, state_t.lift ∘ throw,
@@ -81,6 +85,8 @@ end state_t
 @[reducible] protected def state.run {σ α : Type u} (st : σ) (x : state σ α) : α × σ :=
 state_t.run st x
 
+
+/-- A specialization of `monad_lift` to `state_t` that allows `σ` to be inferred. -/
 class monad_state_lift (σ : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
 [has_lift : has_monad_lift_t (state_t σ m) n]
 
@@ -103,13 +109,16 @@ monad_lift (state_t.put st : state_t σ m _)
 monad_lift (state_t.modify f : state_t σ m _)
 end
 
+
+/-- A specialization of `monad_map` to `state_t` that allows `σ` to be inferred. -/
 class monad_state_functor (σ σ' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
 [functor {} : monad_functor_t (state_t σ m) (state_t σ' m) n n']
 
 attribute [instance] monad_state_functor.mk
 local attribute [instance] monad_state_functor.functor
 
-def zoom {σ σ'} {m n n'} [monad m] {α : Type u} (get : σ → σ') (set : σ' → σ → σ) [monad_state_functor σ' σ m n n'] : n α → n' α :=
+def zoom {σ σ'} {m n n'} [monad m] {α : Type u} (get : σ → σ') (set : σ' → σ → σ)
+  [monad_state_functor σ' σ m n n'] : n α → n' α :=
 monad_map $ λ α, (state_t.zoom get set : state_t σ' m α → state_t σ m α)
 
 instance (σ m out) [monad_run out m] : monad_run (λ α, σ → out (α × σ)) (state_t σ m) :=
diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index db12cdc749..4d15ea7218 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -62,8 +62,7 @@ protected def orelse {α : Type u} : option α → option α → option α
 
 instance : alternative option :=
 { failure := @none,
-  orelse  := @option.orelse,
-  ..option.monad }
+  orelse  := @option.orelse }
 
 end option
 
diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean
index f5313980ce..805241ad30 100644
--- a/library/init/meta/vm.lean
+++ b/library/init/meta/vm.lean
@@ -75,7 +75,7 @@ meta constant vm_core.ret {α : Type} : α → vm_core α
 meta constant vm_core.bind {α β : Type} : vm_core α → (α → vm_core β) → vm_core β
 
 meta instance : monad vm_core :=
-{map := @vm_core.map, pure := @vm_core.ret, bind := @vm_core.bind}
+{ map := @vm_core.map, pure := @vm_core.ret, bind := @vm_core.bind }
 
 @[reducible] meta def vm (α : Type) : Type := option_t vm_core α