本当に構文的に等しい `a = a` という等式しか証明しない `rfl` の派生タクティク

Zulip: strict refl

import Lean

open Lean Elab Tactic

elab "real_rfl" : tactic => do
  let some (_a, lhs, rhs) := (← getMainTarget).eq? | throwError "Not an equality goal"
  if lhs == rhs then
    evalTactic (← `(tactic| rfl))
  else
    logWarning "Not a 'real' equality"

/-- error: Not an equality goal -/
#guard_msgs in
  example : True := by
    real_rfl

/--
warning: Not a 'real' equality
-/
#guard_msgs in
  example : 2 = 1 + 1 := by
    real_rfl
    rfl

example : 2 = 2 := by
  real_rfl

Start from the Lean elaborator snippet in the issue, especially getMainTarget, eq?, and evalTactic. Check how tactics and example checks are organized in the repository, then add the derived tactic so the shown #guard_msgs cases warn or fail as specified while the syntactically identical equality succeeds.