diff --git a/src/Lean/Elab/Tactic/Binders.lean b/src/Lean/Elab/Tactic/Binders.lean
index 7d16b1ca3a..dabb51ec6b 100644
--- a/src/Lean/Elab/Tactic/Binders.lean
+++ b/src/Lean/Elab/Tactic/Binders.lean
@@ -6,8 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Elab.Tactic.Basic
 namespace Lean.Elab.Tactic
 
-private def liftTermBinderSyntax : Macro :=
-fun stx => do
+private def liftTermBinderSyntax : Macro := fun stx => do
   let hole ← `(?_)
   match stx.getKind with
   | Name.str (Name.str p "Tactic" _) s _ =>
@@ -21,8 +20,7 @@ fun stx => do
 @[builtinMacro Lean.Parser.Tactic.«let!»] def expandLetBangTactic : Macro := liftTermBinderSyntax
 @[builtinMacro Lean.Parser.Tactic.suffices] def expandSufficesTactic : Macro := liftTermBinderSyntax
 
-@[builtinMacro Lean.Parser.Tactic.show] def expandShowTactic : Macro :=
-fun stx =>
+@[builtinMacro Lean.Parser.Tactic.show] def expandShowTactic : Macro := fun stx =>
   let type := stx[1]
   `(tactic| refine (show $type from ?_))
 
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 3f41c0b495..cb84c808cd 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -15,17 +15,17 @@ open Meta
 /- `elabTerm` for Tactics and basic tactics that use it. -/
 
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr :=
-withRef stx $ liftTermElabM $ Term.withoutErrToSorry do
-  let e ← Term.elabTerm stx expectedType?
-  Term.synthesizeSyntheticMVars mayPostpone
-  instantiateMVars e
+  withRef stx $ liftTermElabM $ Term.withoutErrToSorry do
+    let e ← Term.elabTerm stx expectedType?
+    Term.synthesizeSyntheticMVars mayPostpone
+    instantiateMVars e
 
 def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
-let e ← elabTerm stx expectedType? mayPostpone
-ensureHasType expectedType? e
+  let e ← elabTerm stx expectedType? mayPostpone
+  ensureHasType expectedType? e
 
-@[builtinTactic «exact»] def evalExact : Tactic :=
-fun stx => match_syntax stx with
+@[builtinTactic «exact»] def evalExact : Tactic := fun stx =>
+  match_syntax stx with
   | `(tactic| exact $e) => do
     let (g, gs) ← getMainGoal
     withMVarContext g do
@@ -36,47 +36,47 @@ fun stx => match_syntax stx with
     setGoals gs
   | _ => throwUnsupportedSyntax
 
-@[builtinMacro Lean.Parser.Tactic.admit] def expandAdmit : Macro :=
-fun _ => `(tactic| exact sorry)
+@[builtinMacro Lean.Parser.Tactic.admit] def expandAdmit : Macro := fun _ =>
+  `(tactic| exact sorry)
 
 def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
-let val ← elabTermEnsuringType stx expectedType?
-let newMVarIds ← getMVarsNoDelayed val
-let newMVarIds ←
-  if allowNaturalHoles then
-    pure newMVarIds.toList
-  else
-    let naturalMVarIds ← newMVarIds.filterM fun mvarId => do return (← getMVarDecl mvarId).kind.isNatural
-    let syntheticMVarIds ← newMVarIds.filterM fun mvarId => do return !(← getMVarDecl mvarId).kind.isNatural
-    Term.logUnassignedUsingErrorInfos naturalMVarIds
-    pure syntheticMVarIds.toList
-tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
-pure (val, newMVarIds)
+  let val ← elabTermEnsuringType stx expectedType?
+  let newMVarIds ← getMVarsNoDelayed val
+  let newMVarIds ←
+    if allowNaturalHoles then
+      pure newMVarIds.toList
+    else
+      let naturalMVarIds ← newMVarIds.filterM fun mvarId => do return (← getMVarDecl mvarId).kind.isNatural
+      let syntheticMVarIds ← newMVarIds.filterM fun mvarId => do return !(← getMVarDecl mvarId).kind.isNatural
+      Term.logUnassignedUsingErrorInfos naturalMVarIds
+      pure syntheticMVarIds.toList
+  tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
+  pure (val, newMVarIds)
 
 /- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
    Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be
    filled by typing constraints.
    "Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation `?<hole-name>`. -/
 def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : TacticM Unit := do
-let (g, gs) ← getMainGoal
-withMVarContext g do
-  let decl ← getMVarDecl g
-  let (val, gs') ← elabTermWithHoles stx decl.type tagSuffix allowNaturalHoles
-  assignExprMVar g val
-  setGoals (gs ++ gs')
+  let (g, gs) ← getMainGoal
+  withMVarContext g do
+    let decl ← getMVarDecl g
+    let (val, gs') ← elabTermWithHoles stx decl.type tagSuffix allowNaturalHoles
+    assignExprMVar g val
+    setGoals (gs ++ gs')
 
-@[builtinTactic «refine»] def evalRefine : Tactic :=
-fun stx => match_syntax stx with
+@[builtinTactic «refine»] def evalRefine : Tactic := fun stx =>
+  match_syntax stx with
   | `(tactic| refine $e) => refineCore e `refine false
   | _                    => throwUnsupportedSyntax
 
-@[builtinTactic «refine!»] def evalRefineBang : Tactic :=
-fun stx => match_syntax stx with
+@[builtinTactic «refine!»] def evalRefineBang : Tactic := fun stx =>
+  match_syntax stx with
   | `(tactic| refine! $e) => refineCore e `refine true
   | _                     => throwUnsupportedSyntax
 
-@[builtinTactic Lean.Parser.Tactic.apply] def evalApply : Tactic :=
-fun stx => match_syntax stx with
+@[builtinTactic Lean.Parser.Tactic.apply] def evalApply : Tactic := fun stx =>
+  match_syntax stx with
   | `(tactic| apply $e) => do
     let (g, gs) ← getMainGoal
     let gs' ← withMVarContext g do
