diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index c3637ca046..ca45e9b4db 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -63,66 +63,52 @@ abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
 abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
   CoeSort.coe a
 
-instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ := {
-  coe := fun a => coeB (coeTC a : β)
-}
+instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ where
+  coe a := coeB (coeTC a : β)
 
-instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β := {
-  coe := fun a => coeB a
-}
+instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β where
+  coe a := coeB a
 
-instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ := {
+instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ where
   coe := coeTail (coeTC (coeHead a : β) : δ)
-}
 
-instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ  := {
+instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ  where
   coe := coeTC (coeHead a : β)
-}
 
-instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ := {
+instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ where
   coe := coeTail (coeTC a : β)
-}
 
-instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β := {
+instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β where
   coe := coeHead a
-}
 
-instance coeOfTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : CoeT α a β := {
+instance coeOfTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : CoeT α a β where
   coe := coeTail a
-}
 
-instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α β] : CoeT α a β := {
+instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α β] : CoeT α a β where
   coe := coeTC a
-}
 
-instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β := {
+instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β where
   coe := coeD a
-}
 
-instance coeId {α : Sort u} (a : α) : CoeT α a α := {
+instance coeId {α : Sort u} (a : α) : CoeT α a α where
   coe := a
-}
 
 /- Basic instances -/
 
-@[inline] instance boolToProp : Coe Bool Prop := {
-  coe := fun b => b = true
-}
+@[inline] instance boolToProp : Coe Bool Prop where
+  coe b := b = true
 
 @[inline] instance coeDecidableEq (x : Bool) : Decidable (coe x) :=
-inferInstanceAs (Decidable (x = true))
+  inferInstanceAs (Decidable (x = true))
 
-instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool := {
+instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
   coe := decide p
-}
 
-instance optionCoe {α : Type u} : CoeTail α (Option α) := {
+instance optionCoe {α : Type u} : CoeTail α (Option α) where
   coe := some
-}
 
-instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α := {
-  coe := fun v => v.val
-}
+instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α where
+  coe v := v.val
 
 /- Coe & OfNat bridge -/
 
diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 1232b0db16..7f3d120303 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -47,7 +47,8 @@ class ToBool (α : Type u) where
 
 export ToBool (toBool)
 
-instance : ToBool Bool := ⟨id⟩
+instance : ToBool Bool where
+  toBool b := b
 
 @[macroInline] def bool {β : Type u} {α : Type v} [ToBool β] (f t : α) (b : β) : α :=
   match toBool b with
@@ -90,7 +91,6 @@ instance (m n o) [MonadControlT m n] [MonadControl n o] : MonadControlT m o wher
   liftWith f := MonadControl.liftWith fun x₂ => liftWith fun x₁ => f (x₁ ∘ x₂)
   restoreM := MonadControl.restoreM ∘ restoreM
 
-
 instance (m : Type u → Type v) [Pure m] : MonadControlT m m where
   stM α := α
   liftWith f := f fun x => x
diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean
index 972c46b286..2231c439a7 100644
--- a/src/Init/Control/EState.lean
+++ b/src/Init/Control/EState.lean
@@ -12,17 +12,15 @@ namespace EStateM
 
 variables {ε σ α : Type u}
 
-instance [ToString ε] [ToString α] : ToString (Result ε σ α) := {
-  toString := fun
+instance [ToString ε] [ToString α] : ToString (Result ε σ α) where
+  toString
     | Result.ok a _    => "ok: " ++ toString a
     | Result.error e _ => "error: " ++ toString e
-}
 
-instance [Repr ε] [Repr α] : Repr (Result ε σ α) := {
-  repr := fun
+instance [Repr ε] [Repr α] : Repr (Result ε σ α) where
+  repr
     | Result.error e _ => "(error " ++ repr e ++ ")"
     | Result.ok a _    => "(ok " ++ repr a ++ ")"
-}
 
 end EStateM
 
diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean
index bca3e94fb7..66c07db513 100644
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@@ -14,11 +14,10 @@ def Id (type : Type u) : Type u := type
 
 namespace Id
 
