merge

src/Init/Data/List/Lemmas.lean

@@ -350,6 +350,26 @@ theorem forall_mem_cons {p : α → Prop} {a : α} {l : List α} :
 theorem forall_mem_ne {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a = a') ↔ a ∉ l :=
   ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
 
+@[simp]
+theorem forall_mem_ne' {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l :=
+  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
+
+@[simp]
+theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
+  induction l <;> simp_all
+
+@[simp]
+theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
+  induction l <;> simp_all [eq_comm (a := a)]
+
+@[simp]
+theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
+  induction l <;> simp_all
+
+@[simp]
+theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
+  induction l <;> simp_all [eq_comm (a := a)]
+
 theorem exists_mem_nil (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ @nil α, p x) := nofun
 
 theorem forall_mem_nil (p : α → Prop) : ∀ (x) (_ : x ∈ @nil α), p x := nofun
@@ -932,10 +952,10 @@ theorem forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} :
 
 /-! ### filter -/
 
-@[simp] theorem filter_cons_of_pos {p : α → Bool} {a : α} (l) (pa : p a) :
+@[simp] theorem filter_cons_of_pos {p : α → Bool} {a : α} {l} (pa : p a) :
     filter p (a :: l) = a :: filter p l := by rw [filter, pa]
 
-@[simp] theorem filter_cons_of_neg {p : α → Bool} {a : α} (l) (pa : ¬ p a) :
+@[simp] theorem filter_cons_of_neg {p : α → Bool} {a : α} {l} (pa : ¬ p a) :
     filter p (a :: l) = filter p l := by rw [filter, eq_false_of_ne_true pa]
 
 theorem filter_cons :
@@ -1030,10 +1050,10 @@ theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p
 
 /-! ### filterMap -/
 
-@[simp] theorem filterMap_cons_none {f : α → Option β} (a : α) (l : List α) (h : f a = none) :
+@[simp] theorem filterMap_cons_none {f : α → Option β} {a : α} {l : List α} (h : f a = none) :
     filterMap f (a :: l) = filterMap f l := by simp only [filterMap, h]
 
-@[simp] theorem filterMap_cons_some (f : α → Option β) (a : α) (l : List α) {b : β} (h : f a = some b) :
+@[simp] theorem filterMap_cons_some {f : α → Option β} {a : α} {l : List α} {b : β} (h : f a = some b) :
     filterMap f (a :: l) = b :: filterMap f l := by simp only [filterMap, h]
 
 @[simp]
@@ -2005,10 +2025,26 @@ theorem takeWhile_cons (p : α → Bool) (a : α) (l : List α) :
   simp only [takeWhile]
   by_cases h: p a <;> simp [h]
 
+@[simp] theorem takeWhile_cons_of_pos {p : α → Bool} {a : α} {l : List α} (h : p a) :
+    (a :: l).takeWhile p = a :: l.takeWhile p := by
+  simp [takeWhile_cons, h]
+
+@[simp] theorem takeWhile_cons_of_neg {p : α → Bool} {a : α} {l : List α} (h : ¬ p a) :
+    (a :: l).takeWhile p = [] := by
+  simp [takeWhile_cons, h]
+
 theorem dropWhile_cons :
     (x :: xs : List α).dropWhile p = if p x then xs.dropWhile p else x :: xs := by
   split <;> simp_all [dropWhile]
 
+@[simp] theorem dropWhile_cons_of_pos {a : α} {l : List α} (h : p a) :
+    (a :: l).dropWhile p = l.dropWhile p := by
+  simp [dropWhile_cons, h]
+
+@[simp] theorem dropWhile_cons_of_neg {a : α} {l : List α} (h : ¬ p a) :
+    (a :: l).dropWhile p = a :: l := by
+  simp [dropWhile_cons, h]
+
 theorem head?_takeWhile (p : α → Bool) (l : List α) : (l.takeWhile p).head? = l.head?.filter p := by
   cases l with
   | nil => rfl
@@ -2058,6 +2094,24 @@ theorem dropWhile_map (f : α → β) (p : β → Bool) (l : List α) :
   | [] => rfl
   | x :: xs => by simp [takeWhile, dropWhile]; cases p x <;> simp [takeWhile_append_dropWhile p xs]
 
+theorem takeWhile_append {xs ys : List α} :
+    (xs ++ ys).takeWhile p =
+      if (xs.takeWhile p).length = xs.length then xs ++ ys.takeWhile p else xs.takeWhile p := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [cons_append, takeWhile_cons]
+    split
+    · simp_all only [length_cons, add_one_inj]
+      split <;> rfl
+    · simp_all
+
+@[simp] theorem takeWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) :
+    (l₁ ++ l₂).takeWhile p = l₁ ++ l₂.takeWhile p := by
+  induction l₁ with
+  | nil => simp
+  | cons x xs ih => simp_all [takeWhile_cons]
+
 theorem dropWhile_append {xs ys : List α} :
     (xs ++ ys).dropWhile p =
       if (xs.dropWhile p).isEmpty then ys.dropWhile p else xs.dropWhile p ++ ys := by