@@ -93,21 +93,21 @@ fun stx => match_syntax stx with
   Elaborate `stx`. If it a free variable, return it. Otherwise, assert it, and return the free variable.
   Note that, the main goal is updated when `Meta.assert` is used in the second case. -/
 def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId := do
-let (mvarId, others) ← getMainGoal
-withMVarContext mvarId do
-  let e ← elabTerm stx none
-  match e with
-  | Expr.fvar fvarId _ => pure fvarId
-  | _ =>
-    let type ← inferType e
-    let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do
-      let (fvarId, mvarId) ← liftMetaM do
-        mvarId ← Meta.assert mvarId userName type e
-        Meta.intro1Core mvarId preserveBinderNames
-      setGoals $ mvarId::others
-      pure fvarId
-    match userName? with
-    | none          => intro `h false
-    | some userName => intro userName true
+  let (mvarId, others) ← getMainGoal
+  withMVarContext mvarId do
+    let e ← elabTerm stx none
+    match e with
+    | Expr.fvar fvarId _ => pure fvarId
+    | _ =>
+      let type ← inferType e
+      let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do
+        let (fvarId, mvarId) ← liftMetaM do
+          mvarId ← Meta.assert mvarId userName type e
+          Meta.intro1Core mvarId preserveBinderNames
+        setGoals $ mvarId::others
+        pure fvarId
+      match userName? with
+      | none          => intro `h false
+      | some userName => intro userName true
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean
index 3f3caa8b0d..ed4484587a 100644
--- a/src/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Lean/Elab/Tactic/Generalize.lean
@@ -12,59 +12,58 @@ namespace Lean.Elab.Tactic
 open Meta
 
 private def getAuxHypothesisName (stx : Syntax) : Option Name :=
-if stx[1].isNone then none
-else some stx[1][0].getId
+  if stx[1].isNone then none
+  else some stx[1][0].getId
 
 private def getVarName (stx : Syntax) : Name :=
-stx[4].getId
+  stx[4].getId
 
 private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
