diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index e6e657698c..c4b50dac39 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -59,13 +59,12 @@ def mkBoxedVersionAux (decl : Decl) : N Decl := do
       pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) default), xs.push (Arg.var x))
   let r ← N.mkFresh
   let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) default)
-  let body ←
-    if !decl.resultType.isScalar then
-      pure <| reshape newVDecls (FnBody.ret (Arg.var r))
-    else
-      let newR ← N.mkFresh
-      let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) default)
-      pure <| reshape newVDecls (FnBody.ret (Arg.var newR))
+  let body ← if !decl.resultType.isScalar then
+    pure <| reshape newVDecls (FnBody.ret (Arg.var r))
+  else
+    let newR ← N.mkFresh
+    let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) default)
+    pure <| reshape newVDecls (FnBody.ret (Arg.var newR))
   return Decl.fdecl (mkBoxedName decl.name) qs IRType.object body decl.getInfo
 
 def mkBoxedVersion (decl : Decl) : Decl :=
diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean
index e4aca3bdcc..2408df3a64 100644
--- a/src/Lean/Data/Json/Parser.lean
+++ b/src/Lean/Data/Json/Parser.lean
@@ -97,30 +97,27 @@ def natMaybeZero : Parsec Nat := do
 
 def num : Parsec JsonNumber := do
   let c ← peek!
-  let sign : Int ←
-    if c = '-' then
-      skip
-      pure (-1 : Int)
-    else
-      pure 1
+  let sign ← if c = '-' then
+    skip
+    pure (-1 : Int)
+  else
+    pure 1
   let c ← peek!
-  let res ←
-    if c = '0' then
-      skip
-      pure 0
-    else
-      natNonZero
+  let res ← if c = '0' then
+    skip
+    pure 0
+  else
+    natNonZero
   let c? ← peek?
-  let res : JsonNumber ←
-    if c? = some '.' then
-      skip
-      let (n, d) ← natNumDigits
-      if d > USize.size then fail "too many decimals"
-      let mantissa' := sign * (res * (10^d : Nat) + n)
-      let exponent' := d
-      pure <| JsonNumber.mk mantissa' exponent'
-    else
-      pure <| JsonNumber.fromInt (sign * res)
+  let res : JsonNumber ← if c? = some '.' then
+    skip
+    let (n, d) ← natNumDigits
+    if d > USize.size then fail "too many decimals"
+    let mantissa' := sign * (res * (10^d : Nat) + n)
+    let exponent' := d
+    pure <| JsonNumber.mk mantissa' exponent'
+  else
+    pure <| JsonNumber.fromInt (sign * res)
   let c? ← peek?
   if c? = some 'e' ∨ c? = some 'E' then
     skip
diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean
index 08629c1977..64390e1e34 100644
--- a/src/Lean/DeclarationRange.lean
+++ b/src/Lean/DeclarationRange.lean
@@ -48,11 +48,10 @@ def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Opt
 
 def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m (Option DeclarationRanges) := do
   let env ← getEnv
-  let ranges ←
-    if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName)  then
-      findDeclarationRangesCore? declName.getPrefix
-    else
-      findDeclarationRangesCore? declName
+  let ranges ← if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName)  then
+    findDeclarationRangesCore? declName.getPrefix
+  else
+    findDeclarationRangesCore? declName
   match ranges with
   | none => return (← builtinDeclRanges.get (m := IO)).find? declName
   | some _ => return ranges
diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 3def8deb6f..8eac21f0cb 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -46,13 +46,11 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
   let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
   let attr := attrInstance[1]
   let attr ← liftMacroM <| expandMacros attr
-  let attrName ←
-    if attr.getKind == ``Parser.Attr.simple then
-      pure attr[0].getId.eraseMacroScopes
-    else
-      match attr.getKind with
-      | Name.str _ s _ => pure <| Name.mkSimple s
-      | _ => throwErrorAt attr  "unknown attribute"
+  let attrName ← if attr.getKind == ``Parser.Attr.simple then
+    pure attr[0].getId.eraseMacroScopes
+  else match attr.getKind with
+    | Name.str _ s _ => pure <| Name.mkSimple s
+    | _ => throwErrorAt attr  "unknown attribute"
   unless isAttribute (← getEnv) attrName do
     throwError "unknown attribute [{attrName}]"
   /- The `AttrM` does not have sufficient information for expanding macros in `args`.
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 51da3249fa..924ae23c10 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -606,20 +606,19 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       let val  ← mkLambdaFVars fvars val (usedLetOnly := false)
       pure (type, val, binders)
   trace[Elab.let.decl] "{id.getId} : {type} := {val}"
