mathlib

39d23b8e - feat(logic/basic): exists_or_eq_{left,right} (#7224)