Documentation

Mathlib.Tactic.Relation.Rfl

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].