Commit 2023-05-03 01:24 ffbbb250
View on Github →chore: tweak subsingleton_of_trichotomous_of_irrefl
(#3749)
Match https://github.com/leanprover-community/mathlib/pull/18749
chore: tweak subsingleton_of_trichotomous_of_irrefl
(#3749)
Match https://github.com/leanprover-community/mathlib/pull/18749