From af968c60e6270aedb132777ffb5fa86b29fda8a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Oct 2020 07:32:23 -0700
Subject: [PATCH] chore: cleanup

---
 src/Lean/Elab/PreDefinition/Basic.lean    | 2 +-
 src/Lean/Elab/StrategyAttrs.lean          | 2 +-
 src/Lean/Expr.lean                        | 2 +-
 src/Lean/Level.lean                       | 4 ++--
 src/Lean/LocalContext.lean                | 2 +-
 src/Lean/Meta/AbstractMVars.lean          | 4 ++--
 src/Lean/Meta/Basic.lean                  | 6 +++---
 src/Lean/Meta/DiscrTree.lean              | 4 ++--
 src/Lean/Meta/Match/CaseArraySizes.lean   | 2 +-
 src/Lean/Meta/Match/CaseValues.lean       | 4 ++--
 src/Lean/Meta/Match/Match.lean            | 2 +-
 src/Lean/Meta/RecursorInfo.lean           | 2 +-
 src/Lean/Meta/SynthInstance.lean          | 6 +++---
 src/Lean/Meta/Tactic/Induction.lean       | 2 +-
 src/Lean/MetavarContext.lean              | 2 +-
 src/Lean/Parser/Extension.lean            | 2 +-
 src/Lean/PrettyPrinter/Formatter.lean     | 4 ++--
 src/Lean/PrettyPrinter/Parenthesizer.lean | 6 +++---
 src/Lean/ProjFns.lean                     | 2 +-
 src/Lean/ReducibilityAttrs.lean           | 2 +-
 src/Lean/ResolveName.lean                 | 2 +-
 src/Lean/Syntax.lean                      | 2 +-
 src/Lean/Util/CollectFVars.lean           | 2 +-
 src/Lean/Util/CollectLevelParams.lean     | 2 +-
 src/Lean/Util/CollectMVars.lean           | 2 +-
 src/Lean/Util/MonadCache.lean             | 8 ++++----
 src/Lean/Util/PPExt.lean                  | 2 +-
 27 files changed, 41 insertions(+), 41 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 24e9c93005..178cd64719 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -26,7 +26,7 @@ structure PreDefinition :=
 (type      : Expr)
 (value     : Expr)
 
-instance PreDefinition.inhabited : Inhabited PreDefinition :=
+instance : Inhabited PreDefinition :=
 ⟨⟨DefKind.«def», [], {}, arbitrary _, arbitrary _, arbitrary _⟩⟩
 
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
diff --git a/src/Lean/Elab/StrategyAttrs.lean b/src/Lean/Elab/StrategyAttrs.lean
index 5b1366663e..e19a619f4d 100644
--- a/src/Lean/Elab/StrategyAttrs.lean
+++ b/src/Lean/Elab/StrategyAttrs.lean
@@ -15,7 +15,7 @@ the strategy selection attributes while we rely on the Lean3 elaborator.
 inductive ElaboratorStrategy
 | simple | withExpectedType | asEliminator
 
-instance ElaboratorStrategy.inhabited : Inhabited ElaboratorStrategy :=
+instance : Inhabited ElaboratorStrategy :=
 ⟨ElaboratorStrategy.withExpectedType⟩
 
 builtin_initialize elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy ←
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index dd1fc11691..242b2a50fc 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -727,7 +727,7 @@ abbrev PExprSet := PersistentExprSet
 structure ExprStructEq :=
 (val : Expr)
 
-instance exprToExprStructEq    : Coe Expr ExprStructEq := ⟨ExprStructEq.mk⟩
+instance : Coe Expr ExprStructEq := ⟨ExprStructEq.mk⟩
 
 namespace ExprStructEq
 
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 4ab5e9a805..62ec9d54bc 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -24,13 +24,13 @@ namespace Lean
    depth     : 24-bits -/
 def Level.Data := UInt64
 
-instance Level.Data.inhabited : Inhabited Level.Data :=
+instance : Inhabited Level.Data :=
 inferInstanceAs (Inhabited UInt64)
 
 def Level.Data.hash (c : Level.Data) : USize :=
 c.toUInt32.toUSize
 
-instance Level.Data.hasBeq : HasBeq Level.Data :=
+instance : HasBeq Level.Data :=
 ⟨fun (a b : UInt64) => a == b⟩
 
 def Level.Data.depth (c : Level.Data) : UInt32 :=
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 67336f188b..b381469f3c 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -392,7 +392,7 @@ class MonadLCtx (m : Type → Type) :=
 
 export MonadLCtx (getLCtx)
 