-let tag    ← Meta.getMVarTag mvarId
-let eType  ← inferType e
-let u      ← Meta.getLevel eType
-let mvar'  ← Meta.mkFreshExprSyntheticOpaqueMVar target tag
-let rfl    := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e
-let val    := mkApp2 mvar' e rfl
-assignExprMVar mvarId val
-let mvarId' := mvar'.mvarId!
-(_, mvarId') ← Meta.introNP mvarId' 2
-pure [mvarId']
+  let tag    ← Meta.getMVarTag mvarId
+  let eType  ← inferType e
+  let u      ← Meta.getLevel eType
+  let mvar'  ← Meta.mkFreshExprSyntheticOpaqueMVar target tag
+  let rfl    := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e
+  let val    := mkApp2 mvar' e rfl
+  assignExprMVar mvarId val
+  let mvarId' := mvar'.mvarId!
+  (_, mvarId') ← Meta.introNP mvarId' 2
+  pure [mvarId']
 
 private def evalGeneralizeWithEq (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
-liftMetaTactic fun mvarId => do
-  let mvarId      ← Meta.generalize mvarId e x false
-  let mvarDecl    ← getMVarDecl mvarId
-  match mvarDecl.type with
-  | Expr.forallE _ _ b _ =>
-    let (_, mvarId) ← Meta.intro1P mvarId
-    let eType       ← inferType e
-    let u           ← Meta.getLevel eType
-    let eq          := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0)
-    let target      := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1)
-    evalGeneralizeFinalize mvarId e target
-  | _ => throwError "unexpected type after generalize"
+  liftMetaTactic fun mvarId => do
+    let mvarId      ← Meta.generalize mvarId e x false
+    let mvarDecl    ← getMVarDecl mvarId
+    match mvarDecl.type with
+    | Expr.forallE _ _ b _ =>
+      let (_, mvarId) ← Meta.intro1P mvarId
+      let eType       ← inferType e
+      let u           ← Meta.getLevel eType
+      let eq          := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0)
+      let target      := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1)
+      evalGeneralizeFinalize mvarId e target
+    | _ => throwError "unexpected type after generalize"
 
 -- If generalizing fails, fall back to not replacing anything
 private def evalGeneralizeFallback (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
-liftMetaTactic fun mvarId => do
-  let eType    ← inferType e
-  let u        ← Meta.getLevel eType
-  let mvarType ← Meta.getMVarType mvarId
-  let eq       := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0)
-  let target   := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq mvarType
-  evalGeneralizeFinalize mvarId e target
+  liftMetaTactic fun mvarId => do
+    let eType    ← inferType e
+    let u        ← Meta.getLevel eType
+    let mvarType ← Meta.getMVarType mvarId
+    let eq       := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0)
+    let target   := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq mvarType
+    evalGeneralizeFinalize mvarId e target
 
 def evalGeneralizeAux (h? : Option Name) (e : Expr) (x : Name) : TacticM Unit :=
-match h? with
-| none   => liftMetaTactic fun mvarId => do
-  let mvarId ← Meta.generalize mvarId e x false
-  let (_, mvarId) ← Meta.intro1P mvarId
-  pure [mvarId]
-| some h =>
-  evalGeneralizeWithEq h e x <|> evalGeneralizeFallback h e x
+  match h? with
+  | none   => liftMetaTactic fun mvarId => do
+    let mvarId ← Meta.generalize mvarId e x false
+    let (_, mvarId) ← Meta.intro1P mvarId
+    pure [mvarId]
+  | some h =>
+    evalGeneralizeWithEq h e x <|> evalGeneralizeFallback h e x
 
-@[builtinTactic Lean.Parser.Tactic.generalize] def evalGeneralize : Tactic :=
-fun stx => do
+@[builtinTactic Lean.Parser.Tactic.generalize] def evalGeneralize : Tactic := fun stx => do
   let h? := getAuxHypothesisName stx
   let x  := getVarName stx
   let e ← elabTerm stx[2] none
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index d4b1177af9..009edab774 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -16,36 +16,36 @@ open Meta
 -- Recall that
 -- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
 private def getAuxHypothesisName (stx : Syntax) : Option Name :=
-if stx[1][0].isNone then
-  none
-else
-  some stx[1][0][0].getId
+  if stx[1][0].isNone then
+    none
+  else
+    some stx[1][0][0].getId
 
 private def getMajor (stx : Syntax) : Syntax :=
-stx[1][1]
+  stx[1][1]
 
 private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
-match h? with
-| none   => withMainMVarContext $ elabTerm major none
-| some h => withMainMVarContext do
-  let lctx ← getLCtx
-  let x := lctx.getUnusedName `x
-  let major ← elabTerm major none
-  evalGeneralizeAux h? major x
-  withMainMVarContext do
+  match h? with
+  | none   => withMainMVarContext $ elabTerm major none
+  | some h => withMainMVarContext do
     let lctx ← getLCtx
-    match lctx.findFromUserName? x with
-    | some decl => pure decl.toExpr
-    | none      => throwError "failed to generalize"
+    let x := lctx.getUnusedName `x
+    let major ← elabTerm major none
+    evalGeneralizeAux h? major x
+    withMainMVarContext do
+      let lctx ← getLCtx
+      match lctx.findFromUserName? x with
+      | some decl => pure decl.toExpr
+      | none      => throwError "failed to generalize"
 
 private def generalizeMajor (major : Expr) : TacticM Expr := do
-match major with
-| Expr.fvar _ _ => pure major
-| _ =>
-  liftMetaTacticAux fun mvarId => do
-    mvarId ← Meta.generalize mvarId major `x false
-    let (fvarId, mvarId) ← Meta.intro1 mvarId
-    pure (mkFVar fvarId, [mvarId])
+  match major with
+  | Expr.fvar _ _ => pure major
+  | _ =>
+    liftMetaTacticAux fun mvarId => do
+      mvarId ← Meta.generalize mvarId major `x false
+      let (fvarId, mvarId) ← Meta.intro1 mvarId
+      pure (mkFVar fvarId, [mvarId])
 
 /-
   Recall that
