rfl tactic extension for reflexive relations

This extends the rfl tactic so that it works on any reflexive relation, provided the reflexivity lemma has been marked as @[refl].

ink

opaque Mathlib.Tactic.reflExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array (Lean.Meta.DiscrTree.Key true)) (Lean.Meta.DiscrTree Lean.Name true)

Environment extensions for refl lemmas