fix: remove derive_functional_induction (#3788)

this follows up on #3776 and the subsequent stage0 update, now relying
on the reserved name for the induction principles.

src/Init/Data/Array/Basic.lean

@@ -730,10 +730,8 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
     a.pop
 termination_by a.size - i.val
 
-derive_functional_induction feraseIdx
-
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
-  induction a, i using feraseIdx.induct with
+  induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ _ ih =>
     unfold feraseIdx
     simp [h, a', ih]

src/Lean/Meta/Tactic/FunInd.lean

@@ -28,7 +28,6 @@ def ackermann : Nat → Nat → Nat
   | 0, m => m + 1
   | n+1, 0 => ackermann n 1
   | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-derive_functional_induction ackermann
 ```
 we get
 ```
@@ -942,13 +941,6 @@ def deriveInduction (name : Name) : MetaM Unit := do
   else
     _ ← deriveUnaryInduction name
 
-@[builtin_command_elab Parser.Command.deriveInduction]
-def elabDeriveInduction : Command.CommandElab := fun stx => Command.runTermElabM fun _xs => do
-  let ident := stx[1]
-  let name ← realizeGlobalConstNoOverloadWithInfo ident
-  deriveInduction name
-
-
 def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
   unless s = "induct" do return false

src/Lean/Parser/Command.lean

@@ -281,17 +281,6 @@ def initializeKeyword := leading_parser
 @[builtin_command_parser] def addDocString := leading_parser
   docComment >> "add_decl_doc " >> ident
 
-/--
-`derive_functional_induction foo`, where `foo` is the name of a function defined using well-founded recursion,
-will define a theorem `foo.induct` which provides an induction principle that follows the branching
-and recursion pattern of `foo`.
-
-If `foo` is part of a mutual recursion group, this defines such `.induct`-theorems for all functions
-in the group.
--/
-@[builtin_command_parser] def deriveInduction := leading_parser
-  "derive_functional_induction " >> Parser.ident
-
 /--
   This is an auxiliary command for generation constructor injectivity theorems for
   inductive types defined at `Prelude.lean`.