@@ -55,26 +55,26 @@ match major with
   ```
   `stx` is syntax for `induction`. -/
 private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
-withRef stx $
-let generalizingStx := stx[3]
-if generalizingStx.isNone then
-  pure #[]
-else withMainMVarContext do
-  trace `Elab.induction fun _ => generalizingStx
-  let vars := generalizingStx[1].getArgs
-  getFVarIds vars
+  withRef stx do
+    let generalizingStx := stx[3]
+    if generalizingStx.isNone then
+      pure #[]
+    else withMainMVarContext do
+      trace `Elab.induction fun _ => generalizingStx
+      let vars := generalizingStx[1].getArgs
+      getFVarIds vars
 
 -- process `generalizingVars` subterm of induction Syntax `stx`.
 private def generalizeVars (stx : Syntax) (major : Expr) : TacticM Nat := do
-let fvarIds ← getGeneralizingFVarIds stx
-liftMetaTacticAux fun mvarId => do
-  let (fvarIds, mvarId') ← Meta.revert mvarId fvarIds
-  if fvarIds.contains major.fvarId! then
-    Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized"
-  pure (fvarIds.size, [mvarId'])
+  let fvarIds ← getGeneralizingFVarIds stx
+  liftMetaTacticAux fun mvarId => do
+    let (fvarIds, mvarId') ← Meta.revert mvarId fvarIds
+    if fvarIds.contains major.fvarId! then
+      Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized"
+    pure (fvarIds.size, [mvarId'])
 
 private def getAlts (withAlts : Syntax) : Array Syntax :=
-withAlts[2].getSepArgs
+  withAlts[2].getSepArgs
 
 /-
   Given an `inductionAlt` of the form
@@ -93,27 +93,26 @@ private def getAltRHS (alt : Syntax) : Syntax := alt[3]
   esnure the first `ident'` is `_` or a constructor name.
 -/
 private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit := do
-for alt in alts do
-  let n := getAltName alt
-  withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}"
-  unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do
-    throwErrorAt! alt[0] "invalid constructor name '{n}'"
+  for alt in alts do
+    let n := getAltName alt
+    withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}"
+    unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do
+      throwErrorAt! alt[0] "invalid constructor name '{n}'"
 
 structure RecInfo :=
