diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 37dcd11aa6..5cca3d0ad0 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -89,14 +89,14 @@ class MonadControlT (m : Type u → Type v) (n : Type u → Type w) :=
 export MonadControlT (stM liftWith restoreM)
 
 instance (m n o) [MonadControlT m n] [MonadControl n o] : MonadControlT m o := {
-  stM      := fun α => stM m n (MonadControl.stM n o α),
-  liftWith := fun f => MonadControl.liftWith fun x₂ => liftWith fun x₁ => f (x₁ ∘ x₂),
+  stM      := fun α => stM m n (MonadControl.stM n o α)
+  liftWith := fun 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 := {
-  stM      := fun α => α,
-  liftWith := fun f => f fun x => x,
+  stM      := fun α => α
+  liftWith := fun f => f fun x => x
   restoreM := fun x => pure x
 }
 
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 4e6febb5bb..2d8e97d578 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -60,8 +60,8 @@ variables {ε : Type u}
   | Except.error e => handle e
 
 instance : Monad (Except ε) := {
-  pure := Except.pure,
-  bind := Except.bind,
+  pure := Except.pure
+  bind := Except.bind
   map  := Except.map
 }
 
@@ -106,8 +106,8 @@ instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
 instance : MonadFunctor m (ExceptT ε m) := ⟨fun f x => f x⟩
 
 instance : Monad (ExceptT ε m) := {
-  pure := ExceptT.pure,
-  bind := ExceptT.bind,
+  pure := ExceptT.pure
+  bind := ExceptT.bind
   map  := ExceptT.map
 }
 
@@ -117,17 +117,17 @@ instance : Monad (ExceptT ε m) := {
 end ExceptT
 
 instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) := {
-  throw    := fun e        => ExceptT.mk <| throwThe ε₁ e,
+  throw    := fun e        => ExceptT.mk <| throwThe ε₁ e
   tryCatch := fun x handle => ExceptT.mk <| tryCatchThe ε₁ x handle
 }
 
 instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) := {
-  throw    := fun e => ExceptT.mk <| pure (Except.error e),
+  throw    := fun e => ExceptT.mk <| pure (Except.error e)
   tryCatch := ExceptT.tryCatch
 }
 
 instance (ε) : MonadExceptOf ε (Except ε) := {
-  throw    := Except.error,
+  throw    := Except.error
   tryCatch := Except.tryCatch
 }
 
@@ -145,8 +145,8 @@ end MonadExcept
   tryCatch (do let a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
 
 instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) := {
-  stM      := Except ε,
-  liftWith := fun f => liftM <| f fun x => x.run,
+  stM      := Except ε
+  liftWith := fun f => liftM <| f fun x => x.run
   restoreM := fun x => x
 }
 
diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean
index 96d146fb44..519bc25bc0 100644
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@@ -19,14 +19,14 @@ namespace Id
 @[inline] protected def map {α β : Type u} (f : α → β) (x : Id α) : Id β := f x
 
 instance : Monad Id := {
-  pure := Id.pure,
-  bind := Id.bind,
+  pure := Id.pure
+  bind := Id.bind
   map  := Id.map
 }
 
 @[inline] protected def run {α : Type u} (x : Id α) : α := x
 
 instance {α} [OfNat α] : OfNat (Id α) :=
-inferInstanceAs (OfNat α)
+  inferInstanceAs (OfNat α)
 
 end Id
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 0f0111011e..091b302a39 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -29,7 +29,7 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u}
   pure (some a)
 
 instance : Monad (OptionT m) := {
-  pure := OptionT.pure,
+  pure := OptionT.pure
   bind := OptionT.bind
 }
 