-instance : Monad Id := {
-  pure := fun x => x
-  bind := fun x f => f x
-  map  := fun f x => f x
-}
+instance : Monad Id where
+  pure x := x
+  bind x f := f x
+  map f x := f x
 
 @[inline] protected def run (x : Id α) : α := x
 
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index f71edfecba..0a5e94a006 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -18,19 +18,16 @@ namespace ReaderT
 @[inline] protected def failure [Alternative m] : ReaderT ρ m α :=
   fun s => failure
 
-instance [Monad m] [Alternative m] : Alternative (ReaderT ρ m) := {
+instance [Monad m] [Alternative m] : Alternative (ReaderT ρ m) where
   failure := ReaderT.failure
   orElse  := ReaderT.orElse
-}
 
 end ReaderT
 
-instance : MonadControl m (ReaderT ρ m) := {
+instance : MonadControl m (ReaderT ρ m) where
   stM      := id
-  liftWith := fun f ctx => f fun x => x ctx
-  restoreM := fun x ctx => x
-}
+  liftWith f ctx := f fun x => x ctx
+  restoreM x ctx := x
 
-instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) := {
-  tryFinally' := fun x h ctx => tryFinally' (x ctx) (fun a? => h a? ctx)
-}
+instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
+  tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index 3a414d6cb6..d58d30ddb3 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -8,24 +8,20 @@ import Init.Data.UInt
 import Init.Data.String
 universes u
 
-instance : Hashable Nat := {
-  hash := fun n => USize.ofNat n
-}
+instance : Hashable Nat where
+  hash n := USize.ofNat n
 
-instance [Hashable α] [Hashable β] : Hashable (α × β) := {
-  hash := fun (a, b) => mixHash (hash a) (hash b)
-}
+instance [Hashable α] [Hashable β] : Hashable (α × β) where
+  hash | (a, b) => mixHash (hash a) (hash b)
 
 protected def Option.hash [Hashable α] : Option α → USize
   | none   => 11
   | some a => mixHash (hash a) 13
 
-instance [Hashable α] : Hashable (Option α) := {
-  hash := fun
+instance [Hashable α] : Hashable (Option α) where
+  hash
     | none   => 11
     | some a => mixHash (hash a) 13
-}
 
-instance [Hashable α] : Hashable (List α) := {
-  hash := fun as => as.foldl (fun r a => mixHash r (hash a)) 7
-}
+instance [Hashable α] : Hashable (List α) where
+  hash as := as.foldl (fun r a => mixHash r (hash a)) 7
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 42382b39e0..71274b859e 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -270,8 +270,8 @@ def mkSep (a : Array Syntax) (sep : Syntax) : Syntax :=
 def SepArray.ofElems {sep} (elems : Array Syntax) : SepArray sep :=
 ⟨mkSepArray elems (mkAtom sep)⟩
 
-instance (sep) : Coe (Array Syntax) (SepArray sep) :=
-⟨SepArray.ofElems⟩
+instance (sep) : Coe (Array Syntax) (SepArray sep) where
+  coe := SepArray.ofElems
 
 /-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/
 def mkApp (fn : Syntax) : (args : Array Syntax) → Syntax
@@ -613,23 +613,26 @@ private def quoteName : Name → Syntax
 
 instance : Quote Name := ⟨quoteName⟩
 
-instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) :=
-  ⟨fun ⟨a, b⟩ => Syntax.mkCApp ``Prod.mk #[quote a, quote b]⟩
+instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) where
+  quote
+    | ⟨a, b⟩ => Syntax.mkCApp ``Prod.mk #[quote a, quote b]
 
 private def quoteList {α : Type} [Quote α] : List α → Syntax
   | []      => mkCIdent ``List.nil
   | (x::xs) => Syntax.mkCApp ``List.cons #[quote x, quoteList xs]
 
-instance {α : Type} [Quote α] : Quote (List α) := ⟨quoteList⟩
+instance {α : Type} [Quote α] : Quote (List α) where
+  quote := quoteList
 
