mathlib3

54d8b94e - chore(logic/basic): add simp lemmas about exist_unique to match those about exists (#7784)

chore(logic/basic): add simp lemmas about exist_unique to match those about exists (#7784) Adds: * `exists_unique_const` to match `exists_const` (provable by simp) * `exists_unique_prop` to match `exists_prop` (provable by simp) * `exists_unique_prop_of_true` to match `exists_prop_of_true`