-instance monadLCtxTrans (m n) [MonadLCtx m] [MonadLift m n] : MonadLCtx n :=
+instance (m n) [MonadLCtx m] [MonadLift m n] : MonadLCtx n :=
   { getLCtx := liftM (getLCtx : m _) }
 
 def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean
index 3d3ede4028..5aee9b2589 100644
--- a/src/Lean/Meta/AbstractMVars.lean
+++ b/src/Lean/Meta/AbstractMVars.lean
@@ -13,12 +13,12 @@ structure AbstractMVarsResult :=
 (numMVars   : Nat)
 (expr       : Expr)
 
-instance AbstractMVarsResult.inhabited : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary _⟩⟩
+instance : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary _⟩⟩
 
 def AbstractMVarsResult.beq (r₁ r₂ : AbstractMVarsResult) : Bool :=
 r₁.paramNames == r₂.paramNames && r₁.numMVars == r₂.numMVars && r₁.expr == r₂.expr
 
-instance AbstractMVarsResult.hasBeq : HasBeq AbstractMVarsResult := ⟨AbstractMVarsResult.beq⟩
+instance : HasBeq AbstractMVarsResult := ⟨AbstractMVarsResult.beq⟩
 
 namespace AbstractMVars
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index deaa0f5a34..3a09f5791d 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -100,7 +100,7 @@ structure State :=
 /- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/
 (zetaFVarIds : NameSet := {})
 
-instance State.inhabited : Inhabited State := ⟨{}⟩
+instance : Inhabited State := ⟨{}⟩
 
 structure Context :=
 (config         : Config         := {})
@@ -118,7 +118,7 @@ abbrev DefEqM := StateRefT (PersistentArray PostponedEntry) MetaM
 instance : MonadIO MetaM :=
 { liftIO := fun x => liftM (liftIO x : CoreM _) }
 
-instance MetaM.inhabited {α} : Inhabited (MetaM α) :=
+instance {α} : Inhabited (MetaM α) :=
 ⟨fun _ _ => arbitrary _⟩
 
 instance : MonadLCtx MetaM :=