-instance {α : Type} [Quote α] : Quote (Array α) :=
-  ⟨fun xs => Syntax.mkCApp ``List.toArray #[quote xs.toList]⟩
+instance {α : Type} [Quote α] : Quote (Array α) where
+  quote xs := Syntax.mkCApp ``List.toArray #[quote xs.toList]
 
 private def quoteOption {α : Type} [Quote α] : Option α → Syntax
   | none     => mkIdent ``none
   | (some x) => Syntax.mkCApp ``some #[quote x]
 
-instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) := ⟨quoteOption⟩
+instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) where
+  quote := quoteOption
 
 end Lean
 
@@ -684,10 +687,10 @@ end Array
 namespace Lean.Syntax.SepArray
 
 def getElems {sep} (sa : SepArray sep) : Array Syntax :=
-sa.elemsAndSeps.getSepElems
+  sa.elemsAndSeps.getSepElems
 
-instance (sep) : Coe (SepArray sep) (Array Syntax) :=
-⟨getElems⟩
+instance (sep) : Coe (SepArray sep) (Array Syntax) where
+  coe := getElems
 
 end Lean.Syntax.SepArray
 
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index cc9a9c6135..c3ccde21e3 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -172,10 +172,9 @@ def sizeofMeasure (α : Sort u) [SizeOf α] : α → α → Prop :=
 def sizeofMeasureWf (α : Sort u) [SizeOf α] : WellFounded (sizeofMeasure α) :=
   measureWf sizeOf
 
-instance hasWellFoundedOfSizeOf (α : Sort u) [SizeOf α] : WellFoundedRelation α := {
-  r := sizeofMeasure α,
+instance hasWellFoundedOfSizeOf (α : Sort u) [SizeOf α] : WellFoundedRelation α where
+  r := sizeofMeasure α
   wf := sizeofMeasureWf α
-}
 
 namespace Prod
 open WellFounded
@@ -228,10 +227,9 @@ def rprodWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Rprod ra
 
 end
 
-instance {α : Type u} {β : Type v} [s₁ : WellFoundedRelation α] [s₂ : WellFoundedRelation β] : WellFoundedRelation (α × β) := {
-  r  := Lex s₁.r s₂.r,
+instance {α : Type u} {β : Type v} [s₁ : WellFoundedRelation α] [s₂ : WellFoundedRelation β] : WellFoundedRelation (α × β) where
+  r  := Lex s₁.r s₂.r
   wf := lexWf s₁.wf s₂.wf
-}
 
 end Prod
 
@@ -274,7 +272,7 @@ def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
   Lex r (fun a => s)
 
 def lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
-    WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
+  WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
 end
 
 section
@@ -318,9 +316,8 @@ def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → P
   RevLex.right _ _ h
 end
 
-instance WellFoundedRelation {α : Type u} {β : α → Type v} [s₁ : WellFoundedRelation α] [s₂ : ∀ a, WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β) := {
-  r  := Lex s₁.r (fun a => (s₂ a).r),
+instance WellFoundedRelation {α : Type u} {β : α → Type v} [s₁ : WellFoundedRelation α] [s₂ : ∀ a, WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β) where
+  r  := Lex s₁.r (fun a => (s₂ a).r)
   wf := lexWf s₁.wf (fun a => (s₂ a).wf)
-}
 
 end PSigma
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index b967f17a7e..e7190d3061 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -35,51 +35,44 @@ abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception)
 
 instance : Inhabited (CoreM α) := ⟨fun _ _ => throw arbitrary⟩
 
-instance : MonadRef CoreM := {
-  getRef  := do let ctx ← read; pure ctx.ref,
-  withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
-}
+instance : MonadRef CoreM where
+  getRef := return (← read).ref
+  withRef ref x := withReader (fun ctx => { ctx with ref := ref }) x
 
-instance : MonadEnv CoreM := {
-  getEnv    := do pure (← get).env,
-  modifyEnv := fun f => modify fun s => { s with env := f s.env }
-}
 
-instance : MonadOptions CoreM := {
-  getOptions := do pure (← read).options
-}
+instance : MonadEnv CoreM where
+  getEnv := return (← get).env
+  modifyEnv f := modify fun s => { s with env := f s.env }
 
-instance : AddMessageContext CoreM := {
+instance : MonadOptions CoreM where
+  getOptions := return (← read).options
+
+instance : AddMessageContext CoreM where
   addMessageContext := addMessageContextPartial
-}
 
