より厳しい `guard_hyp` タクティク

Zulip: Really strict guard_hyp

import Lean

elab "guard_hyp_strict" hyp:ident " : " val:term : tactic => withMainContext do
    let fvarid ← getFVarId hyp
    let lDecl ←
      match (← getLCtx).find? fvarid with
      | none => throwError m!"hypothesis {hyp} not found"
      | some lDecl => pure lDecl
    let e ← elabTerm val none
    let hty ← instantiateMVars lDecl.type
    unless e.equal hty do
      throwError m!"hypothesis {hyp} has type{indentExpr hty}\nnot{indentExpr e}"

example (h : ∃ k : Nat, k = k) : True := by
  guard_hyp_strict h : ∃ l : Nat, l = l -- I hoped this would have failed
  trivial

Start with the linked Zulip discussion and the guard_hyp_strict elaborator shown in the issue. Confirm the intended repository change and locate the relevant Lean example or tactic entry point, since no file or test is named. Done should establish the stricter type comparison behavior illustrated by the existential example and include a way to verify it.