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

src/data/list/sigma.lean

@@ -224,7 +224,7 @@ theorem lookup_all_eq_nil {a : α} : ∀ {l : list (sigma β)},
 | []             := by simp
 | (⟨a', b⟩ :: l) := begin
   by_cases h : a = a',
-  { subst a', simp, exact ⟨_, or.inl rfl⟩ },
+  { subst a', simp },
   { simp [h, lookup_all_eq_nil] },
 end
 

src/logic/basic.lean

@@ -884,6 +884,18 @@ by simp only [or_imp_distrib, forall_and_distrib, forall_eq]
   (∃ b, (∃ a, f a = b) ∧ p b) ↔ ∃ a, p (f a) :=
 ⟨λ ⟨b, ⟨a, ha⟩, hb⟩, ⟨a, ha.symm ▸ hb⟩, λ ⟨a, ha⟩, ⟨f a, ⟨a, rfl⟩, ha⟩⟩
 
+@[simp] lemma exists_or_eq_left (y : α) (p : α → Prop) : ∃ (x : α), x = y ∨ p x :=
+⟨y, or.inl rfl⟩
+
+@[simp] lemma exists_or_eq_right (y : α) (p : α → Prop) : ∃ (x : α), p x ∨ x = y :=
+⟨y, or.inr rfl⟩
+
+@[simp] lemma exists_or_eq_left' (y : α) (p : α → Prop) : ∃ (x : α), y = x ∨ p x :=
+⟨y, or.inl rfl⟩
+
+@[simp] lemma exists_or_eq_right' (y : α) (p : α → Prop) : ∃ (x : α), p x ∨ y = x :=
+⟨y, or.inr rfl⟩
+
 @[simp] theorem forall_apply_eq_imp_iff {f : α → β} {p : β → Prop} :
   (∀ a, ∀ b, f a = b → p b) ↔ (∀ a, p (f a)) :=
 ⟨λ h a, h a (f a) rfl, λ h a b hab, hab ▸ h a⟩