mathlib

c06f500f - feat(logic/basic): add eq_iff_true_of_subsingleton (#3308)

feat(logic/basic): add eq_iff_true_of_subsingleton (#3308) I'm surprised we didn't have this already. ```lean example (x y : unit) : x = y := by simp ``` Co-authored-by: Johan Commelin <johan@commelin.net>