From 91513604691bc08b462bdec9080efdc897b3e37c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 7 May 2026 14:09:36 +0200
Subject: [PATCH] fix: preserve symbol hover for `fun_induction` function
 target (#13678)

This PR ensures that one can hover over the function name in
fun_induction. Fixes #13673

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/Lean/Elab/Tactic/Induction.lean              | 2 +-
 tests/server_interactive/hover.lean              | 9 +++++++++
 tests/server_interactive/hover.lean.out.expected | 9 +++++++++
 3 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index cf59515d01..64af33bfbc 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -1024,7 +1024,7 @@ Elaborates the `foo args` of `fun_induction` or `fun_cases`, inferring the args
 def elabFunTargetCall (cases : Bool) (stx : Syntax) : TacticM Expr := do
   match stx with
   | `($id:ident) =>
-    let fnName ← realizeGlobalConstNoOverload id
+    let fnName ← realizeGlobalConstNoOverloadWithInfo id
     let unfolding := tactic.fun_induction.unfolding.get (← getOptions)
     let some funIndInfo ← getFunIndInfo? (cases := cases) (unfolding := unfolding) fnName |
       let theoremKind := if cases then "cases" else "induction"
diff --git a/tests/server_interactive/hover.lean b/tests/server_interactive/hover.lean
index 86e38a7440..06d1136758 100644
--- a/tests/server_interactive/hover.lean
+++ b/tests/server_interactive/hover.lean
@@ -346,3 +346,12 @@ coinductive InfSeq (r : α → α → Prop) : α → Prop where
 
 #check InfSeq.step
      --^ textDocument/hover
+
+def map' (f : α → β) : List α → List β
+  | []    => []
+  | a::as => f a :: map' f as
+
+example (xs : List α) : map' id xs = xs := by
+  fun_induction map'
+              --^ textDocument/hover
+  <;> simp_all only [id]
diff --git a/tests/server_interactive/hover.lean.out.expected b/tests/server_interactive/hover.lean.out.expected
index c53cb754c7..99c378e801 100644
--- a/tests/server_interactive/hover.lean.out.expected
+++ b/tests/server_interactive/hover.lean.out.expected
@@ -756,3 +756,12 @@
  {"value":
   "```lean\nInfSeq.step.{u_1} {α : Sort u_1} (r : α → α → Prop) {a b : α} : r a b → InfSeq r b → InfSeq r a\n```\n***\nTake a step ",
   "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 354, "character": 16}}
+{"range":
+ {"start": {"line": 354, "character": 16},
+  "end": {"line": 354, "character": 20}},
+ "contents":
+ {"value":
+  "```lean\nmap'.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) : List α → List β\n```",
+  "kind": "markdown"}}