-(recName : Name)
-(altVars : Array (List Name) := #[]) -- new variable names for each minor premise
-(altRHSs : Array Syntax := #[])      -- RHS for each minor premise
+  (recName : Name)
+  (altVars : Array (List Name) := #[]) -- new variable names for each minor premise
+  (altRHSs : Array Syntax := #[])      -- RHS for each minor premise
 
 def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
-liftMetaMAtMain fun mvarId => do
-  let majorType ← inferType major
-  let majorType ← whnf majorType
-  matchConstInduct majorType.getAppFn
-    (fun _ => Meta.throwTacticEx `induction mvarId msg!"major premise type is not an inductive type {indentExpr majorType}")
-    (fun val _ => pure val)
+  liftMetaMAtMain fun mvarId => do
+    let majorType ← inferType major
+    let majorType ← whnf majorType
+    matchConstInduct majorType.getAppFn
+      (fun _ => Meta.throwTacticEx `induction mvarId msg!"major premise type is not an inductive type {indentExpr majorType}")
+      (fun val _ => pure val)
 
-private partial def getRecFromUsingLoop (baseRecName : Name) : Expr → TacticM (Option Meta.RecursorInfo)
-| majorType => do
+private partial def getRecFromUsingLoop (baseRecName : Name) (majorType : Expr) : TacticM (Option Meta.RecursorInfo) := do
   let finalize (majorType : Expr) : TacticM (Option Meta.RecursorInfo) := do
     let majorType? ← unfoldDefinition? majorType
     match majorType? with
@@ -135,57 +134,57 @@ private partial def getRecFromUsingLoop (baseRecName : Name) : Expr → TacticM
   | _ => finalize majorType
 
 def getRecFromUsing (major : Expr) (baseRecName : Name) : TacticM Meta.RecursorInfo := do
-match ← getRecFromUsingLoop baseRecName (← inferType major) with
-| some recInfo => pure recInfo
-| none =>
-  let recName ← resolveGlobalConstNoOverload baseRecName
-  try
-    liftMetaMAtMain fun _ => Meta.mkRecursorInfo recName
-  catch _ =>
-    throwError! "invalid recursor name '{baseRecName}'"
+  match ← getRecFromUsingLoop baseRecName (← inferType major) with
+  | some recInfo => pure recInfo
+  | none =>
+    let recName ← resolveGlobalConstNoOverload baseRecName
+    try
+      liftMetaMAtMain fun _ => Meta.mkRecursorInfo recName
+    catch _ =>
+      throwError! "invalid recursor name '{baseRecName}'"
 
 /- Create `RecInfo` assuming builtin recursor -/
 private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAlts : Bool) : TacticM (RecInfo × Array Name) := do
-let indVal ← getInductiveValFromMajor major
-let recName := mkRecName indVal.name
-if withAlts.isNone then
-  pure ({ recName := recName }, #[])
-else
-  let ctorNames := indVal.ctors
-  let alts      := getAlts withAlts
-  checkAltCtorNames alts ctorNames
-  let altVars := #[]
-  let altRHSs := #[]
-  let remainingAlts := alts
-  let prevAnonymousAlt? := none
-  for ctorName in ctorNames do
-    match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
-    | some idx =>
-      let newAlt := remainingAlts[idx]
-      altVars       := altVars.push (getAltVarNames newAlt).toList
-      altRHSs       := altRHSs.push (getAltRHS newAlt)
-      remainingAlts := remainingAlts.eraseIdx idx
-    | none =>
-        match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
-        | some idx =>
-          let newAlt        := remainingAlts[idx]
-          altVars           := altVars.push (getAltVarNames newAlt).toList
-          altRHSs           := altRHSs.push (getAltRHS newAlt)
-          remainingAlts     := remainingAlts.eraseIdx idx
-          prevAnonymousAlt? := some newAlt
-        | none => match prevAnonymousAlt? with
-          | some alt =>
-            altVars := altVars.push (getAltVarNames alt).toList
-            altRHSs := altRHSs.push (getAltRHS alt)
-          | none     =>
-            if allowMissingAlts then
-              altVars := altVars.push []
-              altRHSs := altRHSs.push Syntax.missing
-            else
-              throwError! "alternative for constructor '{ctorName}' is missing"
-  unless remainingAlts.isEmpty do
-    throwErrorAt remainingAlts[0] "unused alternative"
-  pure ({ recName := recName, altVars := altVars, altRHSs := altRHSs }, ctorNames.toArray)
+  let indVal ← getInductiveValFromMajor major
+  let recName := mkRecName indVal.name
+  if withAlts.isNone then
+    pure ({ recName := recName }, #[])
+  else
+    let ctorNames := indVal.ctors
+    let alts      := getAlts withAlts
+    checkAltCtorNames alts ctorNames
+    let altVars := #[]
+    let altRHSs := #[]
+    let remainingAlts := alts
+    let prevAnonymousAlt? := none
+    for ctorName in ctorNames do
+      match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
+      | some idx =>
+        let newAlt := remainingAlts[idx]
+        altVars       := altVars.push (getAltVarNames newAlt).toList
+        altRHSs       := altRHSs.push (getAltRHS newAlt)
+        remainingAlts := remainingAlts.eraseIdx idx
+      | none =>
+          match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
+          | some idx =>
+            let newAlt        := remainingAlts[idx]
+            altVars           := altVars.push (getAltVarNames newAlt).toList
+            altRHSs           := altRHSs.push (getAltRHS newAlt)
+            remainingAlts     := remainingAlts.eraseIdx idx
+            prevAnonymousAlt? := some newAlt
+          | none => match prevAnonymousAlt? with
+            | some alt =>
+              altVars := altVars.push (getAltVarNames alt).toList
+              altRHSs := altRHSs.push (getAltRHS alt)
+            | none     =>
+              if allowMissingAlts then
+                altVars := altVars.push []
+                altRHSs := altRHSs.push Syntax.missing
+              else
+                throwError! "alternative for constructor '{ctorName}' is missing"
+    unless remainingAlts.isEmpty do
+      throwErrorAt remainingAlts[0] "unused alternative"
+    pure ({ recName := recName, altVars := altVars, altRHSs := altRHSs }, ctorNames.toArray)
 
 /-
   Recall that
@@ -196,86 +195,84 @@ else
   withAlts : Parser := optional (" with " >> inductionAlts)
   usingRec : Parser := optional (" using " >> ident)
   ``` -/
-private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo :=
-withRef stx do
-let usingRecStx := stx[2]
-let withAlts    := stx[4]
-if usingRecStx.isNone then
-  let (rinfo, _) ← getRecInfoDefault major withAlts false
-  pure rinfo
-else
-  let baseRecName := usingRecStx.getIdAt 1 $.eraseMacroScopes
-  let recInfo ← getRecFromUsing major baseRecName
-  let recName := recInfo.recursorName
-  if withAlts.isNone then
-    pure { recName := recName }
+private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRef stx do
+  let usingRecStx := stx[2]
+  let withAlts    := stx[4]
+  if usingRecStx.isNone then
+    let (rinfo, _) ← getRecInfoDefault major withAlts false
+    pure rinfo
   else
-    let alts := getAlts withAlts
-    let paramNames ← liftMetaMAtMain fun _ => getParamNames recInfo.recursorName
-    let altVars           := #[]
-    let altRHSs           := #[]
-    let remainingAlts     := alts
-    let prevAnonymousAlt? := none
-    for i in [:paramNames.size] do
-      if recInfo.isMinor i then
-        let paramName := paramNames[i]
-        match remainingAlts.findIdx? (fun alt => getAltName alt == paramName) with
-        | some idx =>
-          let newAlt := remainingAlts[idx]
-          altVars := altVars.push (getAltVarNames newAlt).toList
-          altRHSs := altRHSs.push (getAltRHS newAlt)
-          remainingAlts := remainingAlts.eraseIdx idx
-        | none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
+    let baseRecName := usingRecStx.getIdAt 1 $.eraseMacroScopes
+    let recInfo ← getRecFromUsing major baseRecName
+    let recName := recInfo.recursorName
+    if withAlts.isNone then
+      pure { recName := recName }
+    else
+      let alts := getAlts withAlts
+      let paramNames ← liftMetaMAtMain fun _ => getParamNames recInfo.recursorName
+      let altVars           := #[]
+      let altRHSs           := #[]
+      let remainingAlts     := alts
+      let prevAnonymousAlt? := none
+      for i in [:paramNames.size] do
+        if recInfo.isMinor i then
+          let paramName := paramNames[i]
+          match remainingAlts.findIdx? (fun alt => getAltName alt == paramName) with
           | some idx =>
-            let newAlt     := remainingAlts[idx]
+            let newAlt := remainingAlts[idx]
             altVars := altVars.push (getAltVarNames newAlt).toList
             altRHSs := altRHSs.push (getAltRHS newAlt)
             remainingAlts := remainingAlts.eraseIdx idx
-            prevAnonymousAlt? := some newAlt
-          | none => match prevAnonymousAlt? with
-            | some alt =>
-              altVars := altVars.push (getAltVarNames alt).toList
-              altRHSs := altRHSs.push (getAltRHS alt)
-            | none     =>
-              throwError! "alternative for minor premise '{paramName}' is missing"
-    unless remainingAlts.isEmpty do
-      throwErrorAt remainingAlts[0] "unused alternative"
-    pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
+          | none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
+            | some idx =>
+              let newAlt     := remainingAlts[idx]
+              altVars := altVars.push (getAltVarNames newAlt).toList
+              altRHSs := altRHSs.push (getAltRHS newAlt)
+              remainingAlts := remainingAlts.eraseIdx idx
+              prevAnonymousAlt? := some newAlt
+            | none => match prevAnonymousAlt? with
+              | some alt =>
+                altVars := altVars.push (getAltVarNames alt).toList
+                altRHSs := altRHSs.push (getAltRHS alt)
+              | none     =>
+                throwError! "alternative for minor premise '{paramName}' is missing"
+      unless remainingAlts.isEmpty do
+        throwErrorAt remainingAlts[0] "unused alternative"
+      pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
 
 -- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
 def isHoleRHS (rhs : Syntax) : Bool :=
-rhs.isOfKind `Lean.Parser.Term.syntheticHole || rhs.isOfKind `Lean.Parser.Term.hole
+  rhs.isOfKind `Lean.Parser.Term.syntheticHole || rhs.isOfKind `Lean.Parser.Term.hole
 
 private def processResult (altRHSs : Array Syntax) (result : Array Meta.InductionSubgoal) : TacticM Unit := do
-if altRHSs.isEmpty then
-  setGoals $ result.toList.map fun s => s.mvarId
-else
-  unless altRHSs.size == result.size do
-    throwError! "mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
-  let gs := []
-  for i in [:result.size] do
-    let subgoal := result[i]
-    let rhs     := altRHSs[i]
-    let ref     := rhs
-    let mvarId  := subgoal.mvarId
-    if isHoleRHS rhs then
-      let gs' ← withMVarContext mvarId $ withRef rhs do
-        let mvarDecl ← getMVarDecl mvarId
-        let val ← elabTermEnsuringType rhs mvarDecl.type
-        assignExprMVar mvarId val
-        let gs' ← getMVarsNoDelayed val
-        let gs' := gs'.toList
-        tagUntaggedGoals mvarDecl.userName `induction gs'
-        pure gs'
-      gs := gs ++ gs'
-    else
-      setGoals [mvarId]
-      evalTactic rhs
-      done
-  setGoals gs
+  if altRHSs.isEmpty then
+    setGoals $ result.toList.map fun s => s.mvarId
+  else
+    unless altRHSs.size == result.size do
+      throwError! "mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
+    let gs := []
+    for i in [:result.size] do
+      let subgoal := result[i]
+      let rhs     := altRHSs[i]
+      let ref     := rhs
+      let mvarId  := subgoal.mvarId
+      if isHoleRHS rhs then
+        let gs' ← withMVarContext mvarId $ withRef rhs do
+          let mvarDecl ← getMVarDecl mvarId
+          let val ← elabTermEnsuringType rhs mvarDecl.type
+          assignExprMVar mvarId val
+          let gs' ← getMVarsNoDelayed val
+          let gs' := gs'.toList
+          tagUntaggedGoals mvarDecl.userName `induction gs'
+          pure gs'
+        gs := gs ++ gs'
+      else
+        setGoals [mvarId]
+        evalTactic rhs
+        done
+    setGoals gs
 
-@[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic :=
-fun stx => focusAux do
+@[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focusAux do
   let h? := getAuxHypothesisName stx
   let major ← elabMajor h? (getMajor stx)
   let major ← generalizeMajor major
@@ -286,31 +283,30 @@ fun stx => focusAux do
   processResult recInfo.altRHSs result
 
 private partial def checkCasesResult (casesResult : Array Meta.CasesSubgoal) (ctorNames : Array Name) (altRHSs : Array Syntax) : TacticM Unit := do
-let rec loop (i j : Nat) : TacticM Unit :=
-  if h : j < altRHSs.size then do
-    let altRHS   := altRHSs.get ⟨j, h⟩
-    if altRHS.isMissing then
-      loop i (j+1)
-    else
-      let ctorName := ctorNames.get! j
-      if h : i < casesResult.size then
-        let subgoal := casesResult.get ⟨i, h⟩
-        if ctorName == subgoal.ctorName then
-          loop (i+1) (j+1)
-        else
-          throwError! "alternative for '{subgoal.ctorName}' has not been provided"
+  let rec loop (i j : Nat) : TacticM Unit :=
+    if h : j < altRHSs.size then do
+      let altRHS   := altRHSs.get ⟨j, h⟩
+      if altRHS.isMissing then
+        loop i (j+1)
       else
-        throwError! "alternative for '{ctorName}' is not needed"
-  else if h : i < casesResult.size then
-    let subgoal := casesResult.get ⟨i, h⟩
-    throwError! "alternative for '{subgoal.ctorName}' has not been provided"
-  else
-    pure ()
-unless altRHSs.isEmpty do
-  loop 0 0
+        let ctorName := ctorNames.get! j
+        if h : i < casesResult.size then
+          let subgoal := casesResult.get ⟨i, h⟩
+          if ctorName == subgoal.ctorName then
+            loop (i+1) (j+1)
+          else
+            throwError! "alternative for '{subgoal.ctorName}' has not been provided"
+        else
+          throwError! "alternative for '{ctorName}' is not needed"
+    else if h : i < casesResult.size then
+      let subgoal := casesResult.get ⟨i, h⟩
+      throwError! "alternative for '{subgoal.ctorName}' has not been provided"
+    else
+      pure ()
+  unless altRHSs.isEmpty do
+    loop 0 0
 
-@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic :=
-fun stx => focusAux do
+@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focusAux do
   -- parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
   let h? := getAuxHypothesisName stx
   let major ← elabMajor h? (getMajor stx)
diff --git a/src/Lean/Elab/Tactic/Injection.lean b/src/Lean/Elab/Tactic/Injection.lean
index 8ba60dad80..c98d70d79c 100644
--- a/src/Lean/Elab/Tactic/Injection.lean
+++ b/src/Lean/Elab/Tactic/Injection.lean
@@ -9,15 +9,16 @@ namespace Lean.Elab.Tactic
 
 -- optional (" with " >> many1 ident')
 private def getInjectionNewIds (stx : Syntax) : List Name :=
-if stx.isNone then []
-else stx[1].getArgs.toList.map Syntax.getId
+  if stx.isNone then
+    []
+  else
+    stx[1].getArgs.toList.map Syntax.getId
 
 private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit := do
-unless unusedIds.isEmpty do
-  Meta.throwTacticEx `injection mvarId msg!"too many identifiers provided, unused: {unusedIds}"
+  unless unusedIds.isEmpty do
+    Meta.throwTacticEx `injection mvarId msg!"too many identifiers provided, unused: {unusedIds}"
 
-@[builtinTactic «injection»] def evalInjection : Tactic :=
-fun stx => do
+@[builtinTactic «injection»] def evalInjection : Tactic := fun stx => do
   -- parser! nonReservedSymbol "injection " >> termParser >> withIds
   let fvarId ← elabAsFVar stx[1]
   let ids := getInjectionNewIds stx[2]
diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index 1d0038901b..edd16a775e 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/src/Lean/Elab/Tactic/Location.lean
@@ -6,9 +6,9 @@ Authors: Leonardo de Moura
 namespace Lean.Elab.Tactic
 
 inductive Location
-| wildcard
-| target
-| localDecls (userNames : Array Name)
+  | wildcard
+  | target
+  | localDecls (userNames : Array Name)
 
 /-
 Recall that
@@ -20,13 +20,15 @@ def location         := parser! "at " >> (locationWildcard <|> locationTarget <|
 ```
 -/
 def expandLocation (stx : Syntax) : Location :=
-let arg := stx[1]
-if arg.getKind == `Lean.Parser.Tactic.locationWildcard then Location.wildcard
-else if arg.getKind == `Lean.Parser.Tactic.locationTarget then Location.target
-else Location.localDecls $ arg[0].getArgs.map fun stx => stx.getId
+  let arg := stx[1]
+  if arg.getKind == `Lean.Parser.Tactic.locationWildcard then Location.wildcard
+  else if arg.getKind == `Lean.Parser.Tactic.locationTarget then Location.target
+  else Location.localDecls $ arg[0].getArgs.map fun stx => stx.getId
 
 def expandOptLocation (stx : Syntax) : Location :=
-if stx.isNone then Location.target
-else expandLocation stx[0]
+  if stx.isNone then
+    Location.target
+  else
+    expandLocation stx[0]
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 66b75b0486..75010eb955 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -10,39 +10,38 @@ import Lean.Elab.Tactic.Induction
 namespace Lean.Elab.Tactic
 
 structure AuxMatchTermState :=
-(nextIdx : Nat := 1)
-(cases   : Array Syntax := #[])
+  (nextIdx : Nat := 1)
+  (cases   : Array Syntax := #[])
 
 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
-let matchAlts := matchTac[4]
-let alts      := matchAlts[1].getArgs
-let newAlts ← alts.mapSepElemsM fun alt => do
-  let alt    := alt.updateKind `Lean.Parser.Term.matchAlt
-  let holeOrTacticSeq := alt[2]
-  if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
-    pure alt
-  else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
-    let s ← get
-    let holeName := mkIdentFrom holeOrTacticSeq (parentTag ++ (`match).appendIndexAfter s.nextIdx)
-    let newHole ← `(?$holeName:ident)
-    modify fun s => { s with nextIdx := s.nextIdx + 1}
-    pure $ alt.setArg 2 newHole
-  else withFreshMacroScope do
-    let newHole ← `(?rhs)
-    let newHoleId := newHole[1]
-    let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
-    modify fun s => { s with cases := s.cases.push newCase }
-    pure $ alt.setArg 2 newHole
-let result  := matchTac.updateKind `Lean.Parser.Term.«match»
-let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts))
-pure result
+  let matchAlts := matchTac[4]
+  let alts      := matchAlts[1].getArgs
+  let newAlts ← alts.mapSepElemsM fun alt => do
+    let alt    := alt.updateKind `Lean.Parser.Term.matchAlt
+    let holeOrTacticSeq := alt[2]
+    if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
+      pure alt
+    else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
+      let s ← get
+      let holeName := mkIdentFrom holeOrTacticSeq (parentTag ++ (`match).appendIndexAfter s.nextIdx)
+      let newHole ← `(?$holeName:ident)
+      modify fun s => { s with nextIdx := s.nextIdx + 1}
+      pure $ alt.setArg 2 newHole
+    else withFreshMacroScope do
+      let newHole ← `(?rhs)
+      let newHoleId := newHole[1]
+      let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
+      modify fun s => { s with cases := s.cases.push newCase }
+      pure $ alt.setArg 2 newHole
+  let result  := matchTac.updateKind `Lean.Parser.Term.«match»
+  let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts))
+  pure result
 
 private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do
-let (matchTerm, s) ← mkAuxiliaryMatchTermAux parentTag matchTac $.run {}
-pure (matchTerm, s.cases)
+  let (matchTerm, s) ← mkAuxiliaryMatchTermAux parentTag matchTac $.run {}
+  pure (matchTerm, s.cases)
 
-@[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic :=
-fun stx => do
+@[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic := fun stx => do
   let tag ← getMainTag
   let (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm tag stx
   let refineMatchTerm ← `(tactic| refine $matchTerm)