-instance : MonadNameGenerator CoreM := {
-  getNGen := do pure (← get).ngen,
-  setNGen := fun ngen => modify fun s => { s with ngen := ngen } }
+instance : MonadNameGenerator CoreM where
+  getNGen := return (← get).ngen
+  setNGen ngen := modify fun s => { s with ngen := ngen }
 
-instance : MonadRecDepth CoreM := {
-  withRecDepth   := fun d x => withReader (fun ctx => { ctx with currRecDepth := d }) x,
-  getRecDepth    := do pure (← read).currRecDepth,
-  getMaxRecDepth := do pure (← read).maxRecDepth
-}
+instance : MonadRecDepth CoreM where
+  withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
+  getRecDepth := return (← read).currRecDepth
+  getMaxRecDepth := return (← read).maxRecDepth
 
-instance : MonadResolveName CoreM := {
-  getCurrNamespace := do pure (← read).currNamespace,
-  getOpenDecls     := do pure (← read).openDecls
-}
+instance : MonadResolveName CoreM where
+  getCurrNamespace := return (← read).currNamespace
+  getOpenDecls := return (← read).openDecls
 
 @[inline] def liftIOCore (x : IO α) : CoreM α := do
   let ref ← getRef
   IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x
 
-instance : MonadLift IO CoreM := {
+instance : MonadLift IO CoreM where
   monadLift := liftIOCore
-}
 
-instance : MonadTrace CoreM := {
-  getTraceState    := do pure (← get).traceState,
-  modifyTraceState := fun f => modify fun s => { s with traceState := f s.traceState }
-}
+instance : MonadTrace CoreM where
+  getTraceState := return (← get).traceState
+  modifyTraceState f := modify fun s => { s with traceState := f s.traceState }
 
 private def mkFreshNameImp (n : Name) : CoreM Name := do
   let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
@@ -101,12 +94,11 @@ def mkFreshUserName [MonadLiftT CoreM m] (n : Name) : m Name :=
   | Except.error (Exception.internal id _) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
   | Except.ok a => pure a
 
-instance [MetaEval α] : MetaEval (CoreM α) := {
-  eval := fun env opts x _ => do
+instance [MetaEval α] : MetaEval (CoreM α) where
+  eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
     let (a, s) ← x.toIO { maxRecDepth := getMaxRecDepth opts, options := opts } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
-}
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 15a3932b91..924ae8c565 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -36,9 +36,9 @@ structure State where
 instance : Inhabited State := ⟨{ env := arbitrary, maxRecDepth := 0 }⟩
 
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
-  env := env,
-  messages := messages,
-  scopes := [{ header := "", opts := opts }],
+  env := env
+  messages := messages
+  scopes := [{ header := "", opts := opts }]
   maxRecDepth := getMaxRecDepth opts
 }
 
@@ -61,38 +61,33 @@ abbrev Linter := Syntax → CommandElabM Unit
 builtin_initialize lintersRef : IO.Ref (Array Linter) ← IO.mkRef #[]
 
 def addLinter (l : Linter) : IO Unit := do
-let ls ← lintersRef.get
-lintersRef.set (ls.push l)
+  let ls ← lintersRef.get
+  lintersRef.set (ls.push l)
 
-instance : MonadEnv CommandElabM := {
-  getEnv    := do pure (← get).env,
-  modifyEnv := fun f => modify fun s => { s with env := f s.env }
-}
+instance : MonadEnv CommandElabM where
+  getEnv := do pure (← get).env
+  modifyEnv f := modify fun s => { s with env := f s.env }
 
-instance : MonadOptions CommandElabM := {
+instance : MonadOptions CommandElabM where
   getOptions := do pure (← get).scopes.head!.opts
-}
 
-protected def getRef : CommandElabM Syntax := do
-  pure (← read).ref
+protected def getRef : CommandElabM Syntax :=
+  return (← read).ref
 
-instance : AddMessageContext CommandElabM := {
+instance : AddMessageContext CommandElabM where
   addMessageContext := addMessageContextPartial
-}
 
