diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index ea9542a2a1..5290b9a4f1 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -228,15 +228,15 @@ export Core (CoreM mkFreshUserName checkMaxHeartbeats withCurrHeartbeats)
   try
     x
   catch ex => match ex with
-    | Exception.error _ _      => throw ex
-    | Exception.internal id' _ => if id == id' then h ex else throw ex
+    | .error ..       => throw ex
+    | .internal id' _ => if id == id' then h ex else throw ex
 
 @[inline] def catchInternalIds [Monad m] [MonadExcept Exception m] (ids : List InternalExceptionId) (x : m α) (h : Exception → m α) : m α := do
   try
     x
   catch ex => match ex with
-    | Exception.error _ _     => throw ex
-    | Exception.internal id _ => if ids.contains id then h ex else throw ex
+    | .error ..      => throw ex
+    | .internal id _ => if ids.contains id then h ex else throw ex
 
 /--
   Return true if `ex` was generated by `throwMaxHeartbeat`.
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index c26931f12c..56ceacae19 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -37,7 +37,7 @@ private def ensureArgType (f : Expr) (arg : Expr) (expectedType : Expr) : TermEl
   try
     ensureHasTypeAux expectedType argType arg f
   catch
-    | ex@(Exception.error ..) =>
+    | ex@(.error ..) =>
       if (← read).errToSorry then
         exceptionToSorry ex expectedType
       else
@@ -249,7 +249,7 @@ private def fTypeHasOptAutoParams : M Bool := do
    See `propagateExpectedType`.
    Remark: `(explicit : Bool) == true` when `@` modifier is used. -/
 private partial def getForallBody (explicit : Bool) : Nat → List NamedArg → Expr → Option Expr
-  | i, namedArgs, type@(Expr.forallE n d b bi) =>
+  | i, namedArgs, type@(.forallE n d b bi) =>
     match namedArgs.find? fun (namedArg : NamedArg) => namedArg.name == n with
     | some _ => getForallBody explicit i (eraseNamedArgCore namedArgs n) b
     | none =>
@@ -538,7 +538,7 @@ mutual
       let argType ← getArgExpectedType
       match (← read).explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
       | false, some defVal, _  => addNewArg argName defVal; main
-      | false, _, some (Expr.const tacticDecl _) =>
+      | false, _, some (.const tacticDecl _) =>
         let env ← getEnv
         let opts ← getOptions
         match evalSyntaxConstant env opts tacticDecl with
@@ -998,7 +998,7 @@ where
         throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
       return idNew
     catch
-      | ex@(.error _ _) =>
+      | ex@(.error ..) =>
         match (← unfoldDefinition? resultType) with
         | some resultType => go (← whnfCore resultType) expectedType (previousExceptions.push ex)
         | none       =>
@@ -1107,8 +1107,8 @@ private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array A
     else if successes.size > 1 then
       let msgs : Array MessageData ← successes.mapM fun success => do
         match success with
-        | EStateM.Result.ok e s => withMCtx s.meta.meta.mctx <| withEnv s.meta.core.env do addMessageContext m!"{e} : {← inferType e}"
-        | _                     => unreachable!
+        | .ok e s => withMCtx s.meta.meta.mctx <| withEnv s.meta.core.env do addMessageContext m!"{e} : {← inferType e}"
+        | _       => unreachable!
       throwErrorAt f "ambiguous, possible interpretations {toMessageList msgs}"
     else
       withRef f <| mergeFailures candidates
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 199c5c6bf8..1f868114e5 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -45,8 +45,8 @@ structure BinderView where
   bi : BinderInfo
 
 partial def quoteAutoTactic : Syntax → TermElabM Syntax
-  | stx@(Syntax.ident _ _ _ _) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
-  | stx@(Syntax.node _ k args)   => do
+  | stx@(.ident ..) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
+  | stx@(.node _ k args) => do
     if stx.isAntiquot then
       throwErrorAt stx "invalid auto tactic, antiquotation is not allowed"
     else