@@ -2067,6 +2121,12 @@ theorem dropWhile_append {xs ys : List α} :
     simp only [cons_append, dropWhile_cons]
     split <;> simp_all
 
+@[simp] theorem dropWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) :
+    (l₁ ++ l₂).dropWhile p = l₂.dropWhile p := by
+  induction l₁ with
+  | nil => simp
+  | cons x xs ih => simp_all [dropWhile_cons]
+
 @[simp] theorem takeWhile_replicate_eq_filter (p : α → Bool) :
     (replicate n a).takeWhile p = (replicate n a).filter p := by
   induction n with
@@ -2317,6 +2377,9 @@ theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l
 theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=
   s.eq_of_length <| Nat.le_antisymm s.length_le h
 
+theorem Sublist.length_eq (s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂ :=
+  ⟨s.eq_of_length, congrArg _⟩
+
 protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂ := by
   induction s with
   | slnil => simp
@@ -2824,10 +2887,10 @@ end insert
 theorem eraseP_cons (a : α) (l : List α) :
     (a :: l).eraseP p = bif p a then l else a :: l.eraseP p := rfl
 
-@[simp] theorem eraseP_cons_of_pos {l : List α} (p) (h : p a) : (a :: l).eraseP p = l := by
+@[simp] theorem eraseP_cons_of_pos {l : List α} {p} (h : p a) : (a :: l).eraseP p = l := by
   simp [eraseP_cons, h]
 
-@[simp] theorem eraseP_cons_of_neg {l : List α} (p) (h : ¬p a) :
+@[simp] theorem eraseP_cons_of_neg {l : List α} {p} (h : ¬p a) :
     (a :: l).eraseP p = a :: l.eraseP p := by simp [eraseP_cons, h]
 
 theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l := by
@@ -2858,22 +2921,18 @@ theorem exists_or_eq_self_of_eraseP (p) (l : List α) :
     .inl (eraseP_of_forall_not (h ⟨·, ·, ·⟩))
 
 @[simp] theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) :
-    length (l.eraseP p) = Nat.pred (length l) := by
+    length (l.eraseP p) = length l - 1 := by
   let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
   rw [e₂]; simp [length_append, e₁]; rfl
 
-theorem eraseP_append_left {a : α} (pa : p a) :
-    ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂
-  | x :: xs, l₂, h => by
-    by_cases h' : p x <;> simp [h']
-    rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]
-    intro | rfl => exact pa
-
-theorem eraseP_append_right :
-    ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
-  | [],      l₂, _ => rfl
-  | x :: xs, l₂, h => by
-    simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]
+theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length := by
+  split <;> rename_i h
+  · simp only [any_eq_true] at h
+    obtain ⟨x, m, h⟩ := h
+    simp [length_eraseP_of_mem m h]
+  · simp only [any_eq_true] at h
+    rw [eraseP_of_forall_not]
+    simp_all
 
 theorem eraseP_sublist (l : List α) : l.eraseP p <+ l := by
   match exists_or_eq_self_of_eraseP p l with