-instance : MonadRef CommandElabM := {
-  getRef     := Command.getRef,
-  withRef    := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
-}
+instance : MonadRef CommandElabM where
+  getRef := Command.getRef
+  withRef ref x := withReader (fun ctx => { ctx with ref := ref }) x
 
-instance : AddErrorMessageContext CommandElabM := {
-  add := fun ref msg => do
+instance : AddErrorMessageContext CommandElabM where
+  add ref msg := do
     let ctx ← read
     let ref := getBetterRef ref ctx.macroStack
     let msg ← addMessageContext msg
     let msg ← addMacroStack msg ctx.macroStack
-    pure (ref, msg)
-}
+    return (ref, msg)
 
 def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
   mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
@@ -132,21 +127,19 @@ instance : MonadLiftT IO CommandElabM := { monadLift := liftIO }
 
 def getScope : CommandElabM Scope := do pure (← get).scopes.head!
 
-instance : MonadResolveName CommandElabM := {
-  getCurrNamespace := do pure (← getScope).currNamespace,
-  getOpenDecls     := do pure (← getScope).openDecls
-}
+instance : MonadResolveName CommandElabM where
+  getCurrNamespace := return (← getScope).currNamespace
+  getOpenDecls     := return (← getScope).openDecls
 
-instance : MonadLog CommandElabM := {
-  getRef      := getRef,
-  getFileMap  := do pure (← read).fileMap,
-  getFileName := do pure (← read).fileName,
-  logMessage  := fun msg => do
+instance : MonadLog CommandElabM where
+  getRef      := getRef
+  getFileMap  := return (← read).fileMap
+  getFileName := return (← read).fileName
+  logMessage msg := do
     let currNamespace ← getCurrNamespace
     let openDecls ← getOpenDecls
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data }
     modify fun s => { s with messages := s.messages.add msg }
-}
 
 def runLinters (stx : Syntax) : CommandElabM Unit := do
   let linters ← lintersRef.get
@@ -167,11 +160,10 @@ protected def getMainModule     : CommandElabM Name := do pure (← getEnv).main
   let fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }))
   withReader (fun ctx => { ctx with currMacroScope := fresh }) x
 
-instance : MonadQuotation CommandElabM := {
-  getCurrMacroScope   := Command.getCurrMacroScope,
-  getMainModule       := Command.getMainModule,
+instance : MonadQuotation CommandElabM where
+  getCurrMacroScope   := Command.getCurrMacroScope
+  getMainModule       := Command.getMainModule
   withFreshMacroScope := Command.withFreshMacroScope
-}
 
 unsafe def mkCommandElabAttributeUnsafe : IO (KeyedDeclsAttribute CommandElab) :=
   mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"
