mathlib3
60bb0711 - feat(logic/unit): Make `punit.star` simp normal form of `default : punit` (#13741)
