diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 00f095a6f5..91d7de14d3 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -40,6 +40,7 @@ structure DefView where
   binders       : Syntax
   type?         : Option Syntax
   value         : Syntax
+  deriving?     : Option (Array Syntax) := none
   deriving Inhabited
 
 namespace Command
@@ -51,20 +52,21 @@ def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let (binders, type) := expandOptDeclSig stx[2]
   let modifiers       := modifiers.addAttribute { name := `inline }
   let modifiers       := modifiers.addAttribute { name := `reducible }
-  { ref := stx, kind := DefKind.abbrev, modifiers := modifiers,
-    declId := stx[1], binders := binders, type? := type, value := stx[3] }
+  { ref := stx, kind := DefKind.abbrev, modifiers,
+    declId := stx[1], binders, type? := type, value := stx[3] }
 
 def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView :=
-  -- leading_parser "def " >> declId >> optDeclSig >> declVal
+  -- leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving
   let (binders, type) := expandOptDeclSig stx[2]
-  { ref := stx, kind := DefKind.def, modifiers := modifiers,
-    declId := stx[1], binders := binders, type? := type, value := stx[3] }
+  let deriving? := if stx[4].isNone then none else some stx[4][1].getSepArgs
+  { ref := stx, kind := DefKind.def, modifiers,
+    declId := stx[1], binders, type? := type, value := stx[3], deriving? }
 
 def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "theorem " >> declId >> declSig >> declVal
   let (binders, type) := expandDeclSig stx[2]
-  { ref := stx, kind := DefKind.theorem, modifiers := modifiers,
-    declId := stx[1], binders := binders, type? := some type, value := stx[3] }
+  { ref := stx, kind := DefKind.theorem, modifiers,
+    declId := stx[1], binders, type? := some type, value := stx[3] }
 
 namespace MkInstanceName
 
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 1f477cda20..7119a641e0 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Wojciech Nawrocki
 -/
 import Lean.Elab.Command
+import Lean.Elab.MutualDef
 
 namespace Lean.Elab
 open Command
@@ -35,29 +36,8 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : O
   | none => defaultHandler className typeNames
 
 private def tryApplyDefHandler (className : Name) (declName : Name) : CommandElabM Bool :=
-  open Meta in
   liftTermElabM none do
-    let ConstantInfo.defnInfo info ← getConstInfo declName | return false
-    forallTelescopeReducing info.type fun xs type => do
-      try
-        let instType ← mkAppM className #[mkAppN (Lean.mkConst declName (info.levelParams.map mkLevelParam)) xs]
-        check instType
-        let oldInstType ← mkAppM className #[(mkAppN info.value xs).headBeta]
-        check oldInstType
-        let instVal ← synthInstance oldInstType
-        let instName ← liftMacroM <| mkUnusedBaseName (declName.appendBefore "inst" |>.appendAfter className.getString!)
-        addAndCompile <| Declaration.defnDecl {
-          name        := instName
-          levelParams := info.levelParams
-          type        := instType
-          value       := instVal
-          hints       := info.hints
-          safety      := info.safety
-        }
-        addInstance instName AttributeKind.global (eval_prio default)
-        return true
-      catch _ =>
-        return false
+    Term.processDefDeriving className declName
 
 @[builtinCommandElab «deriving»] def elabDeriving : CommandElab
   | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index c3058eed59..957d4b8210 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -638,30 +638,63 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let newHeaders ← process.run' 1
   newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
 
+def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool := do
+  try
+    let ConstantInfo.defnInfo info ← getConstInfo declName | return false
+    let instType ← mkAppM className #[Lean.mkConst declName (info.levelParams.map mkLevelParam)]
+    Meta.check instType
+    let oldInstType ← mkAppM className #[info.value]
+    Meta.check oldInstType
+    let instVal ← synthInstance oldInstType
+    let instName ← liftMacroM <| mkUnusedBaseName (declName.appendBefore "inst" |>.appendAfter className.getString!)
+    addAndCompile <| Declaration.defnDecl {
+      name        := instName
+      levelParams := info.levelParams
+      type        := instType
+      value       := instVal
+      hints       := info.hints
+      safety      := info.safety
+    }
+    addInstance instName AttributeKind.global (eval_prio default)
+    return true
+  catch _ =>
+    return false
+
 def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv go
   else
     go