@@ -192,17 +184,15 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → C
 @[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
   withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
 
-instance : MonadMacroAdapter CommandElabM := {
-  getCurrMacroScope := getCurrMacroScope,
-  getNextMacroScope := do pure (← get).nextMacroScope,
-  setNextMacroScope := fun next => modify fun s => { s with nextMacroScope := next }
-}
+instance : MonadMacroAdapter CommandElabM where
+  getCurrMacroScope := getCurrMacroScope
+  getNextMacroScope := return (← get).nextMacroScope
+  setNextMacroScope next := modify fun s => { s with nextMacroScope := next }
 
-instance : MonadRecDepth CommandElabM := {
-  withRecDepth   := fun d x => withReader (fun ctx => { ctx with currRecDepth := d }) x,
-  getRecDepth    := return (← read).currRecDepth,
+instance : MonadRecDepth CommandElabM where
+  withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
+  getRecDepth := return (← read).currRecDepth
   getMaxRecDepth := return (← get).maxRecDepth
-}
 
 @[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
   try
@@ -219,7 +209,7 @@ instance : MonadRecDepth CommandElabM := {
 builtin_initialize registerTraceClass `Elab.command
 
 partial def elabCommand (stx : Syntax) : CommandElabM Unit :=
-  withLogging $ withRef stx $ withIncRecDepth $ withFreshMacroScope do
+  withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
     runLinters stx
     match stx with
     | Syntax.node k args =>
@@ -258,11 +248,11 @@ private def mkMetaContext : Meta.Context := {
 }
 
 private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context :=
-  let scope      := s.scopes.head!;
-  { macroStack     := ctx.macroStack,
-    fileName       := ctx.fileName,
-    fileMap        := ctx.fileMap,
-    currMacroScope := ctx.currMacroScope,
+  let scope      := s.scopes.head!
+  { macroStack     := ctx.macroStack
+    fileName       := ctx.fileName
+    fileMap        := ctx.fileMap
+    currMacroScope := ctx.currMacroScope
     declName?      := declName? }
 
 private def addTraceAsMessages (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog :=
@@ -285,9 +275,9 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
   let x : EIO _ _      := x.run (mkCoreContext ctx s) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope }
   let (((ea, termS), _), coreS) ← liftEIO x
   modify fun s => { s with
-    env            := coreS.env,
-    messages       := addTraceAsMessages ctx (messages ++ termS.messages) coreS.traceState,
-    nextMacroScope := coreS.nextMacroScope,
+    env            := coreS.env
+    messages       := addTraceAsMessages ctx (messages ++ termS.messages) coreS.traceState
+    nextMacroScope := coreS.nextMacroScope
     ngen           := coreS.ngen
   }
   match ea with
@@ -472,7 +462,7 @@ def elabOpenOnly (n : SyntaxNode) : CommandElabM Unit := do
     if env.contains declName then
       addOpenDecl (OpenDecl.explicit id declName)
     else
-      withRef idStx $ logUnknownDecl declName
+      withRef idStx do logUnknownDecl declName
 
 -- `open` id `hiding` id+
 def elabOpenHiding (n : SyntaxNode) : CommandElabM Unit := do
@@ -480,13 +470,13 @@ def elabOpenHiding (n : SyntaxNode) : CommandElabM Unit := do
   let ns ← resolveNamespace ns
   let idsStx := n.getArg 2
   let env ← getEnv
-  let ids : List Name ← idsStx.foldArgsM (fun idStx ids => do
+  let ids ← idsStx.foldArgsM (fun idStx ids => do
     let id := idStx.getId
     let declName := ns ++ id
     if env.contains declName then
       pure (id::ids)
     else do
-      withRef idStx $ logUnknownDecl declName
+      withRef idStx do logUnknownDecl declName
       pure ids)
     []
   addOpenDecl (OpenDecl.simple ns ids)
@@ -504,7 +494,7 @@ def elabOpenRenaming (n : SyntaxNode) : CommandElabM Unit := do
     if env.contains declName then
       addOpenDecl (OpenDecl.explicit toId declName)
     else
-      withRef stx $ logUnknownDecl declName
+      withRef stx do logUnknownDecl declName
 
 @[builtinCommandElab «open»] def elabOpen : CommandElab := fun n => do
   let body := (n.getArg 1).asNode
@@ -538,7 +528,7 @@ open Meta
 
 @[builtinCommandElab Lean.Parser.Command.check] def elabCheck : CommandElab := fun stx => do
   let term := stx[1]
-  withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
+  withoutModifyingEnv $ runTermElabM (some `_check) fun _ => do
     let e ← Term.elabTerm term none
     Term.synthesizeSyntheticMVarsNoPostponing
     let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
@@ -548,7 +538,7 @@ open Meta
 
 @[builtinCommandElab Lean.Parser.Command.reduce] def elabReduce : CommandElab := fun stx => do
   let term := stx[1]
-  withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
+  withoutModifyingEnv $ runTermElabM (some `_check) fun _ => do
     let e ← Term.elabTerm term none
     Term.synthesizeSyntheticMVarsNoPostponing
     let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
@@ -582,7 +572,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     throwError "unexpected success"
 
 @[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab := fun stx =>
-  failIfSucceeds $ elabCheck stx
+  failIfSucceeds <| elabCheck stx
 
 unsafe def elabEvalUnsafe : CommandElab := fun stx => do
   let ref  := stx
@@ -644,7 +634,7 @@ constant elabEval : CommandElab
     pure ()
 
 def setOption (optionName : Name) (val : DataValue) : CommandElabM Unit := do
-  let decl ← liftIO $ getOptionDecl optionName
+  let decl ← liftIO <| getOptionDecl optionName
   unless decl.defValue.sameCtor val do throwError "type mismatch at set_option"
   modifyScope fun scope => { scope with opts := scope.opts.insert optionName val }
   match optionName, val with
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 67a43d0cb5..d2b8cffebb 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -674,7 +674,8 @@ def replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr :=
 def replaceFVars (e : Expr) (fvars : Array Expr) (vs : Array Expr) : Expr :=
   (e.abstract fvars).instantiateRev vs
 
-instance : ToString Expr := ⟨Expr.dbgToString⟩
+instance : ToString Expr where
+  toString := Expr.dbgToString
 
 -- TODO: should not use dbgToString, but constructors.
 instance : Repr Expr := ⟨Expr.dbgToString⟩
diff --git a/src/Lean/InternalExceptionId.lean b/src/Lean/InternalExceptionId.lean
index 1d3e81cf4c..e71778772f 100644
--- a/src/Lean/InternalExceptionId.lean
+++ b/src/Lean/InternalExceptionId.lean
@@ -9,8 +9,8 @@ structure InternalExceptionId where
   idx : Nat := 0
 
 instance : Inhabited InternalExceptionId := ⟨{}⟩
-instance : BEq InternalExceptionId :=
-  ⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩
+instance : BEq InternalExceptionId where
+  beq id₁ id₂ := id₁.idx == id₂.idx
 
 builtin_initialize internalExceptionsRef : IO.Ref (Array Name) ← IO.mkRef #[]
 
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index ccb54a9c08..3a19810a26 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -21,15 +21,13 @@ match (← MonadCache.findCached? a) with
     MonadCache.cache a b
     pure b
 
-instance {α β ρ : Type} {m : Type → Type} [MonadCache α β m] : MonadCache α β (ReaderT ρ m) := {
-  findCached? := fun a r   => MonadCache.findCached? a,
-  cache       := fun a b r => MonadCache.cache a b
-}
+instance {α β ρ : Type} {m : Type → Type} [MonadCache α β m] : MonadCache α β (ReaderT ρ m) where
+  findCached? a r := MonadCache.findCached? a
+  cache a b r := MonadCache.cache a b
 
-instance {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : MonadCache α β (ExceptT ε m) := {
-  findCached? := fun a   => ExceptT.lift $ MonadCache.findCached? a,
-  cache       := fun a b => ExceptT.lift $ MonadCache.cache a b
-}
+instance {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : MonadCache α β (ExceptT ε m) where
+  findCached? a := ExceptT.lift $ MonadCache.findCached? a
+  cache a b := ExceptT.lift $ MonadCache.cache a b
 
 open Std (HashMap)
 
@@ -48,10 +46,9 @@ namespace MonadHashMapCacheAdapter
 @[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
   modifyCache fun s => s.insert a b
 
-instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m := {
-  findCached? := MonadHashMapCacheAdapter.findCached?,
+instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
+  findCached? := MonadHashMapCacheAdapter.findCached?
   cache       := MonadHashMapCacheAdapter.cache
-}
 
 end MonadHashMapCacheAdapter
 
@@ -61,10 +58,9 @@ namespace MonadCacheT
 
 variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
 
-instance  : MonadHashMapCacheAdapter α β (MonadCacheT α β m) := {
-  getCache    := (get : StateRefT' ..),
-  modifyCache := fun f => (modify f : StateRefT' ..)
-}
+instance  : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where
+  getCache := (get : StateRefT' ..)
+  modifyCache f := (modify f : StateRefT' ..)
 
 @[inline] def run {σ} (x : MonadCacheT α β m σ) : m σ :=
   x.run' Std.mkHashMap
@@ -85,10 +81,9 @@ namespace MonadStateCacheT
 
 variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
 
-instance  : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) := {
-  getCache    := (get : StateT ..),
-  modifyCache := fun f => (modify f : StateT ..)
-}
+instance  : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where
+  getCache := (get : StateT ..)
+  modifyCache f := (modify f : StateT ..)
 
 @[inline] def run {σ} (x : MonadStateCacheT α β m σ) : m σ :=
   x.run' Std.mkHashMap