mathlib

a51ce549 - chore(data/set/semiring): add an `idem_semiring` instance (#18449)

chore(data/set/semiring): add an `idem_semiring` instance (#18449) This typeclass is reasonably new, so some obvious instances are missing. Also adds some basic API lemmas that were missing about the casting functions `set.up` and `set_semiring.down`. forward-ported as https://github.com/leanprover-community/mathlib4/pull/2518