-where go := do
-  let scopeLevelNames ← getLevelNames
-  let headers ← elabHeaders views
-  let headers ← levelMVarToParamHeaders views headers
-  let allUserLevelNames := getAllUserLevelNames headers
-  withFunLocalDecls headers fun funFVars => do
-    let values ← elabFunValues headers
-    Term.synthesizeSyntheticMVarsNoPostponing
-    let values ← values.mapM (instantiateMVars ·)
-    let headers ← headers.mapM instantiateMVarsAtHeader
-    let letRecsToLift ← getLetRecsToLift
-    let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
-    checkLetRecsToLiftTypes funFVars letRecsToLift
-    withUsed vars headers values letRecsToLift fun vars => do
-      let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
-      let preDefs ← levelMVarToParamPreDecls preDefs
-      let preDefs ← instantiateMVarsAtPreDecls preDefs
-      let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
-      addPreDefinitions preDefs
+where
+  go := do
+    let scopeLevelNames ← getLevelNames
+    let headers ← elabHeaders views
+    let headers ← levelMVarToParamHeaders views headers
+    let allUserLevelNames := getAllUserLevelNames headers
+    withFunLocalDecls headers fun funFVars => do
+      let values ← elabFunValues headers
+      Term.synthesizeSyntheticMVarsNoPostponing
+      let values ← values.mapM (instantiateMVars ·)
+      let headers ← headers.mapM instantiateMVarsAtHeader
+      let letRecsToLift ← getLetRecsToLift
+      let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
+      checkLetRecsToLiftTypes funFVars letRecsToLift
+      withUsed vars headers values letRecsToLift fun vars => do
+        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+        let preDefs ← levelMVarToParamPreDecls preDefs
+        let preDefs ← instantiateMVarsAtPreDecls preDefs
+        let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+        addPreDefinitions preDefs
+        processDeriving headers
+
+  processDeriving (headers : Array DefViewElabHeader) := do
+    for header in headers, view in views do
+      if let some classNamesStx := view.deriving? then
+        for classNameStx in classNamesStx do
+          let className ← resolveGlobalConstNoOverload classNameStx
+          withRef classNameStx do
+            unless (← processDefDeriving className header.declName) do
+              throwError "failed to synthesize instance '{className}' for '{header.declName}'"
 
 end Term
 namespace Command
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 17edb49787..4f4255f2c4 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -41,7 +41,7 @@ def declValSimple    := leading_parser " :=\n" >> termParser >> optional Term.wh
 def declValEqns      := leading_parser Term.matchAltsWhereDecls
 def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls
 def «abbrev»         := leading_parser "abbrev " >> declId >> optDeclSig >> declVal
-def optDefDeriving   := leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
+def optDefDeriving   := optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
 def «def»            := leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving
 def «theorem»        := leading_parser "theorem " >> declId >> declSig >> declVal
 def «constant»       := leading_parser "constant " >> declId >> declSig >> optional declValSimple
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 52f462a61e..0de22d176a 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -8,8 +8,8 @@ StxQuot.lean:8:12: error: expected command, identifier or term
 "(«term_+_» (numLit \"1\") \"+\" (numLit \"1\"))"
 StxQuot.lean:18:15: error: expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])\n  (Command.optDefDeriving [])))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])\n   (Command.optDefDeriving [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])\n   (Command.optDefDeriving [])))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])\n   []))]"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
@@ -18,8 +18,8 @@ StxQuot.lean:18:15: error: expected term
 "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
 "(«term_+_» (numLit \"2\") \"+\" (numLit \"1\"))"
 "(«term_+_» («term_+_» (numLit \"1\") \"+\" (numLit \"2\")) \"+\" (numLit \"1\"))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])\n  (Command.optDefDeriving [])))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])\n   (Command.optDefDeriving [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])\n   (Command.optDefDeriving [])))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])\n   []))]"
 "0"
 0
 1
diff --git a/tests/lean/defInst.lean b/tests/lean/defInst.lean
index 8ebf47a0b6..923fb6752c 100644
--- a/tests/lean/defInst.lean
+++ b/tests/lean/defInst.lean
@@ -12,3 +12,22 @@ deriving instance BEq, Repr for Foo
 #eval test 4
 
 #check fun (x y : Foo) => x == y
+
+def Boo := List (String × String)
+  deriving BEq, Repr
+
+def mkBoo (s : String) : Boo :=
+  [(s, s)]
+
+#eval mkBoo "hello"
+
+#eval mkBoo "hell" == mkBoo "hello"
+#eval mkBoo "hello" == mkBoo "hello"
+
+def M := ReaderT String (StateT Nat IO)
+  deriving Monad
+
+#print instMMonad
+
+def action : M Unit := do
+  pure ()
diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out
index 0dc2399dd4..6c75ff3937 100644
--- a/tests/lean/defInst.lean.expected.out
+++ b/tests/lean/defInst.lean.expected.out
@@ -5,3 +5,8 @@ defInst.lean:8:26-8:32: error: failed to synthesize instance
 fun x y => sorry : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool
+[("hello", "hello")]
+false
+true
+def instMMonad : Monad M :=
+ReaderT.instMonadReaderT