@@ -58,8 +58,8 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
           let quotedArg ← quoteAutoTactic arg
           quotedArgs ← `(Array.push $quotedArgs $quotedArg)
       `(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
-  | Syntax.atom _ val => `(mkAtom $(quote val))
-  | Syntax.missing    => throwError "invalid auto tactic, tactic is missing"
+  | .atom _ val => `(mkAtom $(quote val))
+  | .missing    => throwError "invalid auto tactic, tactic is missing"
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
   withFreshMacroScope do
@@ -108,28 +108,28 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
   let k := stx.getKind
   if stx.isIdent || k == ``hole then
     -- binderIdent
-    pure #[{ id := (← expandBinderIdent stx), type := mkHole stx, bi := BinderInfo.default }]
+    return #[{ id := (← expandBinderIdent stx), type := mkHole stx, bi := .default }]
   else if k == ``Lean.Parser.Term.explicitBinder then
     -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
     let ids ← getBinderIds stx[1]
     let type        := stx[2]
     let optModifier := stx[3]
-    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := (← expandBinderModifier (expandBinderType id type) optModifier), bi := BinderInfo.default }
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := (← expandBinderModifier (expandBinderType id type) optModifier), bi := .default }
   else if k == ``Lean.Parser.Term.implicitBinder then
     -- `{` binderIdent+ binderType `}`
     let ids ← getBinderIds stx[1]
     let type := stx[2]
-    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := BinderInfo.implicit }
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := .implicit }
   else if k == ``Lean.Parser.Term.strictImplicitBinder then
     -- `⦃` binderIdent+ binderType `⦄`
     let ids ← getBinderIds stx[1]
     let type := stx[2]
-    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := BinderInfo.strictImplicit }
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := .strictImplicit }
   else if k == ``Lean.Parser.Term.instBinder then
     -- `[` optIdent type `]`
     let id ← expandOptIdent stx[1]
     let type := stx[2]
-    pure #[ { id := id, type := type, bi := BinderInfo.instImplicit } ]
+    return #[ { id := id, type := type, bi := .instImplicit } ]
   else
     throwUnsupportedSyntax
 
@@ -149,11 +149,11 @@ register_builtin_option checkBinderAnnotations : Bool := {
   descr    := "check whether type is a class instance whenever the binder annotation `[...]` is used"
 }
 
-private partial def elabBinderViews {α} (binderViews : Array BinderView) (fvars : Array (Syntax × Expr)) (k : Array (Syntax × Expr) → TermElabM α)
+private partial def elabBinderViews (binderViews : Array BinderView) (fvars : Array (Syntax × Expr)) (k : Array (Syntax × Expr) → TermElabM α)
     : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array (Syntax × Expr)) : TermElabM α := do
     if h : i < binderViews.size then
-      let binderView := binderViews.get ⟨i, h⟩
+      let binderView := binderViews[i]
       ensureAtomicBinderName binderView
       let type ← elabType binderView.type
       registerFailedToInferBinderTypeInfo type binderView.type