@@ -42,7 +42,7 @@ instance : Monad (OptionT m) := {
   pure none
 
 instance : Alternative (OptionT m) := {
-  failure := OptionT.fail,
+  failure := OptionT.fail
   orElse  := OptionT.orElse
 }
 
@@ -58,7 +58,7 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
   pure a
 
 instance : MonadExceptOf Unit (OptionT m) := {
-  throw    := fun _ => OptionT.fail,
+  throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 }
 
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index 0808ef7c58..11eab3df6d 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -28,7 +28,7 @@ section
 variables {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u}
 
 instance [Alternative m] : Alternative (ReaderT ρ m) := {
-  failure := ReaderT.failure,
+  failure := ReaderT.failure
   orElse  := ReaderT.orElse
 }
 
@@ -36,9 +36,9 @@ end
 end ReaderT
 
 instance (ρ : Type u) (m : Type u → Type v) : MonadControl m (ReaderT ρ m) := {
-  stM      := id,
-  liftWith := fun f ctx => f fun x => x ctx,
-  restoreM := fun x ctx => x,
+  stM      := id
+  liftWith := fun f ctx => f fun x => x ctx
+  restoreM := fun x ctx => x
 }
 
 instance ReaderT.tryFinally {m : Type u → Type v} {ρ : Type u} [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) := {
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index 05917abcef..3a6369921f 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -46,9 +46,9 @@ variables [Monad m] {α β : Type u}
   fun s => do let (a, s) ← x s; pure (f a, s)
 
 instance : Monad (StateT σ m) := {
-  pure := StateT.pure,
-  bind := StateT.bind,
-   map := StateT.map
+  pure := StateT.pure
+  bind := StateT.bind
+  map  := StateT.map
 }
 
 @[inline] protected def orElse [Alternative m] {α : Type u} (x₁ x₂ : StateT σ m α) : StateT σ m α :=
@@ -79,7 +79,7 @@ instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩
 instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
 
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {
-  throw    := StateT.lift ∘ throwThe ε,
+  throw    := StateT.lift ∘ throwThe ε
   tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
 }
 
@@ -90,16 +90,16 @@ section
 variables {σ : Type u} {m : Type u → Type v}
 
 instance [Monad m] : MonadStateOf σ (StateT σ m) := {
-  get       := StateT.get,
-  set       := StateT.set,
+  get       := StateT.get
+  set       := StateT.set
   modifyGet := StateT.modifyGet
 }
 
 end
 
 instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m) := {
-  stM      := fun α   => α × σ,
-  liftWith := fun f => do let s ← get; liftM (f (fun x => x.run s)),
+  stM      := fun α   => α × σ
+  liftWith := fun f => do let s ← get; liftM (f (fun x => x.run s))
   restoreM := fun x => do let (a, s) ← liftM x; set s; pure a
 }
 
diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index 65bdfbc82a..09eab326c5 100644
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@@ -43,13 +43,13 @@ instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstance
   fun ref => ref.modifyGet f
 
 instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) := {
-  get       := StateRefT'.get,
-  set       := StateRefT'.set,
+  get       := StateRefT'.get
+  set       := StateRefT'.set
   modifyGet := StateRefT'.modifyGet
 }
 
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateRefT' ω σ m) := {
-  throw    := StateRefT'.lift ∘ throwThe ε,
+  throw    := StateRefT'.lift ∘ throwThe ε
   tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
 }
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 08203f28c4..53e88bcbf3 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1121,7 +1121,7 @@ class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :=
 export MonadExcept (throw tryCatch)
 
 instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m := {
-  throw    := throwThe ε,
+  throw    := throwThe ε
   tryCatch := tryCatchThe ε
 }
 
@@ -1158,7 +1158,7 @@ variables {ρ : Type u} {m : Type u → Type v} {α : Type u}
 instance  : MonadLift m (ReaderT ρ m) := ⟨ReaderT.lift⟩
 
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) := {
-  throw    := Function.comp ReaderT.lift (throwThe ε),
+  throw    := Function.comp ReaderT.lift (throwThe ε)
   tryCatch := fun x c r => tryCatchThe ε (x r) (fun e => (c e) r)
 }
 
@@ -1180,8 +1180,8 @@ variables {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u}
   fun r => Functor.map f (x r)
 
 instance : Monad (ReaderT ρ m) := {
-  pure := ReaderT.pure,
-  bind := ReaderT.bind,
+  pure := ReaderT.pure
+  bind := ReaderT.bind
   map  := ReaderT.map
 }
 
