mathlib

aa47bba5 - feat(data/equiv): equiv_of_subsingleton_of_subsingleton (#2856)