diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 48bb2e6835..be9126065d 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -358,13 +358,7 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
   | _ => throwError "unexpected parentheses notation"
 
 @[builtinTermElab subst] def elabSubst : TermElab := fun stx expectedType? => do
-  tryPostponeIfNoneOrMVar expectedType?
-  let some expectedType ← pure expectedType? |
-    throwError! "invalid `▸` notation, expected type must be known"
-  let expectedType ← instantiateMVars expectedType
-  if expectedType.hasExprMVar then
-    tryPostpone
-    throwError! "invalid `▸` notation, expected type contains metavariables{indentExpr expectedType}"
+  let expectedType ← tryPostponeIfHasMVars expectedType? "invalid `▸` notation"
   match_syntax stx with
   | `($heq ▸ $h) => do
      let heq ← elabTerm heq none
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 8abf55ad5c..73f4753951 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -29,7 +29,7 @@ private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
   | none   => withMainMVarContext $ elabTerm major none
   | some h => withMainMVarContext do
     let lctx ← getLCtx
-    let x := lctx.getUnusedName `x
+    let x ← mkFreshUserName `x
     let major ← elabTerm major none
     evalGeneralizeAux h? major x
     withMainMVarContext do
@@ -74,7 +74,7 @@ private def generalizeVars (stx : Syntax) (major : Expr) : TacticM Nat := do
     pure (fvarIds.size, [mvarId'])
 
 private def getAlts (withAlts : Syntax) : Array Syntax :=
-  withAlts[2].getSepArgs
+  withAlts[1].getSepArgs
 
 /-
   Given an `inductionAlt` of the form
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index f62afca835..bccc0a0b89 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -815,6 +815,16 @@ def tryPostponeIfNoneOrMVar (e? : Option Expr) : TermElabM Unit :=
   | some e => tryPostponeIfMVar e
   | none   => tryPostpone
 
+def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermElabM Expr := do
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType ← pure expectedType? |
+    throwError! "{msg}, expected type must be known"
+  let expectedType ← instantiateMVars expectedType
+  if expectedType.hasExprMVar then
+    tryPostpone
+    throwError! "{msg}, expected type contains metavariables{indentExpr expectedType}"
+  pure expectedType
+
 private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
   trace[Elab.postpone]! "{stx} : {expectedType?}"
   let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 48c896d9b9..63d5fe2c28 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -62,7 +62,7 @@ def majorPremise := parser! optional («try» (ident >> " : ")) >> termParser
 def altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq
 def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS
 def inductionAlts : Parser := withPosition $ "| " >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|")
-def withAlts : Parser := optional (" with " >> inductionAlts)
+def withAlts : Parser := optional inductionAlts
 def usingRec : Parser := optional (" using " >> ident)
 def generalizingVars := optional (" generalizing " >> many1 ident)
 @[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
diff --git a/tests/lean/hygienicIntro.lean b/tests/lean/hygienicIntro.lean
index 7acfda4124..48c2337501 100644
--- a/tests/lean/hygienicIntro.lean
+++ b/tests/lean/hygienicIntro.lean
@@ -32,7 +32,7 @@ exact h
 
 -- Hygienic versions
 example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
-cases h₂ with
+cases h₂
 | inl h => apply h₁; exact h
 | inr h => exact h
 
diff --git a/tests/lean/run/concatElim.lean b/tests/lean/run/concatElim.lean
index 57512de9df..5953a952dd 100644
--- a/tests/lean/run/concatElim.lean
+++ b/tests/lean/run/concatElim.lean
@@ -49,7 +49,7 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
     rfl
   | x₁::x₂::xs =>
     intro n h
-    cases n with
+    cases n
     | zero   =>
       rw [lengthCons, lengthCons] at h
       injection h with h
diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index 71e86fbebe..3179c4b3bb 100644
--- a/tests/lean/run/induction1.lean
+++ b/tests/lean/run/induction1.lean
@@ -1,5 +1,3 @@
-
-
 @[recursor 4]
 def Or.elim2 {p q r : Prop} (major : p ∨ q) (left : p → r) (right : q → r) : r :=
 Or.elim major left right
@@ -21,30 +19,30 @@ focus
   assumption
 
 theorem tst1 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h with
+induction h
 | inr h2 => exact Or.inl h2
 | inl h1 => exact Or.inr h1
 
 
 theorem tst2 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
+induction h using elim2
 | left _  => apply Or.inr; assumption
 | right _ => apply Or.inl; assumption
 
 theorem tst3 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
+induction h using elim2
 | right h => exact Or.inl h
 | left h  => exact Or.inr h
 
 theorem tst4 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
+induction h using elim2
 | right h => ?myright
 | left h  => ?myleft
 case myleft  => exact Or.inr h
 case myright => exact Or.inl h
 
 theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
+induction h using elim2
 | right h => _
 | left h  =>
   refine Or.inr ?_
@@ -53,42 +51,41 @@ case right => exact Or.inl h
 
 theorem tst6 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
-  cases h with
+  cases h
   | inr h2 => exact Or.inl h2
   | inl h1 => exact Or.inr h1
 }
 
 theorem tst7 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
 by {
-  induction xs with
+  induction xs
   | nil          => exact rfl
   | cons z zs ih => exact absurd rfl (h z zs)
 }
 
-theorem tst8 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
-by {
+theorem tst8 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] := by {
   induction xs;
   exact rfl;
   exact absurd rfl $ h _ _
 }
 
-theorem tst9 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
-by cases xs with
-   | nil       => exact rfl
-   | cons z zs => exact absurd rfl (h z zs)
+theorem tst9 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] := by
+  cases xs
+     | nil       => exact rfl
+     | cons z zs => exact absurd rfl (h z zs)
 
-theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q :=
-by induction h₁ using Iff.elim with
-   | _ h _ => exact h h₂
+theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q := by
+  induction h₁ using Iff.elim
+  | _ h _ => exact h h₂
 
 def Iff2 (m p q : Prop) := p ↔ q
 
-theorem tst11 {p q r : Prop } (h₁ : Iff2 r p q) (h₂ : p) : q :=
-by induction h₁ using Iff.elim with
-   | _ h _ => exact h h₂
+theorem tst11 {p q r : Prop } (h₁ : Iff2 r p q) (h₂ : p) : q := by
+  induction h₁ using Iff.elim
+  | _ h _ => exact h h₂
 
 theorem tst12 {p q : Prop } (h₁ : p ∨ q) (h₂ : p ↔ q) (h₃ : p) : q := by
-failIfSuccess induction h₁ using Iff.elim
-induction h₂ using Iff.elim with
-| _ h _ =>
-  exact h h₃
+  failIfSuccess induction h₁ using Iff.elim
+  induction h₂ using Iff.elim
+  | _ h _ =>
+    exact h h₃
diff --git a/tests/lean/run/inj2.lean b/tests/lean/run/inj2.lean
index a195a0b2f0..c20d5c1f64 100644
--- a/tests/lean/run/inj2.lean
+++ b/tests/lean/run/inj2.lean
@@ -1,5 +1,3 @@
-
-
 universes u v
 
 inductive Vec2 (α : Type u) (β : Type v) : Nat → Type (max u v)
@@ -31,10 +29,10 @@ by {
 theorem test4 {α} (v : Fin2 0) : α :=
 by cases v
 
-def test5 {α β} {n} (v : Vec2 α β (n+1)) : α :=
-by cases v with
-   | cons h1 h2 n tail => exact h1
+def test5 {α β} {n} (v : Vec2 α β (n+1)) : α := by
+  cases v
+  | cons h1 h2 n tail => exact h1
 
-def test6 {α β} {n} (v : Vec2 α β (n+2)) : α :=
-by cases v with
-   | cons h1 h2 n tail => exact h1
+def test6 {α β} {n} (v : Vec2 α β (n+2)) : α := by
+  cases v
+  | cons h1 h2 n tail => exact h1
diff --git a/tests/lean/run/tacticTests.lean b/tests/lean/run/tacticTests.lean
index be035acb77..f760b78bb1 100644
--- a/tests/lean/run/tacticTests.lean
+++ b/tests/lean/run/tacticTests.lean
@@ -9,14 +9,14 @@ theorem ex1 (m : Nat) : Le m 0 → m = 0 := by
 
 theorem ex2 (m n : Nat) : Le m n → Le m.succ n.succ := by
   intro h
-  induction h with
+  induction h
   | base n => apply Le.base
   | succ n m ih =>
     apply Le.succ
     apply ih
 
 theorem ex3 (m : Nat) : Le 0 m := by
-  induction m with
+  induction m
   | zero => apply Le.base
   | succ m ih =>
     apply Le.succ
@@ -28,22 +28,22 @@ theorem ex4 (m : Nat) : ¬ Le m.succ 0 := by
 
 theorem ex5 {m n : Nat} : Le m n.succ → m = n.succ ∨ Le m n := by
   intro h
-  cases h with
+  cases h
   | base => apply Or.inl; rfl
   | succ => apply Or.inr; assumption
 
 theorem ex6 {m n : Nat} : Le m.succ n.succ → Le m n := by
   revert m
-  induction n with
+  induction n
   | zero =>
     intros m h;
-    cases h with
+    cases h
     | base => apply Le.base
     | succ n h => exact absurd h (ex4 _)
   | succ n ih =>
     intros m h
     have aux := ih (m := m)
-    cases ex5 h with
+    cases ex5 h
     | inl h =>
       injection h with h
       subst h
@@ -54,7 +54,7 @@ theorem ex6 {m n : Nat} : Le m.succ n.succ → Le m n := by
 
 theorem ex7 {m n o : Nat} : Le m n → Le n o → Le m o := by
   intro h
-  induction h with
+  induction h
   | base => intros; assumption
   | succ n s ih =>
     intro h₂
@@ -71,7 +71,7 @@ theorem ex8 {m n : Nat} : Le m.succ n → Le m n := by
 
 theorem ex9 {m n : Nat} : Le m n → m = n ∨ Le m.succ n := by
   intro h
-  cases h with
+  cases h
   | base => apply Or.inl; rfl
   | succ n s =>
     apply Or.inr
@@ -86,12 +86,12 @@ theorem ex10 (n : Nat) : ¬ Le n.succ n := by
 -/
 
 theorem ex10 (n : Nat) : n.succ ≠ n := by
-  induction n with
+  induction n
   | zero => intro h; injection h; done
   | succ n ih => intro h; injection h with h; apply ih h
 
 theorem ex11 (n : Nat) : ¬ Le n.succ n := by
-  induction n with
+  induction n
   | zero => intro h; cases h; done
   | succ n ih =>
     intro h
@@ -101,12 +101,12 @@ theorem ex11 (n : Nat) : ¬ Le n.succ n := by
 
 theorem ex12 (m n : Nat) : Le m n → Le n m → m = n := by
   revert m
-  induction n with
+  induction n
   | zero => intro m h1 h2; apply ex1; assumption; done
   | succ n ih =>
     intro m h1 h2
     have ih := ih m
-    cases ex5 h1 with
+    cases ex5 h1
     | inl h => assumption
     | inr h =>
       have ih := ih h