@@ -1277,8 +1277,8 @@ class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :=
 export MonadState (get modifyGet)
 
 instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState σ m := {
-  set       := MonadStateOf.set,
-  get       := getThe σ,
+  set       := MonadStateOf.set
+  get       := getThe σ
   modifyGet := fun f => MonadStateOf.modifyGet f
 }
 
@@ -1291,8 +1291,8 @@ instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
 -- will be picked first
 instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n := {
-  get       := liftM (m := m) MonadStateOf.get,
-  set       := fun s => liftM (m := m) (MonadStateOf.set s),
+  get       := liftM (m := m) MonadStateOf.get
+  set       := fun s => liftM (m := m) (MonadStateOf.set s)
   modifyGet := fun f => monadLift (m := m) (MonadState.modifyGet f)
 }
 
@@ -1372,9 +1372,9 @@ class Backtrackable (δ : outParam (Type u)) (σ : Type u) :=
   | Result.error e s => Result.error e s
 
 instance : Monad (EStateM ε σ) := {
-  bind     := EStateM.bind,
-  pure     := EStateM.pure,
-  map      := EStateM.map,
+  bind     := EStateM.bind
+  pure     := EStateM.pure
+  map      := EStateM.map
   seqRight := EStateM.seqRight
 }
 
@@ -1383,13 +1383,13 @@ instance {δ} [Backtrackable δ σ] : OrElse (EStateM ε σ α) := {
 }
 
 instance : MonadStateOf σ (EStateM ε σ) := {
-  set       := EStateM.set,
-  get       := EStateM.get,
+  set       := EStateM.set
+  get       := EStateM.get
   modifyGet := EStateM.modifyGet
 }
 
 instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) := {
-  throw    := EStateM.throw,
+  throw    := EStateM.throw
   tryCatch := EStateM.tryCatch
 }
 
@@ -1407,7 +1407,7 @@ instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) := {
 
 /- Dummy default instance -/
 instance nonBacktrackable : Backtrackable PUnit σ := {
-  save    := dummySave,
+  save    := dummySave
   restore := dummyRestore
 }
 
@@ -1624,8 +1624,8 @@ class MonadQuotation (m : Type → Type) :=
 export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
 
 instance {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctorT m n] : MonadQuotation n := {
-  getCurrMacroScope   := liftM (m := m) getCurrMacroScope,
-  getMainModule       := liftM (m := m) getMainModule,
+  getCurrMacroScope   := liftM (m := m) getCurrMacroScope
+  getMainModule       := liftM (m := m) getMainModule
   withFreshMacroScope := monadMap (m := m) withFreshMacroScope
 }
 
@@ -1762,7 +1762,7 @@ class MonadRef (m : Type → Type) :=
 export MonadRef (getRef)
 
 instance (m n : Type → Type) [MonadRef m] [MonadFunctor m n] [MonadLift m n] : MonadRef n := {
-  getRef  := liftM (getRef : m _),
+  getRef  := liftM (getRef : m _)
   withRef := fun ref x => monadMap (m := m) (MonadRef.withRef ref) x
 }
 
@@ -1805,7 +1805,7 @@ abbrev Macro := Syntax → MacroM Syntax
 namespace Macro
 
 instance : MonadRef MacroM := {
-  getRef     := bind read fun ctx => pure ctx.ref,
+  getRef     := bind read fun ctx => pure ctx.ref
   withRef    := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
 }
 
@@ -1834,8 +1834,8 @@ def throwErrorAt {α} (ref : Syntax) (msg : String) : MacroM α :=
   | false => withReader (fun ctx => { ctx with currRecDepth := add ctx.currRecDepth 1 }) x
 
 instance : MonadQuotation MacroM := {
-  getCurrMacroScope   := fun ctx => pure ctx.currMacroScope,
-  getMainModule       := fun ctx => pure ctx.mainModule,
+  getCurrMacroScope   := fun ctx => pure ctx.currMacroScope
+  getMainModule       := fun ctx => pure ctx.mainModule
   withFreshMacroScope := Macro.withFreshMacroScope
 }