fix: cases tactic to handle non-atomic eliminator well (#8361)

This PR fixes a bug in the `cases` tacic introduced in #3188 that arises
when cases (not induction) is used with a non-atomic expression in using
and the argument indexing gets confused.

This fixes #8360.

src/Lean/Elab/Tactic/Induction.lean

@@ -128,10 +128,11 @@ private def getFType : M Expr := do
   pure fType
 
 structure Result where
-  elimApp : Expr
-  motive  : MVarId
-  alts    : Array Alt
-  others  : Array MVarId
+  elimApp     : Expr
+  elimArgs    : Array Expr
+  motive      : MVarId
+  alts        : Array Alt
+  others      : Array MVarId
   complexArgs : Array Expr
 
 /--
@@ -209,7 +210,10 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
       unless targets.contains motiveArg do
         throwError "mkElimApp: Expected first {targets.size} arguments of motive in conclusion to be one of the targets:{indentExpr s.fType}"
     pure motiveArgs[targets.size:]
-  return { elimApp := (← instantiateMVars s.f), alts, others, motive, complexArgs }
+  let elimApp ← instantiateMVars s.f
+  -- `elimArgs` is the argument list that the offsets in `elimInfo` work with
+  let elimArgs := elimApp.getAppArgs[elimInfo.elimExpr.getAppNumArgs:]
+  return { elimApp, elimArgs, alts, others, motive, complexArgs }
 
 /--
 Given a goal `... targets ... |- C[targets, complexArgs]` associated with `mvarId`,
@@ -981,7 +985,7 @@ def evalCasesCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Array Expr)
   let tag ← mvarId.getTag
   mvarId.withContext do
     let result ← withRef targetRef <| ElimApp.mkElimApp elimInfo targets tag
-    let elimArgs := result.elimApp.getAppArgs
+    let elimArgs := result.elimArgs
     let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]!
     let motiveType ← inferType elimArgs[elimInfo.motivePos]!
     let mvarId ← generalizeTargetsEq mvarId motiveType targets

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -62,7 +62,7 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
     let motiveType ← inferType motive
     forallTelescopeReducing motiveType fun motiveParams motiveResultType => do
       unless motiveParams.size == motiveArgs.size do
-        throwError "expecetd {motiveArgs.size} parameters at motive type, got {motiveParams.size}:{indentExpr motiveType}"
+        throwError "expected {motiveArgs.size} parameters at motive type, got {motiveParams.size}:{indentExpr motiveType}"
       unless motiveResultType.isSort do
         throwError "motive result type must be a sort{indentExpr motiveType}"
     let some motivePos ← pure (xs.idxOf? motive) |

tests/lean/run/issue8360.lean

@@ -0,0 +1,7 @@
+axiom thm.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β)
+  (motive : List α → List β → Prop) (case1 : motive [] [])
+  (case2 : ∀ (a : α) (as : List α), motive (a :: as) (f a :: List.map f as)) (l : List α) : motive l (List.map f l)
+
+theorem map_isNil (f : α → β) (l : List α) :
+  List.map f l = [] ↔ l = [] := by
+  cases l using thm f <;> simp