@@ -2904,10 +2963,126 @@ theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (erase
     have : a ≠ c := fun h => (h ▸ pa).elim h₂
     simp [this] at al; simp [al]
 
+@[simp] theorem eraseP_eq_self_iff {p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a := by
+  rw [← Sublist.length_eq (eraseP_sublist l), length_eraseP]
+  split <;> rename_i h
+  · simp only [any_eq_true, length_eq_zero] at h
+    constructor
+    · intro; simp_all [Nat.sub_one_eq_self]
+    · intro; obtain ⟨x, m, h⟩ := h; simp_all
+  · simp_all
+
 theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map f (l.eraseP (p ∘ f))
   | [] => rfl
   | b::l => by by_cases h : p (f b) <;> simp [h, eraseP_map f l, eraseP_cons_of_pos]
 
+theorem eraseP_filterMap (f : α → Option β) : ∀ (l : List α),
+    (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false))
+  | [] => rfl
+  | a::l => by
+    rw [filterMap_cons, eraseP_cons]
+    split <;> rename_i h
+    · simp [h, eraseP_filterMap]
+    · rename_i b
+      rw [h, eraseP_cons]
+      by_cases w : p b
+      · simp [w]
+      · simp only [w, cond_false]
+        rw [filterMap_cons_some h, eraseP_filterMap]
+
+theorem eraseP_filter (f : α → Bool) (l : List α) :
+    (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x)) := by
+  rw [← filterMap_eq_filter, eraseP_filterMap]
+  congr
+  ext x
+  simp only [Option.guard]
+  split <;> split at * <;> simp_all
+
+theorem eraseP_append_left {a : α} (pa : p a) :
+    ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂
+  | x :: xs, l₂, h => by
+    by_cases h' : p x <;> simp [h']
+    rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]
+    intro | rfl => exact pa
+
+theorem eraseP_append_right :
+    ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
+  | [],      l₂, _ => rfl
+  | x :: xs, l₂, h => by
+    simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]
+
+theorem eraseP_append (l₁ l₂ : List α) :
+    (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p := by
+  split <;> rename_i h
+  · simp only [any_eq_true] at h
+    obtain ⟨x, m, h⟩ := h
+    rw [eraseP_append_left h _ m]
+  · simp only [any_eq_true] at h
+    rw [eraseP_append_right _]
+    simp_all
+
+theorem eraseP_eq_iff {p} {l : List α} :
+    l.eraseP p = l' ↔
+      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
+        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by
+  cases exists_or_eq_self_of_eraseP p l with
+  | inl h =>
+    constructor
+    · intro h'
+      left
+      exact ⟨eraseP_eq_self_iff.1 h, by simp_all⟩
+    · rintro (⟨-, rfl⟩ | ⟨a, l₁, l₂, h₁, h₂, rfl, rfl⟩)
+      · assumption
+      · rw [eraseP_append_right _ h₁, eraseP_cons_of_pos h₂]
+  | inr h =>
+    obtain ⟨a, l₁, l₂, h₁, h₂, w₁, w₂⟩ := h
+    rw [w₂]
+    subst w₁
+    constructor
+    · rintro rfl
+      right
+      refine ⟨a, l₁, l₂, ?_⟩
+      simp_all
+    · rintro (h | h)
+      · simp_all
+      · obtain ⟨a', l₁', l₂', h₁', h₂', h, rfl⟩ := h
+        have p : l₁ = l₁' := by
+          have q : l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂) := by
+            rw [takeWhile_append_of_pos (by simp_all),
+              takeWhile_cons_of_neg (by simp [h₂]), append_nil]
+          have q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂') := by
+            rw [takeWhile_append_of_pos (by simpa using h₁'),
+              takeWhile_cons_of_neg (by simp [h₂']), append_nil]
+          simp [h] at q
+          rw [q', q]
+        subst p
+        simp_all
+
+@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
+    (replicate n a).eraseP p = replicate (n - 1) a := by
+  cases n <;> simp [replicate_succ, h]
+
+@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
+    (replicate n a).eraseP p = replicate n a := by
+  rw [eraseP_of_forall_not (by simp_all)]
+
+theorem Nodup.eraseP [BEq α] [LawfulBEq α] (p) : Nodup l → Nodup (l.eraseP p) :=
+  Nodup.sublist <| eraseP_sublist _
+
+theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
+    (l.eraseP p).eraseP q = (l.eraseP q).eraseP p := by
+  induction l with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [eraseP_cons]
+    by_cases h₁ : p a
+    · by_cases h₂ : q a
+      · simp_all
+      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
+    · by_cases h₂ : q a
+      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
+      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
+
 /-! ### erase -/
 section erase
 variable [BEq α]
@@ -2915,7 +3090,7 @@ variable [BEq α]
 @[simp] theorem erase_cons_head [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l := by
   simp [erase_cons]
 
-@[simp] theorem erase_cons_tail {a b : α} (l : List α) (h : ¬(b == a)) :
+@[simp] theorem erase_cons_tail {a b : α} {l : List α} (h : ¬(b == a)) :
     (b :: l).erase a = b :: l.erase a := by simp only [erase_cons, if_neg h]
 
 theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l
@@ -2945,14 +3120,13 @@ theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
     length (l.erase a) = length l - 1 := by
   rw [erase_eq_eraseP]; exact length_eraseP_of_mem h (beq_self_eq_true a)
 
-theorem erase_sublist (a : α) (l : List α) : l.erase a <+ l := by
-  induction l with
-  | nil => simp
-  | cons b l ih =>
-    simp only [erase_cons]
-    split
-    · exact sublist_cons b l
-    · exact cons_sublist_cons.mpr ih
+theorem length_erase [LawfulBEq α] (a : α) (l : List α) :
+    length (l.erase a) = if a ∈ l then length l - 1 else length l := by
+  rw [erase_eq_eraseP, length_eraseP]
+  split <;> split <;> simp_all
+
+theorem erase_sublist (a : α) (l : List α) : l.erase a <+ l :=
+  erase_eq_eraseP' a l ▸ eraseP_sublist ..
 
 theorem erase_subset (a : α) (l : List α) : l.erase a ⊆ l := (erase_sublist a l).subset
 
@@ -2965,6 +3139,28 @@ theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈
     a ∈ l.erase b ↔ a ∈ l :=
   erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
 
+@[simp] theorem erase_eq_self_iff [LawfulBEq α] {l : List α} : l.erase a = l ↔ a ∉ l := by
+  rw [erase_eq_eraseP', eraseP_eq_self_iff]
+  simp
+
+theorem erase_filter [LawfulBEq α] (f : α → Bool) (l : List α) :
+    (filter f l).erase a = filter f (l.erase a) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    by_cases h : a = x
+    · rw [erase_cons]
+      simp only [h, beq_self_eq_true, ↓reduceIte]
+      rw [filter_cons]
+      split
+      · rw [erase_cons_head]
+      · rw [erase_of_not_mem]
+        simp_all [mem_filter]
+    · rw [erase_cons_tail (by simpa using Ne.symm h), filter_cons, filter_cons]
+      split
+      · rw [erase_cons_tail (by simpa using Ne.symm h), ih]
+      · rw [ih]
+
 theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁) :
     (l₁ ++ l₂).erase a = l₁.erase a ++ l₂ := by
   simp [erase_eq_eraseP]; exact eraseP_append_left (beq_self_eq_true a) l₂ h
@@ -2974,6 +3170,10 @@ theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List
   rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right]
   intros b h' h''; rw [eq_of_beq h''] at h; exact h h'
 
+theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
+    (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a := by
+  simp [erase_eq_eraseP, eraseP_append]
+
 theorem erase_comm [LawfulBEq α] (a b : α) (l : List α) :
     (l.erase a).erase b = (l.erase b).erase a := by
   if ab : a == b then rw [eq_of_beq ab] else ?_
@@ -2988,7 +3188,21 @@ theorem erase_comm [LawfulBEq α] (a b : α) (l : List α) :
           erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head]
     else
       rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha',
-          erase_cons_tail _ ab, erase_cons_head]
+          erase_cons_tail ab, erase_cons_head]
+
+theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
+    l.erase a = l' ↔
+      (a ∉ l ∧ l = l') ∨
+        ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by
+  rw [erase_eq_eraseP', eraseP_eq_iff]
+  simp only [beq_iff_eq, forall_mem_ne', exists_and_left]
+  constructor
+  · rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, x, rfl, rfl⟩)
+    · left; simp_all
+    · right; refine ⟨l', h, x, by simp⟩
+  · rintro (⟨h, rfl⟩ | ⟨l₁, h, x, rfl, rfl⟩)
+    · left; simp_all
+    · right; refine ⟨a, l₁, h, by simp⟩
 
 @[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} :
     (replicate n a).erase a = replicate (n - 1) a := by
@@ -3006,7 +3220,7 @@ theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α)
     rename_i b l
     by_cases h : b = a
     · subst h
-      rw [erase_cons_head, filter_cons_of_neg _ (by simp)]
+      rw [erase_cons_head, filter_cons_of_neg (by simp)]
       apply Eq.symm
       rw [filter_eq_self]
       simpa [@eq_comm α] using m

src/Init/Data/Nat/Basic.lean

@@ -634,6 +634,10 @@ theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, s
 
 theorem add_one_inj : a + 1 = b + 1 ↔ a = b := succ_inj'
 
+theorem ne_add_one (n : Nat) : n ≠ n + 1 := fun h => by cases h
+
+theorem add_one_ne (n : Nat) : n + 1 ≠ n := fun h => by cases h
+
 theorem add_one_le_add_one_iff : a + 1 ≤ b + 1 ↔ a ≤ b := succ_le_succ_iff
 
 theorem add_one_lt_add_one_iff : a + 1 < b + 1 ↔ a < b := succ_lt_succ_iff
@@ -815,6 +819,9 @@ protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
 @[simp] protected theorem zero_sub_one : 0 - 1 = 0 := rfl
 @[simp] protected theorem add_one_sub_one (n : Nat) : n + 1 - 1 = n := rfl
 
+theorem sub_one_eq_self (n : Nat) : n - 1 = n ↔ n = 0 := by cases n <;> simp [ne_add_one]
+theorem eq_self_sub_one (n : Nat) : n = n - 1 ↔ n = 0 := by cases n <;> simp [add_one_ne]
+
 theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
   induction a with
   | zero => contradiction

src/Init/PropLemmas.lean

@@ -295,6 +295,8 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
 
 @[simp] theorem exists_eq_left' : (∃ a, a' = a ∧ p a) ↔ p a' := by simp [@eq_comm _ a']
 
+@[simp] theorem exists_eq_right' : (∃ a, p a ∧ a' = a) ↔ p a' := by simp [@eq_comm _ a']
+
 @[simp] theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a := by
   simp only [or_imp, forall_and, forall_eq]