@@ -167,10 +167,10 @@ private partial def elabBinderViews {α} (binderViews : Array BinderView) (fvars
       k fvars
   loop 0 fvars
 
-private partial def elabBindersAux {α} (binders : Array Syntax) (k : Array (Syntax × Expr) → TermElabM α) : TermElabM α :=
+private partial def elabBindersAux (binders : Array Syntax) (k : Array (Syntax × Expr) → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array (Syntax × Expr)) : TermElabM α := do
     if h : i < binders.size then
-      let binderViews ← matchBinder (binders.get ⟨i, h⟩)
+      let binderViews ← matchBinder binders[i]
       elabBinderViews binderViews fvars <| loop (i+1)
     else
       k fvars
@@ -181,7 +181,7 @@ private partial def elabBindersAux {α} (binders : Array Syntax) (k : Array (Syn
   `elabBinders(Ex)` automatically adds binder info nodes for the produced fvars, but storing the syntax nodes
   might be necessary when later adding the same binders back to the local context so that info nodes can
   manually be added for the new fvars; see `MutualDef` for an example. -/
-def elabBindersEx {α} (binders : Array Syntax) (k : Array (Syntax × Expr) → TermElabM α) : TermElabM α :=
+def elabBindersEx (binders : Array Syntax) (k : Array (Syntax × Expr) → TermElabM α) : TermElabM α :=
   universeConstraintsCheckpoint do
     if binders.isEmpty then
       k #[]
@@ -201,7 +201,7 @@ def elabBinders (binders : Array Syntax) (k : Array Expr → TermElabM α) : Ter
   elabBindersEx binders (fun fvars => k (fvars.map (·.2)))
 
 /-- Same as `elabBinder` with a single binder.-/
-def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α :=
+def elabBinder (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α :=
   elabBinders #[binder] fun fvars => x fvars[0]!
 
 def expandSimpleBinderWithType (type : Term) (binder : Syntax) : MacroM Syntax :=
@@ -289,7 +289,7 @@ private partial def getFunBinderIds? (stx : Syntax) : OptionT MacroM (Array Synt
 partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (Array Syntax × Syntax × Bool) :=
   let rec loop (body : Syntax) (i : Nat) (newBinders : Array Syntax) := do
     if h : i < binders.size then
-      let binder := binders.get ⟨i, h⟩
+      let binder := binders[i]
       let processAsPattern : Unit → MacroM (Array Syntax × Syntax × Bool) := fun _ => do
         let pattern := binder
         let major ← mkFreshIdent binder
@@ -352,19 +352,19 @@ private def propagateExpectedType (fvar : Expr) (fvarType : Expr) (s : State) :
   | some expectedType =>
     let expectedType ← whnfForall expectedType
     match expectedType with
-    | Expr.forallE _ d b _ =>
+    | .forallE _ d b _ =>
       discard <| isDefEq fvarType d
       let b := b.instantiate1 fvar
-      pure { s with expectedType? := some b }
+      return { s with expectedType? := some b }
     | _ =>
-      pure { s with expectedType? := none }
+      return { s with expectedType? := none }
 
 private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat) (s : State) : TermElabM State := do
   if h : i < binderViews.size then
-    let binderView := binderViews.get ⟨i, h⟩
+    let binderView := binderViews[i]
     ensureAtomicBinderName binderView
     withRef binderView.type <| withLCtx s.lctx s.localInsts do
-      let type       ← elabType binderView.type
+      let type ← elabType binderView.type
       registerFailedToInferBinderTypeInfo type binderView.type
       let fvarId ← mkFreshFVarId
       let fvar  := mkFVar fvarId
@@ -378,19 +378,19 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat
       let lctx  := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi
       addTermInfo' (lctx? := some lctx) (isBinder := true) binderView.id fvar
       let s ← withRef binderView.id <| propagateExpectedType fvar type s
-      let s := { s with lctx := lctx }
+      let s := { s with lctx }
       match (← isClass? type) with
       | none           => elabFunBinderViews binderViews (i+1) s
       | some className =>
         resettingSynthInstanceCache do
-          let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId }
-          elabFunBinderViews binderViews (i+1) { s with localInsts := localInsts }
+          let localInsts := s.localInsts.push { className, fvar := mkFVar fvarId }
+          elabFunBinderViews binderViews (i+1) { s with localInsts }
   else
     pure s
 
 partial def elabFunBindersAux (binders : Array Syntax) (i : Nat) (s : State) : TermElabM State := do
   if h : i < binders.size then
-    let binderViews ← matchBinder (binders.get ⟨i, h⟩)
+    let binderViews ← matchBinder binders[i]
     let s ← elabFunBinderViews binderViews 0 s
     elabFunBindersAux binders (i+1) s
   else
@@ -398,13 +398,13 @@ partial def elabFunBindersAux (binders : Array Syntax) (i : Nat) (s : State) : T
 
 end FunBinders
 
-def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (x : Array Expr → Option Expr → TermElabM α) : TermElabM α :=
+def elabFunBinders (binders : Array Syntax) (expectedType? : Option Expr) (x : Array Expr → Option Expr → TermElabM α) : TermElabM α :=
   if binders.isEmpty then
     x #[] expectedType?
   else do
     let lctx ← getLCtx
     let localInsts ← getLocalInstances
-    let s ← FunBinders.elabFunBindersAux binders 0 { lctx := lctx, localInsts := localInsts, expectedType? := expectedType? }
+    let s ← FunBinders.elabFunBindersAux binders 0 { lctx, localInsts, expectedType? }
     resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) <| withLCtx s.lctx s.localInsts <|
       x s.fvars s.expectedType?
 
@@ -650,7 +650,7 @@ def mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView :=
   let optType := letIdDecl[2]
   let type    := expandOptType id optType
   let value   := letIdDecl[4]
-  { id := id, binders := binders, type := type, value := value }
+  { id, binders, type, value }
 
 def expandLetEqnsDecl (letDecl : Syntax) : MacroM Syntax := do
   let ref       := letDecl
@@ -662,8 +662,8 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
   let letDecl := stx[1][0]
   let body    := stx[3]
   if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
-    let { id := id, binders := binders, type := type, value := val } := mkLetIdDeclView letDecl
-    elabLetDeclAux id binders type val body expectedType? useLetExpr elabBodyFirst usedLetOnly
+    let { id, binders, type, value } := mkLetIdDeclView letDecl
+    elabLetDeclAux id binders type value body expectedType? useLetExpr elabBodyFirst usedLetOnly
   else if letDecl.getKind == ``Lean.Parser.Term.letPatDecl then
     -- node `Lean.Parser.Term.letPatDecl  $ try (termParser >> pushNone >> optType >> " := ") >> termParser
     if elabBodyFirst then
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index e66ef7cd84..76dab4f54d 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -144,11 +144,11 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List (Key
       try
         withReader ({ · with elaborator := evalFn.declName }) <| withTacticInfoContext stx <| evalFn.value stx
       catch
-      | ex@(Exception.error _ _) =>
+      | ex@(.error ..) =>
         match evalFns with
         | []      => throw ex -- (*)
         | evalFns => s.restore; loop evalFns
-      | ex@(Exception.internal id _) =>
+      | ex@(.internal id _) =>
         if id == unsupportedSyntaxExceptionId then
           s.restore; loop evalFns
         else
@@ -176,7 +176,7 @@ mutual
 
   partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
     withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
-      | Syntax.node _ k _    =>
+      | .node _ k _    =>
         if k == nullKind then
           -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
           stx.getArgs.forM evalTactic
@@ -186,7 +186,7 @@ mutual
           match tacticElabAttribute.getEntries (← getEnv) stx.getKind with
           | []      => expandTacticMacro s stx
           | evalFns => evalTacticUsing s stx evalFns
-      | Syntax.missing => pure ()
+      | .missing => pure ()
       | _ => throwError m!"unexpected tactic{indentD stx}"
 
   partial def evalTactic (stx : Syntax) : TacticM Unit :=
@@ -248,10 +248,10 @@ instance : MonadExcept Exception TacticM where
 def withoutRecover (x : TacticM α) : TacticM α :=
   withReader (fun ctx => { ctx with recover := false }) x
 
-@[inline] protected def orElse {α} (x : TacticM α) (y : Unit → TacticM α) : TacticM α := do
+@[inline] protected def orElse (x : TacticM α) (y : Unit → TacticM α) : TacticM α := do
   try withoutRecover x catch _ => y ()
 
-instance {α} : OrElse (TacticM α) where
+instance : OrElse (TacticM α) where
   orElse := Tactic.orElse
 
 instance : Alternative TacticM where
@@ -269,7 +269,7 @@ def saveTacticInfoForToken (stx : Syntax) : TacticM Unit := do
 
 /- Elaborate `x` with `stx` on the macro stack -/
 @[inline]
-def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α :=
+def withMacroExpansion (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α :=
   withMacroExpansionInfo beforeStx afterStx do
     withTheReader Term.Context (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
 
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 3f5d6ae0ad..202f3621fe 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -224,7 +224,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
   withMainContext do
     let e ← elabTerm stx none
     match e with
-    | Expr.fvar fvarId => pure fvarId
+    | .fvar fvarId => pure fvarId
     | _ =>
       let type ← inferType e
       let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 94e7c0f6ac..8a9c2df512 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -114,7 +114,7 @@ structure Result where
 partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do
   let rec loop : M Unit := do
     match (← getFType) with
-    | Expr.forallE binderName _ _ c =>
+    | .forallE binderName _ _ c =>
       let ctx ← read
       let argPos := (← get).argPos
       if ctx.elimInfo.motivePos == argPos then
@@ -131,13 +131,13 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
         modify fun s => { s with targetPos := s.targetPos + 1 }
         addNewArg target
       else match c with
-        | BinderInfo.implicit =>
+        | .implicit =>
           let arg ← mkFreshExprMVar (← getArgExpectedType)
           addNewArg arg
-        | BinderInfo.strictImplicit =>
+        | .strictImplicit =>
           let arg ← mkFreshExprMVar (← getArgExpectedType)
           addNewArg arg
-        | BinderInfo.instImplicit =>
+        | .instImplicit =>
           let arg ← mkFreshExprMVar (← getArgExpectedType) (kind := MetavarKind.synthetic) (userName := appendTag tag binderName)
           modify fun s => { s with insts := s.insts.push arg.mvarId! }
           addNewArg arg
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index a29b12f279..838d5d69cd 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -283,7 +283,7 @@ def observing (x : TermElabM α) : TermElabM (TermElabResult α) := do
     | ex@(.error ..) =>
       let sNew ← saveState
       s.restore (restoreInfo := true)
-      return EStateM.Result.error ex sNew
+      return .error ex sNew
     | ex@(.internal id _) =>
       if id == postponeExceptionId then
         s.restore (restoreInfo := true)
@@ -344,7 +344,7 @@ def withoutModifyingElabMetaStateWithInfo (x : TermElabM α) : TermElabM α := d
   let s ← get
   let sMeta ← getThe Meta.State
   try
-     withSaveInfoContext x
+    withSaveInfoContext x
   finally
     modify ({ s with infoState := ·.infoState })
     set sMeta