mathlib

f24dc98b - feat(logic/unique): forall_iff and exists_iff (#1249)

feat(logic/unique): forall_iff and exists_iff (#1249) Maybe these should be `@[simp]`. My use case in `fin 1` and it's slightly annoying to have `default (fin 1)` everwhere instead of `0`, but maybe that should also be a `@[simp]` lemma.