-  let result ←
-    if useLetExpr then
-      withLetDecl id.getId type val fun x => do
-        addLocalVarInfo id x
-        let body ← elabTermEnsuringType body expectedType?
-        let body ← instantiateMVars body
-        mkLetFVars #[x] body (usedLetOnly := usedLetOnly)
-    else
-      let f ← withLocalDecl id.getId BinderInfo.default type fun x => do
-        addLocalVarInfo id x
-        let body ← elabTermEnsuringType body expectedType?
-        let body ← instantiateMVars body
-        mkLambdaFVars #[x] body (usedLetOnly := false)
-      pure <| mkLetFunAnnotation (mkApp f val)
+  let result ← if useLetExpr then
+    withLetDecl id.getId type val fun x => do
+      addLocalVarInfo id x
+      let body ← elabTermEnsuringType body expectedType?
+      let body ← instantiateMVars body
+      mkLetFVars #[x] body (usedLetOnly := usedLetOnly)
+  else
+    let f ← withLocalDecl id.getId BinderInfo.default type fun x => do
+      addLocalVarInfo id x
+      let body ← elabTermEnsuringType body expectedType?
+      let body ← instantiateMVars body
+      mkLambdaFVars #[x] body (usedLetOnly := false)
+    pure <| mkLetFunAnnotation (mkApp f val)
   if elabBodyFirst then
     forallBoundedTelescope type binders.size fun xs type => do
       -- the original `fvars` from above are gone, so add back info manually
@@ -672,12 +671,11 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
       elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly
     else
       -- We are currently treating `let_fun` and `let` the same way when patterns are used.
-      let stxNew ←
-        if optType.isNone then
-          `(match $val:term with | $pat => $body)
-        else
-          let type := optType[0][1]
-          `(match ($val:term : $type) with | $pat => $body)
+      let stxNew ← if optType.isNone then
+        `(match $val:term with | $pat => $body)
+      else
+        let type := optType[0][1]
+        `(match ($val:term : $type) with | $pat => $body)
       withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   else if letDecl.getKind == ``Lean.Parser.Term.letEqnsDecl then
     let letDeclIdNew ← liftMacroM <| expandLetEqnsDecl letDecl
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index e7b73520be..fc215261c6 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -252,15 +252,14 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
   let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do
     modify fun s => { s with messages := prevMessages ++ s.messages.errorsToWarnings }
   let prevMessages ← resetMessages
-  let succeeded ←
-    try
-      x
-      hasNoErrorMessages
-    catch
-      | ex@(Exception.error _ _) => do logException ex; pure false
-      | Exception.internal id _  => do logError (← id.getName); pure false
-    finally
-      restoreMessages prevMessages
+  let succeeded ← try
+    x
+    hasNoErrorMessages
+  catch
+    | ex@(Exception.error _ _) => do logException ex; pure false
+    | Exception.internal id _  => do logError (← id.getName); pure false
+  finally
+    restoreMessages prevMessages
   if succeeded then
     throwError "unexpected success"
 
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 0583d4f4e6..5f49fd987f 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -54,16 +54,15 @@ are turned into a new anonymous constructor application. For example,
             let args := args.getElems
             if args.size < numExplicitFields then
               throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' has #{numExplicitFields} explicit fields, but only #{args.size} provided"
-            let newStx ←
-              if args.size == numExplicitFields then
-                `($(mkCIdentFrom stx ctor) $(args)*)
-              else if numExplicitFields == 0 then
-                throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' does not have explicit fields, but #{args.size} provided"
-              else
-                let extra := args[numExplicitFields-1:args.size]
-                let newLast ← `(⟨$[$extra],*⟩)
-                let newArgs := args[0:numExplicitFields-1].toArray.push newLast
-                `($(mkCIdentFrom stx ctor) $(newArgs)*)
+            let newStx ← if args.size == numExplicitFields then
+              `($(mkCIdentFrom stx ctor) $(args)*)
+            else if numExplicitFields == 0 then
+              throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' does not have explicit fields, but #{args.size} provided"
+            else
+              let extra := args[numExplicitFields-1:args.size]
+              let newLast ← `(⟨$[$extra],*⟩)
+              let newArgs := args[0:numExplicitFields-1].toArray.push newLast
+              `($(mkCIdentFrom stx ctor) $(newArgs)*)
             withMacroExpansion stx newStx $ elabTerm newStx expectedType?
           | _ => throwError "invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor {indentExpr expectedType}")
     | none => throwError "invalid constructor ⟨...⟩, expected type must be known"
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 65f7992b57..660ad2b29b 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -206,19 +206,18 @@ structure ExpandDeclIdResult where
 def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) : m ExpandDeclIdResult := do
   -- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
   let (shortName, optUnivDeclStx) := expandDeclIdCore declId
-  let levelNames ←
-    if optUnivDeclStx.isNone then
-      pure currLevelNames
-    else
-      let extraLevels := optUnivDeclStx[1].getArgs.getEvenElems
-      extraLevels.foldlM
-        (fun levelNames idStx =>
-          let id := idStx.getId
-          if levelNames.elem id then
-            withRef idStx <| throwAlreadyDeclaredUniverseLevel id
-          else
-            pure (id :: levelNames))
-        currLevelNames
+  let levelNames ← if optUnivDeclStx.isNone then
+    pure currLevelNames
+  else
+    let extraLevels := optUnivDeclStx[1].getArgs.getEvenElems
+    extraLevels.foldlM
+      (fun levelNames idStx =>
+        let id := idStx.getId
+        if levelNames.elem id then
+          withRef idStx <| throwAlreadyDeclaredUniverseLevel id
+        else
+          pure (id :: levelNames))
+      currLevelNames
   let (declName, shortName) ← withRef declId <| mkDeclName currNamespace modifiers shortName
   addDocString' declName modifiers.docString?
   return { shortName := shortName, declName := declName, levelNames := levelNames }
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 188c9af683..6b232a2da7 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -23,15 +23,13 @@ where
   mkSameCtorRhs : List (Syntax × Syntax × Bool × Bool) → TermElabM Syntax
     | [] => ``(isTrue rfl)
     | (a, b, recField, isProof) :: todo => withFreshMacroScope do