@@ -140,7 +140,7 @@ Prod.fst <$> x.run ctx s
 let ((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore
 pure (a, sCore, s)
 
-instance hasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
+instance {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
 ⟨fun env opts x _ => MetaHasEval.eval env opts x.run' true⟩
 
 protected def throwIsDefEqStuck {α} : DefEqM α :=
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index c8a913e754..f41081fd6f 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -247,7 +247,7 @@ partial def Trie.format {α} [HasFormat α] : Trie α → Format
   "node" ++ (if vs.isEmpty then Format.nil else " " ++ fmt vs)
   ++ Format.join (cs.toList.map $ fun ⟨k, c⟩ => Format.line ++ Format.paren (fmt k ++ " => " ++ format c))
 
-instance Trie.hasFormat {α} [HasFormat α] : HasFormat (Trie α) := ⟨Trie.format⟩
+instance {α} [HasFormat α] : HasFormat (Trie α) := ⟨Trie.format⟩
 
 partial def format {α} [HasFormat α] (d : DiscrTree α) : Format :=
 let (_, r) := d.root.foldl
@@ -256,7 +256,7 @@ let (_, r) := d.root.foldl
   (true, Format.nil)
 Format.group r
 
-instance DiscrTree.hasFormat {α} [HasFormat α] : HasFormat (DiscrTree α) := ⟨format⟩
+instance {α} [HasFormat α] : HasFormat (DiscrTree α) := ⟨format⟩
 
 private def getKeyArgs (e : Expr) (isMatch? : Bool) : MetaM (Key × Array Expr) := do
 let e ← whnfEta e
diff --git a/src/Lean/Meta/Match/CaseArraySizes.lean b/src/Lean/Meta/Match/CaseArraySizes.lean
index 3af1f7294e..cabdea4fe0 100644
--- a/src/Lean/Meta/Match/CaseArraySizes.lean
+++ b/src/Lean/Meta/Match/CaseArraySizes.lean
@@ -15,7 +15,7 @@ structure CaseArraySizesSubgoal :=
 (diseqs : Array FVarId := #[])
 (subst  : FVarSubst := {})
 
-instance CaseArraySizesSubgoal.inhabited : Inhabited CaseArraySizesSubgoal :=
+instance : Inhabited CaseArraySizesSubgoal :=
 ⟨{ mvarId := arbitrary _ }⟩
 
 def getArrayArgType (a : Expr) : MetaM Expr := do
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index b024550c29..d3ffc36ef7 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/src/Lean/Meta/Match/CaseValues.lean
@@ -14,7 +14,7 @@ structure CaseValueSubgoal :=
 (newH   : FVarId)
 (subst  : FVarSubst := {})
 
-instance CaseValueSubgoal.inhabited : Inhabited CaseValueSubgoal :=
+instance : Inhabited CaseValueSubgoal :=
 ⟨{ mvarId := arbitrary _, newH := arbitrary _ }⟩
 
 /--
@@ -65,7 +65,7 @@ structure CaseValuesSubgoal :=
 (newHs  : Array FVarId := #[])
 (subst  : FVarSubst := {})
 
-instance CaseValueSubgoals.inhabited : Inhabited CaseValuesSubgoal :=
+instance : Inhabited CaseValuesSubgoal :=
 ⟨{ mvarId := arbitrary _ }⟩
 
 /--
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 360c6cb228..9fe7edd488 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -773,7 +773,7 @@ structure Entry :=
 structure State :=
 (map : SMap Name MatcherInfo := {})
 
-instance State.inhabited : Inhabited State :=
+instance : Inhabited State :=
 ⟨{}⟩
 
 def State.addEntry (s : State) (e : Entry) : State := { s with map  := s.map.insert e.name e.info }
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index f884296708..3b17f0fdbd 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -24,7 +24,7 @@ inductive RecursorUnivLevelPos
 | motive                -- marks where the universe of the motive should go
 | majorType (idx : Nat) -- marks where the #idx universe of the major premise type goes
 
-instance RecursorUnivLevelPos.hasToString : HasToString RecursorUnivLevelPos :=
+instance : HasToString RecursorUnivLevelPos :=
 ⟨fun pos => match pos with
   | RecursorUnivLevelPos.motive        => "<motive-univ>"
   | RecursorUnivLevelPos.majorType idx => toString idx⟩
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index dcd0864ffc..55ddec8626 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -33,7 +33,7 @@ structure GeneratorNode :=
 (instances       : Array Expr)
 (currInstanceIdx : Nat)
 
-instance GeneratorNode.inhabited : Inhabited GeneratorNode := ⟨⟨arbitrary _, arbitrary _, arbitrary _, arbitrary _, 0⟩⟩
+instance : Inhabited GeneratorNode := ⟨⟨arbitrary _, arbitrary _, arbitrary _, arbitrary _, 0⟩⟩
 
 structure ConsumerNode :=
 (mvar     : Expr)
@@ -41,7 +41,7 @@ structure ConsumerNode :=
 (mctx     : MetavarContext)
 (subgoals : List Expr)
 
-instance Consumernode.inhabited : Inhabited ConsumerNode := ⟨⟨arbitrary _, arbitrary _, arbitrary _, []⟩⟩
+instance : Inhabited ConsumerNode := ⟨⟨arbitrary _, arbitrary _, arbitrary _, []⟩⟩
 
 inductive Waiter
 | consumerNode : ConsumerNode → Waiter
@@ -137,7 +137,7 @@ structure Answer :=
 (result     : AbstractMVarsResult)
 (resultType : Expr)
 
-instance Answer.inhabited : Inhabited Answer := ⟨⟨arbitrary _, arbitrary _⟩⟩
+instance : Inhabited Answer := ⟨⟨arbitrary _, arbitrary _⟩⟩
 
 structure TableEntry :=
 (waiters : Array Waiter)
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index 43e7d3b96c..df0e3e852a 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -41,7 +41,7 @@ structure InductionSubgoal :=
 (fields : Array Expr := #[])
 (subst  : FVarSubst := {})
 
-instance InductionSubgoal.inhabited : Inhabited InductionSubgoal := ⟨{ mvarId := arbitrary _ }⟩
+instance : Inhabited InductionSubgoal := ⟨{ mvarId := arbitrary _ }⟩
 
 private def getTypeBody (mvarId : MVarId) (type : Expr) (x : Expr) : MetaM Expr := do
 type ← whnfForall type
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index fb5c6f58a0..98ed19564e 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -1113,7 +1113,7 @@ class MonadMCtx (m : Type → Type) :=
 
 export MonadMCtx (getMCtx)
 
-instance monadMCtxTrans (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n :=
+instance (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n :=
   { getMCtx := liftM (getMCtx : m _) }
 
 end Lean
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 7a8a8c2042..91599c22aa 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -65,7 +65,7 @@ structure ParserExtensionState :=
 (categories  : ParserCategories := {})
 (newEntries  : List ParserExtensionOleanEntry := [])
 
-instance ParserExtensionState.inhabited : Inhabited ParserExtensionState := ⟨{}⟩
+instance : Inhabited ParserExtensionState := ⟨{}⟩
 
 abbrev ParserExtension := PersistentEnvExtension ParserExtensionOleanEntry ParserExtensionEntry ParserExtensionState
 
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index dbd7594ff3..82c8b47676 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -47,7 +47,7 @@ abbrev FormatterM := ReaderT Formatter.Context $ StateRefT Formatter.State $ Cor
     p₁
     (fun _ => do set s; p₂)
 
-instance Formatter.orelse {α} : HasOrelse (FormatterM α) := ⟨FormatterM.orelse⟩
+instance {α} : HasOrelse (FormatterM α) := ⟨FormatterM.orelse⟩
 
 abbrev Formatter := FormatterM Unit
 
@@ -90,7 +90,7 @@ open Lean.Parser
 def throwBacktrack {α} : FormatterM α :=
 throw $ Exception.internal backtrackExceptionId
 
-instance FormatterM.monadTraverser : Syntax.MonadTraverser FormatterM := ⟨{
+instance : Syntax.MonadTraverser FormatterM := ⟨{
   get       := State.stxTrav <$> get,
   set       := fun t => modify (fun st => { st with stxTrav := t }),
   modifyGet := fun f => modifyGet (fun st => let (a, t) := f st.stxTrav; (a, { st with stxTrav := t }))
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 1aaa1e3c7f..5f0e9b5a0c 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -109,7 +109,7 @@ abbrev Parenthesizer := ParenthesizerM Unit
     p₁
     (fun _ => do set s; p₂)
 
-instance Parenthesizer.orelse {α} : HasOrelse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩
+instance {α} : HasOrelse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩
 
 unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) :=
   KeyedDeclsAttribute.init {
@@ -173,7 +173,7 @@ open Lean.Format
 def throwBacktrack {α} : ParenthesizerM α :=
 throw $ Exception.internal backtrackExceptionId
 
-instance ParenthesizerM.monadTraverser : Syntax.MonadTraverser ParenthesizerM := ⟨{
+instance : Syntax.MonadTraverser ParenthesizerM := ⟨{
   get       := State.stxTrav <$> get,
   set       := fun t => modify (fun st => { st with stxTrav := t }),
   modifyGet := fun f => modifyGet (fun st => let (a, t) := f st.stxTrav; (a, { st with stxTrav := t }))
@@ -193,7 +193,7 @@ def visitArgs (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
 
 -- Macro scopes in the parenthesizer output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.
-instance monadQuotation : MonadQuotation ParenthesizerM := {
+instance : MonadQuotation ParenthesizerM := {
   getCurrMacroScope   := pure $ arbitrary _,
   getMainModule       := pure $ arbitrary _,
   withFreshMacroScope := fun x => x,
diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean
index a0dc143da6..07e6a1135b 100644
--- a/src/Lean/ProjFns.lean
+++ b/src/Lean/ProjFns.lean
@@ -22,7 +22,7 @@ def mkProjectionInfoEx (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass :
 @[export lean_projection_info_from_class]
 def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass
 
-instance ProjectionFunctionInfo.inhabited : Inhabited ProjectionFunctionInfo :=
+instance : Inhabited ProjectionFunctionInfo :=
 ⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
 
 builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) ←
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index 79e30eff75..91f69c2bea 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -11,7 +11,7 @@ namespace Lean
 inductive ReducibilityStatus
 | reducible | semireducible | irreducible
 
-instance ReducibilityStatus.inhabited : Inhabited ReducibilityStatus := ⟨ReducibilityStatus.semireducible⟩
+instance : Inhabited ReducibilityStatus := ⟨ReducibilityStatus.semireducible⟩
 
 builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
   registerEnumAttributes `reducibility
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index da80f62293..c639b6e14e 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -151,7 +151,7 @@ class MonadResolveName (m : Type → Type) :=
 
 export MonadResolveName (getCurrNamespace getOpenDecls)
 
-instance monadResolveNameFromLift (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n :=
+instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n :=
 { getCurrNamespace := liftM (getCurrNamespace : m _),
   getOpenDecls     := liftM (getOpenDecls : m _) }
 
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index e716cc9cf9..6254f62147 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -332,7 +332,7 @@ partial def structEq : Syntax → Syntax → Bool
 | Syntax.ident _ rawVal val preresolved, Syntax.ident _ rawVal' val' preresolved' => rawVal == rawVal' && val == val' && preresolved == preresolved'
 | _, _ => false
 
-instance structHasBeq : HasBeq Lean.Syntax := ⟨structEq⟩
+instance : HasBeq Lean.Syntax := ⟨structEq⟩
 
 /--
 Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.
diff --git a/src/Lean/Util/CollectFVars.lean b/src/Lean/Util/CollectFVars.lean
index 58169192f3..db8293cd91 100644
--- a/src/Lean/Util/CollectFVars.lean
+++ b/src/Lean/Util/CollectFVars.lean
@@ -12,7 +12,7 @@ structure State :=
 (visitedExpr  : ExprSet  := {})
 (fvarSet      : NameSet  := {})
 
-instance State.inhabited : Inhabited State := ⟨{}⟩
+instance : Inhabited State := ⟨{}⟩
 
 abbrev Visitor := State → State
 
diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean
index 8ca5bff49e..b312c51ce9 100644
--- a/src/Lean/Util/CollectLevelParams.lean
+++ b/src/Lean/Util/CollectLevelParams.lean
@@ -15,7 +15,7 @@ structure State :=
 (visitedExpr  : ExprSet    := {})
 (params       : Array Name := #[])
 
-instance State.inhabited : Inhabited State := ⟨{}⟩
+instance : Inhabited State := ⟨{}⟩
 
 abbrev Visitor := State → State
 
diff --git a/src/Lean/Util/CollectMVars.lean b/src/Lean/Util/CollectMVars.lean
index 6ac5b847b5..21d50da3c4 100644
--- a/src/Lean/Util/CollectMVars.lean
+++ b/src/Lean/Util/CollectMVars.lean
@@ -14,7 +14,7 @@ structure State :=
 (visitedExpr  : ExprSet      := {})
 (result       : Array MVarId := #[])
 
-instance State.inhabited : Inhabited State := ⟨{}⟩
+instance : Inhabited State := ⟨{}⟩
 
 abbrev Visitor := State → State
 
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index d7ecc7ab4f..5448e15df5 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -22,11 +22,11 @@ match b? with
   MonadCache.cache a b
   pure b
 
-instance readerLift {α β ρ : Type} {m : Type → Type} [MonadCache α β m] : MonadCache α β (ReaderT ρ m) :=
+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 exceptLift {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : MonadCache α β (ExceptT ε m) :=
+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 }
 
@@ -88,7 +88,7 @@ let s ← get; pure s.cache
 @[inline] def modifyCache {α β σ : Type} [HasBeq α] [Hashable α] (f : HashMap α β → HashMap α β) : StateM (WithHashMapCache α β σ) Unit :=
 modify fun s => { s with cache := f s.cache }
 
-instance stateAdapter (α β σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (StateM (WithHashMapCache α β σ)) :=
+instance (α β σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (StateM (WithHashMapCache α β σ)) :=
 { getCache    := WithHashMapCache.getCache,
   modifyCache := WithHashMapCache.modifyCache }
 
@@ -98,7 +98,7 @@ let s ← get; pure s.cache
 @[inline] def modifyCacheE {α β ε σ : Type} [HasBeq α] [Hashable α] (f : HashMap α β → HashMap α β) : EStateM ε (WithHashMapCache α β σ) Unit :=
 modify fun s => { s with cache := f s.cache }
 
-instance estateAdapter (α β ε σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (EStateM ε (WithHashMapCache α β σ)) :=
+instance (α β ε σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (EStateM ε (WithHashMapCache α β σ)) :=
 { getCache    := WithHashMapCache.getCacheE,
   modifyCache := WithHashMapCache.modifyCacheE }
 
diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
index fa2eae3381..7e727c5baa 100644
--- a/src/Lean/Util/PPExt.lean
+++ b/src/Lean/Util/PPExt.lean
@@ -32,7 +32,7 @@ structure PPFns :=
   (ppExpr : PPContext → Expr → IO Format)
   (ppTerm : PPContext → Syntax → IO Format)
 
-instance PPFns.inhabited : Inhabited PPFns := ⟨⟨arbitrary _, arbitrary _⟩⟩
+instance : Inhabited PPFns := ⟨⟨arbitrary _, arbitrary _⟩⟩
 
 builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {