feat: fix some issues with `equals t => tac`

[plp127]

This PR fixed some issues with the conv tactic equals t => tac:

• It gives bad error messages when t has the wrong type. For example,

  type mismatch
    this
  has type
    ?m.6391 = 1 : Prop
  but is expected to have type
    3 = ?m.6381 : Prop
  

• The use of show (_ = $t) means that if t has exposed function dots, something like

  equals · => tacs
  

  will turn into

  tactic => show (_ = ·); next => tacs
  

  and (_ = ·) will elaborate as fun x => _ = x, which is probably unexpected.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1291 has successfully built against this PR. (2025-06-27 13:44:22) View Log

[fgdorais]

This needs tests.