自動で変数に名前をつける `case` タクティクの派生形

Zulip: > Using rename_i with try

import Lean

open Lean Elab Tactic Meta in
elab "cases_on" : tactic => do
  let g0 ← popMainGoal
  g0.withContext do
    let (x, g) ← g0.intro1
    g.withContext do
      let dom ← x.getType
      matchConstInduct dom.getAppFn
        (fun _ => throwError "Expecting type to be an inductive type, not{indentExpr dom}")
        (fun ival _ => do
          let c ← mkConstWithFreshMVarLevels (mkCasesOnName ival.name)
          -- use the g0 context so that `x` doesn't appear in any premises
          let (args, _) ← g0.withContext do forallMetaTelescope (← inferType c)
          let params := dom.getAppArgs
          for i in [0:params.size] do
            unless ← isDefEq args[i]! params[i]! do
              throwError "(internal error) failed to assign inductive type parameter"
          let mut args := args
          -- Set major premise (replace the metavariable)
          args := args.set! (ival.numParams + 1) (.fvar x)
          -- Set remaining arguments as synthetic opaque so they can be tactic goals
          let minors := args[ival.numParams + 2 : args.size].toArray.toList.map (·.mvarId!)
          for m in minors do
            m.setKind .syntheticOpaque
          -- Construct recursor application, motive still needs solving-for
          let casesOn := mkAppN c args
          let gs ← g.apply casesOn
          pushGoals gs)

example : (xs : List Nat) → 0 ≤ xs.length := by
  cases_on
  /-
  case nil
  ⊢ 0 ≤ [].length

  case cons
  ⊢ ∀ (head : Nat) (tail : List Nat), 0 ≤ (head :: tail).length
  -/

Start from the elab "cases_on" tactic implementation shown in the issue and compare it with the cases_on example for List Nat. Determine the intended automatic naming behavior and define what the generated case goals should look like; the issue does not identify a repository file or test to update.