exists simplifying ors

Stream: Is there code for X?

[Yakov Pechersky]

Do we have these?

@[simp] lemma exists_or_eq_left {α : Sort*} (y : α) (p : α → Prop) : ∃ (x : α), x = y ∨ p x :=
⟨y, or.inl rfl⟩

@[simp] lemma exists_or_eq_right {α : Sort*} (y : α) (p : α → Prop) : ∃ (x : α), p x ∨ x = y :=
⟨y, or.inr rfl⟩

[Eric Wieser]

I assume we have docs#exist_eq?

[Eric Wieser]

But I guess not under that name...