feat(logic/basic): exists_eq simp lemmas without and.comm (#5694)

src/control/traversable/instances.lean

@@ -111,7 +111,7 @@ lemma mem_traverse {f : α' → set β'} :
 | []      (b::bs) := by simp
 | (a::as) (b::bs) :=
   suffices (b :: bs : list β') ∈ traverse f (a :: as) ↔ b ∈ f a ∧ bs ∈ traverse f as,
-    by simpa [mem_traverse as bs],
+    by simp [mem_traverse as bs],
   iff.intro
     (assume ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩, ⟨hb, hl⟩)
     (assume ⟨hb, hl⟩, ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩)

src/data/buffer/parser/basic.lean

@@ -42,12 +42,6 @@ section lemmas
 
 variables {α : Type*} {P Q : α → Prop} {Q' : Prop} {x : α}
 
-@[simp] lemma exists_eq_right_right : (∃ (y : α), P y ∧ Q' ∧ y = x) ↔ P x ∧ Q' :=
-⟨λ ⟨_, hp, hq, rfl⟩, ⟨hp, hq⟩, λ ⟨hp, hq⟩, ⟨x, hp, hq, rfl⟩⟩
-
-@[simp] lemma exists_eq_right_right' : (∃ (y : α), P y ∧ Q' ∧ x = y) ↔ P x ∧ Q' :=
-⟨λ ⟨_, hp, hq, rfl⟩, ⟨hp, hq⟩, λ ⟨hp, hq⟩, ⟨x, hp, hq, rfl⟩⟩
-
 @[simp] lemma ne_iff_lt_iff_le {n m : ℕ} : (n ≠ m ↔ n < m) ↔ n ≤ m :=
 begin
   refine ⟨λ h, _, λ h, _⟩,

src/data/list/perm.lean

@@ -860,7 +860,7 @@ begin
   { simp at h, simp [h] },
   { rw [sublists'_cons, reverse_append, zip_append, ← map_reverse,
         zip_map_right, zip_map_left] at h; [simp at h, simp],
-    rcases h with ⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩,
+    rcases h with ⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩,
     { exact perm_middle.trans ((IH _ _ h).cons _) },
     { exact (IH _ _ h).cons _ } }
 end

src/logic/basic.lean

@@ -797,6 +797,14 @@ by simp only [or_imp_distrib, forall_and_distrib, forall_eq]
 @[simp] theorem exists_eq_right {a' : α} : (∃ a, p a ∧ a = a') ↔ p a' :=
 (exists_congr $ by exact λ a, and.comm).trans exists_eq_left
 
+@[simp] theorem exists_eq_right_right {a' : α} :
+  (∃ (a : α), p a ∧ b ∧ a = a') ↔ p a' ∧ b :=
+⟨λ ⟨_, hp, hq, rfl⟩, ⟨hp, hq⟩, λ ⟨hp, hq⟩, ⟨a', hp, hq, rfl⟩⟩
+
+@[simp] theorem exists_eq_right_right' {a' : α} :
+  (∃ (a : α), p a ∧ b ∧ a' = a) ↔ p a' ∧ b :=
+⟨λ ⟨_, hp, hq, rfl⟩, ⟨hp, hq⟩, λ ⟨hp, hq⟩, ⟨a', hp, hq, rfl⟩⟩
+
 @[simp] theorem exists_apply_eq_apply {α β : Type*} (f : α → β) (a' : α) : ∃ a, f a = f a' :=
 ⟨a', rfl⟩