-      let rhs ←
-        if isProof
-        then
-          `(have h : $a = $b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
-        else
-          `(if h : $a = $b then
-             by subst h; exact $(← mkSameCtorRhs todo):term
-            else
-             isFalse (by intro n; injection n; apply h _; assumption))
+      let rhs ← if isProof then
+        `(have h : $a = $b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
+      else
+        `(if h : $a = $b then
+           by subst h; exact $(← mkSameCtorRhs todo):term
+          else
+           isFalse (by intro n; injection n; apply h _; assumption))
       if recField then
         -- add local instance for `a = b` using the function being defined `auxFunName`
         `(let inst := $(mkIdent auxFunName) $a $b; $rhs)
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 3e91cb78ab..45386697b1 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -167,11 +167,10 @@ where
           else `(Lean.Parser.Term.doExpr| fromJson? jsons[$(quote idx)])
         let identNames := binders.map Prod.fst
         let fromJsons ← binders.mapIdxM fun idx (_, type) => mkFromJson idx type
-
-        let userNamesOpt ←
-          if binders.size == userNames.size then
-            ``(some #[$[$(userNames.map quote):ident],*])
-          else ``(none)
+        let userNamesOpt ← if binders.size == userNames.size then
+          ``(some #[$[$(userNames.map quote):ident],*])
+        else
+          ``(none)
         let stx ←
           `((Json.parseTagged json $(quote ctor.getString!) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind
             (fun jsons => do
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 67c633b572..bf0f6f86f4 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -303,12 +303,11 @@ def attachJPs (jpDecls : Array JPDecl) (k : Code) : Code :=
   jpDecls.foldr attachJP k
 
 def mkFreshJP (ps : Array (Var × Bool)) (body : Code) : TermElabM JPDecl := do
-  let ps ←
-    if ps.isEmpty then
-      let y ← `(y)
-      pure #[(y, false)]
-    else
-      pure ps
+  let ps ← if ps.isEmpty then
+    let y ← `(y)
+    pure #[(y, false)]
+  else
+    pure ps
   -- Remark: the compiler frontend implemented in C++ currently detects jointpoints created by
   -- the "do" notation by testing the name. See hack at method `visit_let` at `lcnf.cpp`
   -- We will remove this hack when we re-implement the compiler frontend in Lean.
@@ -1271,11 +1270,10 @@ mutual
       let doElem  := decl[2]
       let optElse := decl[3]
       if optElse.isNone then withFreshMacroScope do
-        let auxDo ←
-          if isMutableLet doLetArrow then
-            `(do let discr ← $doElem; let mut $pattern:term := discr)
-          else
-            `(do let discr ← $doElem; let $pattern:term := discr)
+        let auxDo ← if isMutableLet doLetArrow then
+          `(do let discr ← $doElem; let mut $pattern:term := discr)
+        else
+          `(do let discr ← $doElem; let $pattern:term := discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         if isMutableLet doLetArrow then
@@ -1409,11 +1407,10 @@ mutual
       let uvarsTuple ← liftMacroM do mkTuple uvars
       if hasReturn forInBodyCodeBlock.code then
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ←
-          if let some h := h? then
-            `(for_in'% $(xs) (MProd.mk none $uvarsTuple) fun $x $h r => let r := r.2; $forInBody)
-          else
-            `(for_in% $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
+        let forInTerm ← if let some h := h? then
+          `(for_in'% $(xs) (MProd.mk none $uvarsTuple) fun $x $h r => let r := r.2; $forInBody)
+        else
+          `(for_in% $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
         let auxDo ← `(do let r ← $forInTerm:term;
                          $uvarsTuple:term := r.2;
                          match r.1 with
@@ -1422,11 +1419,10 @@ mutual
         doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
       else
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ←
-          if let some h := h? then
-            `(for_in'% $(xs) $uvarsTuple fun $x $h r => $forInBody)
-          else
-            `(for_in% $(xs) $uvarsTuple fun $x r => $forInBody)
+        let forInTerm ← if let some h := h? then
+          `(for_in'% $(xs) $uvarsTuple fun $x $h r => $forInBody)
+        else
+          `(for_in% $(xs) $uvarsTuple fun $x r => $forInBody)
         if doElems.isEmpty then
           let auxDo ← `(do let r ← $forInTerm:term;
                            $uvarsTuple:term := r;
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 10ddb85a2a..eb2b687f63 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -33,11 +33,10 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
         let m ← getMonadForIn expectedType?
         let colType ← inferType colFVar
         let elemType ← mkFreshExprMVar (mkSort (mkLevelSucc (← mkFreshLevelMVar)))
-        let forInInstance ←
-          try
-            mkAppM ``ForIn #[m, colType, elemType]
-          catch _ =>
-            tryPostpone; throwError "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
+        let forInInstance ← try
+          mkAppM ``ForIn #[m, colType, elemType]
+        catch _ =>
+          tryPostpone; throwError "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
         | LOption.some _   =>
           let forInFn ← mkConst ``forIn
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 3f49738fce..2a92e1d9c1 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -763,12 +763,11 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
         let numVars   := vars.size
         let numParams := numVars + numExplicitParams
         let indTypes ← updateParams vars indTypes
-        let indTypes ←
-          if let some univToInfer := univToInfer? then
-            updateResultingUniverse views numParams (← levelMVarToParam indTypes univToInfer)
-          else
-            checkResultingUniverses views numParams indTypes
-            levelMVarToParam indTypes none
+        let indTypes ← if let some univToInfer := univToInfer? then
+          updateResultingUniverse views numParams (← levelMVarToParam indTypes univToInfer)
+        else
+          checkResultingUniverses views numParams indTypes
+          levelMVarToParam indTypes none
         let usedLevelNames := collectLevelParamsInInductive indTypes
         match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
         | .error msg      => throwError msg
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index dfa2763582..bf9206a558 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -53,11 +53,10 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
           let type ← mkForallFVars xs type
           pure (type, binderIds)
       let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
-      let valStx ←
-        if decl.isOfKind `Lean.Parser.Term.letIdDecl then
-          pure decl[4]
-        else
-          liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
+      let valStx ← if decl.isOfKind `Lean.Parser.Term.letIdDecl then
+        pure decl[4]
+      else
+        liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
       pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx : LetRecDeclView }
     else
       throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean
index c1321de30b..4fda0d6e01 100644
--- a/src/Lean/Elab/Macro.lean
+++ b/src/Lean/Elab/Macro.lean
@@ -25,15 +25,14 @@ open Lean.Parser.Command
     let pat := mkNode ((← Macro.getCurrNamespace) ++ name) patArgs
     let stxCmd ← `($[$doc?:docComment]? $attrKind:attrKind
       syntax%$tk$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat)
-    let macroRulesCmd ←
-      if rhs.getArgs.size == 1 then
-        -- `rhs` is a `term`
-        let rhs := rhs[0]
-        `($[$doc?:docComment]? macro_rules%$tk | `($pat) => $rhs)
-      else
-        -- `rhs` is of the form `` `( $body ) ``
-        let rhsBody := rhs[1]
-        `($[$doc?:docComment]? macro_rules%$tk | `($pat) => `($rhsBody))
+    let macroRulesCmd ← if rhs.getArgs.size == 1 then
+      -- `rhs` is a `term`
+      let rhs := rhs[0]
+      `($[$doc?:docComment]? macro_rules%$tk | `($pat) => $rhs)
+    else
+      -- `rhs` is of the form `` `( $body ) ``
+      let rhsBody := rhs[1]
+      `($[$doc?:docComment]? macro_rules%$tk | `($pat) => `($rhsBody))
     return mkNullNode #[stxCmd, macroRulesCmd]
   | _ => Macro.throwUnsupported
 
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 176e73dc85..fb4e053f86 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -174,11 +174,9 @@ open Lean.Elab.Term.Quotation in
   | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
     discrs.forM precheck
     for (pats, rhs) in patss.zip rhss do
-      let vars ←
-        try
-          getPatternsVars pats
-        catch
-          | _ => return  -- can happen in case of pattern antiquotations
+      let vars ← try
+        getPatternsVars pats
+      catch | _ => return  -- can happen in case of pattern antiquotations
       Quotation.withNewLocals (getPatternVarNames vars) <| precheck rhs
   | _ => throwUnsupportedSyntax
 
@@ -920,11 +918,9 @@ where
       let first ← updateFirst first? ex
       s.restore (restoreInfo := true)
       let indices ← collectDeps #[index] (discrs.map (·.expr))
-      let matchType ←
-        try
-          updateMatchType indices matchType
-        catch _ =>
-          throwEx first
+      let matchType ← try
+        updateMatchType indices matchType
+      catch _ => throwEx first
       let ref ← getRef
       trace[Elab.match] "new indices to add as discriminants: {indices}"
       let wildcards ← indices.mapM fun index => do
diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index 1f7b025264..ec16e93c2a 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -189,11 +189,10 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
      -/
     let id := stx[0]
     discard <| processVar id
-    let h ←
-      if stx[2].isNone then
-        `(h)
-      else
-        pure stx[2][0]
+    let h ← if stx[2].isNone then
+      `(h)
+    else
+      pure stx[2][0]
     let pat := stx[3]
     let pat ← collect pat
     discard <| processVar h
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 6d2c1ee56c..53dff57c58 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -20,11 +20,10 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
   for preDef in preDefs do
     trace[Elab.definition] "processing {preDef.declName}"
     forallTelescope preDef.type fun xs type => do
-      let val ←
-        if useSorry then
-          mkLambdaFVars xs (← mkSorry type (synthetic := true))
-        else
-          liftM <| mkInhabitantFor preDef.declName xs type
+      let val ← if useSorry then
+        mkLambdaFVars xs (← mkSorry type (synthetic := true))
+      else
+        liftM <| mkInhabitantFor preDef.declName xs type
       addNonRec { preDef with
         kind  := DefKind.«opaque»
         value := val
diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index eb28fea59b..dc891f390a 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean
@@ -66,9 +66,10 @@ private def elimRecursion (preDef : PreDefinition) : M (Nat × PreDefinition) :=
     trace[Elab.definition.structural] "numFixed: {numFixed}"
     findRecArg numFixed xs fun recArgInfo => do
       -- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
-      let valueNew ←
-        if recArgInfo.indPred then mkIndPredBRecOn preDef.declName recArgInfo value
-        else mkBRecOn preDef.declName recArgInfo value
+      let valueNew ← if recArgInfo.indPred then
+        mkIndPredBRecOn preDef.declName recArgInfo value
+      else
+        mkBRecOn preDef.declName recArgInfo value
       let valueNew ← mkLambdaFVars xs valueNew
       trace[Elab.definition.structural] "result: {valueNew}"
       -- Recursive applications may still occur in expressions that were not visited by replaceRecApps (e.g., in types)
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 4b9d5e03e9..3308bb6646 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -135,10 +135,10 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
             | _ =>
               let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back
               `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr)
-          let arr ←
-            if k == `sepBy then
-              `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
-            else pure arr
+          let arr ← if k == `sepBy then
+            `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
+          else
+            pure arr
           let arr ← bindLets arr
           args := args.append (appendName := appendName) arr
         else do
@@ -411,17 +411,16 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
               uncovered
           | _ => uncovered,
         doMatch := fun yes no => do
-          let (cond, newDiscrs) ←
-            if lit then
-              let cond ← `(Syntax.matchesLit discr $(quote kind) $(quote (isLit? kind quoted).get!))
-              pure (cond, [])
-            else
-              let cond ← match kind with
-              | `null => `(Syntax.matchesNull discr $(quote argPats.size))
-              | `ident => `(Syntax.matchesIdent discr $(quote quoted.getId))
-              | _     => `(Syntax.isOfKind discr $(quote kind))
-              let newDiscrs ← (List.range argPats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
-              pure (cond, newDiscrs)
+          let (cond, newDiscrs) ← if lit then
+            let cond ← `(Syntax.matchesLit discr $(quote kind) $(quote (isLit? kind quoted).get!))
+            pure (cond, [])
+          else
+            let cond ← match kind with
+            | `null => `(Syntax.matchesNull discr $(quote argPats.size))
+            | `ident => `(Syntax.matchesIdent discr $(quote quoted.getId))
+            | _     => `(Syntax.isOfKind discr $(quote kind))
+            let newDiscrs ← (List.range argPats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
+            pure (cond, newDiscrs)
           `(ite (Eq $cond true) $(← yes newDiscrs) $(← no))
       }
   else match pat with
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index dd72ee479d..991b98c70f 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -184,19 +184,18 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
       else
         let (binders, type) := expandDeclSig fieldBinder[3]
         pure (binders, some type)
-    let value? ←
-      if binfo != BinderInfo.default then
+    let value? ← if binfo != BinderInfo.default then
+      pure none
+    else
+      let optBinderTacticDefault := fieldBinder[4]
+      -- trace[Elab.struct] ">>> {optBinderTacticDefault}"
+      if optBinderTacticDefault.isNone then
+        pure none
+      else if optBinderTacticDefault[0].getKind == ``Parser.Term.binderTactic then
         pure none
       else
-        let optBinderTacticDefault := fieldBinder[4]
-        -- trace[Elab.struct] ">>> {optBinderTacticDefault}"
-        if optBinderTacticDefault.isNone then
-          pure none
-        else if optBinderTacticDefault[0].getKind == ``Parser.Term.binderTactic then
-          pure none
-        else
-          -- binderDefault := leading_parser " := " >> termParser
-          pure (some optBinderTacticDefault[0][1])
+        -- binderDefault := leading_parser " := " >> termParser
+        pure (some optBinderTacticDefault[0][1])
     let idents := fieldBinder[2].getArgs
     idents.foldlM (init := views) fun (views : Array StructFieldView) ident => withRef ident do
       let rawName := ident.getId
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index b6756e44a7..000243d76c 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -321,12 +321,11 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   let catParserId := mkIdentFrom stx (cat.appendAfter "Parser")
   let (val, lhsPrec?) ← runTermElabM none fun _ => Term.toParserDescr syntaxParser cat
   let declName := mkIdentFrom stx name
-  let d ←
-    if let some lhsPrec := lhsPrec? then
-      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.TrailingParserDescr :=
+  let d ← if let some lhsPrec := lhsPrec? then
+    `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.TrailingParserDescr :=
         ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
-    else
-      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.ParserDescr :=
+  else
+    `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.ParserDescr :=
         ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
   trace `Elab fun _ => d
   withMacroExpansion stx d <| elabCommand d
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index bd347cd43b..c7def51b42 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -307,13 +307,12 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
 
 private def getCaseGoals (tag : Syntax) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals
-  let g ←
-    if tag.isIdent then
-      let tag := tag.getId
-      let some g ← findTag? gs tag | throwError "tag not found"
-      pure g
-    else
-      getMainGoal
+  let g ← if tag.isIdent then
+    let tag := tag.getId
+    let some g ← findTag? gs tag | throwError "tag not found"
+    pure g
+  else
+    getMainGoal
   return (g, gs.erase g)
 
 @[builtinTactic «case»] def evalCase : Tactic
diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index 8a91b0ae4f..5342dc1437 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -19,11 +19,10 @@ private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List (Option MV
     let mut newGoals : Array (Option MVarId) := #[]
     let mut i := 0
     for arg in args do
-      let addGoal ←
-        if i < infos.size then
-          pure infos[i].binderInfo.isExplicit
-        else
-          pure (← whnfD (← inferType r.expr)).isArrow
+      let addGoal ← if i < infos.size then
+        pure infos[i].binderInfo.isExplicit
+      else
+        pure (← whnfD (← inferType r.expr)).isArrow
       let hasFwdDep := i < infos.size && infos[i].hasFwdDeps
       if addGoal then
         if hasFwdDep then
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 1104bb4828..b3d2efc8f3 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -70,15 +70,14 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix :
   let newMVarIds ← getMVarsNoDelayed val
   /- ignore let-rec auxiliary variables, they are synthesized automatically later -/
   let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId)
-  let newMVarIds ←
-    if allowNaturalHoles then
-      pure newMVarIds.toList
-    else
-      let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural
-      let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural
-      let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved
-      logUnassignedAndAbort naturalMVarIds
-      pure syntheticMVarIds.toList
+  let newMVarIds ← if allowNaturalHoles then
+    pure newMVarIds.toList
+  else
+    let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural
+    let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural
+    let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved
+    logUnassignedAndAbort naturalMVarIds
+    pure syntheticMVarIds.toList
   tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
   pure (val, newMVarIds)
 
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 19727aafd7..a4b3299e42 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -212,11 +212,10 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
       throwError "'dsimp' tactic does not support 'discharger' option"
   let dischargeWrapper ← mkDischargeWrapper stx[2]
   let simpOnly := !stx[3].isNone
-  let simpTheorems ←
-    if simpOnly then
-      ({} : SimpTheorems).addConst ``eq_self
-    else
-      getSimpTheorems
+  let simpTheorems ← if simpOnly then
+    ({} : SimpTheorems).addConst ``eq_self
+  else
+    getSimpTheorems
   let congrTheorems ← getSimpCongrTheorems
   let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
     config      := (← elabSimpConfig stx[1] (kind := kind))
diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index 4603931234..31a4fe9750 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -44,11 +44,10 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
         if !(← isProp arg1Type) && arg1 != arg2 then
           eqs := eqs.push (← mkEqHEq arg1 arg2)
       if let some andEqs := mkAnd? eqs then
-        let result ←
-          if useEq then
-            mkEq eq andEqs
-          else
-            mkArrow eq andEqs
+        let result ← if useEq then
+          mkEq eq andEqs
+        else
+          mkArrow eq andEqs
         mkForallFVars params (← mkForallFVars args1 (← mkForallFVars args2New result))
       else
         return none
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index dcfbfc521a..dbd15a7de8 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/src/Lean/Meta/Match/CaseValues.lean
@@ -90,12 +90,11 @@ def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNameP
           | Expr.fvar fvarId _ => tryClear thenMVarId fvarId
           | _                  => pure thenMVarId)
         thenSubgoal.mvarId
-      let subgoals ←
-         if substNewEqs then
-           let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH false thenSubgoal.subst true
-           pure <| subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
-         else
-           pure <| subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }
+      let subgoals ← if substNewEqs then
+         let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH false thenSubgoal.subst true
+         pure <| subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
+      else
+         pure <| subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }
       match vs with
       | [] => do
         appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index b0e0861c58..90190bb42b 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -104,13 +104,12 @@ where
                return (← go ys eqs args (mask.push false) (i+1) typeNew)
           go (ys.push y) eqs (args.push y) (mask.push true) (i+1) typeNew
       else
-        let arg ←
-           if let some (_, _, rhs) ← matchEq? d then
-             mkEqRefl rhs
-           else if let some (_, _, _, rhs) ← matchHEq? d then
-             mkHEqRefl rhs
-           else
-             throwError "unexpected match alternative type{indentExpr altType}"
+        let arg ← if let some (_, _, rhs) ← matchEq? d then
+          mkEqRefl rhs
+        else if let some (_, _, _, rhs) ← matchHEq? d then
+          mkHEqRefl rhs
+        else
+          throwError "unexpected match alternative type{indentExpr altType}"
         withLocalDeclD n d fun eq => do
           let typeNew := b.instantiate1 eq
           go ys (eqs.push eq) (args.push arg) (mask.push false) (i+1) typeNew
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index eacfa86253..72b683e446 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -427,13 +427,12 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
       let thmName   := mkSizeOfSpecLemmaName ctorName
       let thmParams := params ++ localInsts ++ fields
       let thmType ← mkForallFVars thmParams target
-      let thmValue ←
-        if indInfo.isNested then
-          SizeOfSpecNested.main lhs rhs |>.run {
-            indInfo := indInfo, sizeOfFns := sizeOfFns, ctorName := ctorName, params := params, localInsts := localInsts, recMap := recMap
-          }
-        else
-          mkEqRefl rhs
+      let thmValue ← if indInfo.isNested then
+        SizeOfSpecNested.main lhs rhs |>.run {
+          indInfo := indInfo, sizeOfFns := sizeOfFns, ctorName := ctorName, params := params, localInsts := localInsts, recMap := recMap
+        }
+      else
+        mkEqRefl rhs
       let thmValue ← mkLambdaFVars thmParams thmValue
       trace[Meta.sizeOf] "sizeOf spec theorem: {thmName}"
       addDecl <| Declaration.thmDecl {
diff --git a/src/Lean/Meta/Tactic/Generalize.lean b/src/Lean/Meta/Tactic/Generalize.lean
index 1e0ecbef09..90f8d3c430 100644
--- a/src/Lean/Meta/Tactic/Generalize.lean
+++ b/src/Lean/Meta/Tactic/Generalize.lean
@@ -51,11 +51,10 @@ partial def generalize
               let xType ← inferType xs[i]
               let e ← instantiateMVars arg.expr
               let eType ← instantiateMVars (← inferType e)
-              let (hType, r) ←
-                if (← isDefEq xType eType) then
-                  pure (← mkEq e xs[i], ← mkEqRefl e)
-                else
-                  pure (← mkHEq e xs[i], ← mkHEqRefl e)
+              let (hType, r) ← if (← isDefEq xType eType) then
+                pure (← mkEq e xs[i], ← mkEqRefl e)
+              else
+                pure (← mkHEq e xs[i], ← mkHEqRefl e)
               let (rs, type) ← go' (i+1)
               return (r :: rs, mkForall hName BinderInfo.default hType type)
             else
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index 1fba05f5e7..d6e5e52036 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -196,11 +196,10 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
             let recursor ← addRecParams mvarId majorTypeArgs recursorInfo.paramsPos recursor
             -- Compute motive
             let motive := target
-            let motive ←
-              if recursorInfo.depElim then
-                pure <| mkLambda `x BinderInfo.default (← inferType major) (← abstract motive #[major])
-              else
-                pure motive
+            let motive ← if recursorInfo.depElim then
+              pure <| mkLambda `x BinderInfo.default (← inferType major) (← abstract motive #[major])
+            else
+              pure motive
             let motive ← mkLambdaFVars indices motive
             let recursor := mkApp recursor motive
             finalize mvarId givenNames recursorInfo reverted major indices baseSubst recursor
diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean
index fc44957751..8d32e4842f 100644
--- a/src/Lean/Meta/Tactic/Refl.lean
+++ b/src/Lean/Meta/Tactic/Refl.lean
@@ -16,11 +16,10 @@ def refl (mvarId : MVarId) : MetaM Unit := do
       throwTacticEx `rfl mvarId m!"equality expected{indentExpr targetType}"
     let lhs ← instantiateMVars targetType.appFn!.appArg!
     let rhs ← instantiateMVars targetType.appArg!
-    let success ←
-      if (← useKernel lhs rhs) then
-        pure (Kernel.isDefEq (← getEnv) {} lhs rhs)
-      else
-        isDefEq lhs rhs
+    let success ← if (← useKernel lhs rhs) then
+      pure (Kernel.isDefEq (← getEnv) {} lhs rhs)
+    else
+      isDefEq lhs rhs
     unless success do
       throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
     let us := targetType.getAppFn.constLevels!
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index ac985a0ecb..79d4de9557 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -435,15 +435,14 @@ where
       | CongrArgKind.cast  => pure ()
       | CongrArgKind.subsingletonInst =>
         let clsNew := type.bindingDomain!.instantiateRev subst
-        let instNew ←
-          if (← isDefEq (← inferType arg) clsNew) then
-            pure arg
-          else
-            match (← trySynthInstance clsNew) with
-            | LOption.some val => pure val
-            | _ =>
-              trace[Meta.Tactic.simp.congr] "failed to synthesize instance{indentExpr clsNew}"
-              return none
+        let instNew ← if (← isDefEq (← inferType arg) clsNew) then
+          pure arg
+        else
+          match (← trySynthInstance clsNew) with
+          | LOption.some val => pure val
+          | _ =>
+            trace[Meta.Tactic.simp.congr] "failed to synthesize instance{indentExpr clsNew}"
+            return none
         proof := mkApp proof instNew
         subst := subst.push instNew
         type := type.bindingBody!
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 834347db5e..61656c387c 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -57,15 +57,14 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.getName xs bis discharge?) do
         return none
-      let proof? ←
-        if thm.rfl then
-          pure none
-        else
-          let proof ← instantiateMVars (mkAppN val xs)
-          if (← hasAssignableMVar proof) then
-            trace[Meta.Tactic.simp.rewrite] "{thm}, has unassigned metavariables after unification"
-            return none
-          pure <| some proof
+      let proof? ← if thm.rfl then
+        pure none
+      else
+        let proof ← instantiateMVars (mkAppN val xs)
+        if (← hasAssignableMVar proof) then
+          trace[Meta.Tactic.simp.rewrite] "{thm}, has unassigned metavariables after unification"
+          return none
+        pure <| some proof
       let rhs := (← instantiateMVars type).appArg!
       if e == rhs then
         return none
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 095fd09ca5..466d4783ff 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -216,13 +216,12 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
   let discrsNew := discrFVarIdsNew.map mkFVar
   let mvarType ← getMVarType mvarId
   let elimUniv ← withMVarContext mvarId <| getLevel mvarType
-  let us ←
-    if let some uElimPos := info.uElimPos? then
-      pure <| us.set! uElimPos elimUniv
-    else
-      unless elimUniv.isZero do
-        throwError "match-splitter can only eliminate into `Prop`"
-      pure us
+  let us ← if let some uElimPos := info.uElimPos? then
+    pure <| us.set! uElimPos elimUniv
+  else
+    unless elimUniv.isZero do
+      throwError "match-splitter can only eliminate into `Prop`"
+    pure us
   let splitter := mkAppN (mkConst matchEqns.splitterName us.toList) params
   withMVarContext mvarId do
     let motive ← mkLambdaFVars discrsNew mvarType
diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index 5b869108fd..71e1fd0ee0 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -42,13 +42,12 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
         let hFVarId := twoVars[1]
         let h       := mkFVar hFVarId
         /- Set skip to true if there is no local variable nor the target depend on the equality -/
-        let skip ←
-          if !tryToSkip || vars.size != 2 then
-            pure false
-          else
-            let mvarType ← getMVarType mvarId
-            let mctx ← getMCtx
-            pure (!mctx.exprDependsOn mvarType aFVarId && !mctx.exprDependsOn mvarType hFVarId)
+        let skip ← if !tryToSkip || vars.size != 2 then
+          pure false
+        else
+          let mvarType ← getMVarType mvarId
+          let mctx ← getMCtx
+          pure (!mctx.exprDependsOn mvarType aFVarId && !mctx.exprDependsOn mvarType hFVarId)
         if skip then
           if clearH then
             let mvarId ← clear mvarId hFVarId
@@ -74,12 +73,11 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
                 let newVal  ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major
                 assignExprMVar mvarId newVal
                 let mvarId := newMVar.mvarId!
-                let mvarId ←
-                  if clearH then
-                    let mvarId ← clear mvarId hFVarId
-                    clear mvarId aFVarId
-                  else
-                    pure mvarId
+                let mvarId ← if clearH then
+                  let mvarId ← clear mvarId hFVarId
+                  clear mvarId aFVarId
+                else
+                  pure mvarId
                 let (newFVars, mvarId) ← introNP mvarId (vars.size - 2)
                 trace[Meta.Tactic.subst] "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}"
                 let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) =>
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 0b0f71c43c..e94fa1e0e1 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -90,18 +90,17 @@ def delabConst : Delab := do
   let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
 
   let mut c ← unresolveNameGlobal c₀
-  let stx ←
-    if ls.isEmpty || !(← getPPOption getPPUniverses) then
-      if (← getLCtx).usesUserName c then
-        -- `c` is also a local declaration
-        if c == c₀ && !(← read).inPattern then
-          -- `c` is the fully qualified named. So, we append the `_root_` prefix
-          c := `_root_ ++ c
-        else
-          c := c₀
-      pure <| mkIdent c
-    else
-      `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
+  let stx ← if ls.isEmpty || !(← getPPOption getPPUniverses) then
+    if (← getLCtx).usesUserName c then
+      -- `c` is also a local declaration
+      if c == c₀ && !(← read).inPattern then
+        -- `c` is the fully qualified named. So, we append the `_root_` prefix
+        c := `_root_ ++ c
+      else
+        c := c₀
+    pure <| mkIdent c
+  else
+    `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
 
   let mut stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 832e2fc8af..2e208a1183 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -346,11 +346,10 @@ where
 
 private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (hoverInfo : HoverInfo) (expectedType? : Option Expr) : IO (Option CompletionList) :=
   runM ctx info.lctx do
-    let nameSet ←
-      try
-        getDotCompletionTypeNames (← instantiateMVars (← inferType info.expr))
-      catch _ =>
-        pure {}
+    let nameSet ← try
+      getDotCompletionTypeNames (← instantiateMVars (← inferType info.expr))
+    catch _ =>
+      pure {}
     if nameSet.isEmpty then
       if info.stx.isIdent then
         idCompletionCore ctx info.stx.getId hoverInfo (danglingDot := false) expectedType?
diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index 9e60615bb2..32d051f644 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
-some { range := { pos := { line := 148, column := 41 },
+some { range := { pos := { line := 147, column := 41 },
     charUtf16 := 41,
-    endPos := { line := 154, column := 70 },
+    endPos := { line := 153, column := 70 },
     endCharUtf16 := 70 },
-  selectionRange := { pos := { line := 148, column := 45 },
+  selectionRange := { pos := { line := 147, column := 45 },
     charUtf16 := 45,
-    endPos := { line := 148, column := 57 },
+    endPos := { line := 147, column := 57 },
     endCharUtf16 := 57 } }