RFC: use `Std.Refl`/`Std.Symm` instances in `rfl`/`symm`

Proposal

When using the tactic rfl and no @[refl] lemmas apply, try to use exact Std.Refl.refl _ to solve the goal.
(at the end of Lean.MVarId.applyRfl)

Similarly, when using the tactic symm and no @[symm] lemmas apply, try to use refine Std.Symm.symm _ _ ?_.
(at the end of Lean.MVarId.applySymm, and maybe also for Lean.Expr.applySymm and Lean.MVarId.symmSaturate)

If those tactics fail, the error message should mention that in addition to using the @[refl]/@[symm] attributes, registering an Std.Refl/Std.Symm instance also works.

I'm not sure whether it's faster to go through the list of registered lemmas before or after trying to synthesize an instance, but in most cases probably trying to synthesize an instance after the tactics failed to find registered lemmas wouldn't make performance worse, since they were about to fail anyway.
There's also the possibility of deprecating the @[refl]/@[symm] tags in favor of Std.Refl/Std.Symm instances.

Code example:

def Int.SameParity (a b : Int) : Prop := 2 ∣ (a - b)

instance : Std.Refl Int.SameParity where
  refl _ := by simp [Int.SameParity]

instance : Std.Symm Int.SameParity where
  symm _ _ h := by simpa [Int.SameParity, Int.neg_sub] using Int.dvd_neg.mpr h

/--
error: Tactic `rfl` failed: No `[refl]` lemma registered for relation
  Int.SameParity

Hint: Add the `[refl]` attribute to reflexivity lemmas for `Int.SameParity` to use this tactic

⊢ Int.SameParity 5 5
-/
#guard_msgs in
example : Int.SameParity 5 5 := by
  rfl

/--
error: No applicable symmetry lemma found for
  Int.SameParity 3 7

Note: Additional symmetry lemmas can be registered using the `[symm]` attribute
-/
#guard_msgs in
example : Int.SameParity 3 7 := by
  symm
  simp [Int.SameParity]

Note that attribute [refl] Std.Refl.refl makes the first example work (although I don't know how performant it is, and it ruins rfls error message), but attribute [symm] Std.Symm.symm does not work -- it causes a declaration has metavariables error.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Read Lean/Meta/Tactic/Rfl.lean at Lean.MVarId.applyRfl and Lean/Meta/Tactic/Symm.lean at Lean.MVarId.applySymm; also inspect Lean.Expr.applySymm and Lean.MVarId.symmSaturate. Compare the proposed Std.Refl and Std.Symm fallback behavior with existing attribute lookup and guarded error messages, then validate the examples and failure hints shown in the issue.