chore: remove begin ... end syntax

We should use `by { ... }` from now on.

cc @Kha

src/Lean/Elab/App.lean

@@ -236,12 +236,10 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
             match evalSyntaxConstant env tacticDecl with
             | Except.error err       => throwError err
             | Except.ok tacticSyntax => do
-              tacticBlock ← `(begin $(tacticSyntax.getArgs)* end);
-              -- tacticBlock does not have any position information
-              -- use ctx.ref.getHeadInfo if available
-              let tacticBlock := match ctx.ref.getHeadInfo with
-                | some info => tacticBlock.replaceInfo info
-                | _         => tacticBlock;
+              tacticBlock ← `(by { $(tacticSyntax.getArgs)* });
+              -- tacticBlock does not have any position information.
+              -- So, we use ctx.ref
+              let tacticBlock := tacticBlock.copyInfo ctx.ref;
               let d := d.getArg! 0; -- `autoParam type := by tactic` ==> `type`
               argElab ← elabArg e (Arg.stx tacticBlock) d;
               elabAppArgsAux ctx (mkApp e argElab) (b.instantiate1 argElab)

src/Lean/Elab/Tactic/Basic.lean

@@ -372,12 +372,9 @@ fun stx => match_syntax stx with
 @[builtinTactic paren] def evalParen : Tactic :=
 fun stx => evalTactic (stx.getArg 1)
 
-@[builtinTactic nestedTacticBlock] def evalNestedTacticBlock : Tactic :=
+@[builtinTactic nestedTacticBlockCurly] def evalNestedTacticBlock : Tactic :=
 fun stx => focus (evalTactic (stx.getArg 1))
 
-@[builtinTactic nestedTacticBlockCurly] def evalNestedTacticBlockCurly : Tactic :=
-evalNestedTacticBlock
-
 @[builtinTactic «case»] def evalCase : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| case $tag $tac) => do

src/Lean/Elab/Term.lean

@@ -972,12 +972,6 @@ ref ← getRef;
 registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic tacticCode;
 pure mvar
 
-@[builtinTermElab tacticBlock] def elabTacticBlock : TermElab :=
-fun stx expectedType? =>
-  match expectedType? with
-  | some expectedType => mkTacticMVar expectedType (stx.getArg 1)
-  | none => throwError ("invalid tactic block, expected type has not been provided")
-
 @[builtinTermElab byTactic] def elabByTactic : TermElab :=
 fun stx expectedType? =>
   match expectedType? with

src/Lean/Parser/Tactic.lean

@@ -60,7 +60,6 @@ def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 ma
 @[builtinTacticParser] def «match»      := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
 @[builtinTacticParser] def «injection»  := parser! nonReservedSymbol "injection " >> termParser >> withIds
 @[builtinTacticParser] def paren        := parser! "(" >> nonEmptySeq >> ")"
-@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
 @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
 @[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
 

src/Lean/Parser/Term.lean

@@ -222,7 +222,6 @@ stx.isAntiquot || stx.isIdent
 @[builtinTermParser] def seqRight    := tparser! infixR " *> "  60
 @[builtinTermParser] def map         := tparser! infixR " <$> " 100
 
-@[builtinTermParser] def tacticBlock := parser! "begin " >> Tactic.seq >> "end"
 @[builtinTermParser] def byTactic    := parser!:leadPrec "by " >> Tactic.nonEmptySeq
 
 @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"

tests/lean/match3.lean

@@ -33,10 +33,10 @@ match a', h₁, h₂ with
 | _, rfl, h₂ => h₂
 
 theorem ex6  {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
-begin
+by {
   subst h₁;
   assumption
-end
+}
 
 theorem ex7 (a : Bool) (p q : Prop) (h₁ : a = true → p) (h₂ : a = false → q) : p ∨ q :=
 match h:a with

tests/lean/run/newfrontend1.lean

@@ -119,7 +119,7 @@ by {
 namespace Foo
   def Prod.mk := 1
   #check (⟨2, 3⟩ : Prod _ _)
-} Foo
+end Foo
 
 theorem simple10 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {