feat: List.mem_ite_nil_left and analogues (#5289)

src/Init/Data/Array/Lemmas.lean

@@ -267,6 +267,22 @@ theorem getElem_of_mem {a : α} {as : Array α} :
   exists i
   exists hbound
 
+@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
+    (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
+  split <;> simp_all [mem_def]
+
+@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Array α} :
+    (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h := by
+  split <;> simp_all [mem_def]
+
+@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
+    (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l := by
+  split <;> simp_all [mem_def]
+
+@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
+    (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
+  split <;> simp_all [mem_def]
+
 /-- # get lemmas -/
 
 theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :

src/Init/Data/List/Lemmas.lean

@@ -398,6 +398,22 @@ theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
 theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
   cases l <;> simp [-not_or]
 
+@[simp] theorem mem_dite_nil_left {x : α} [Decidable p] {l : ¬ p → List α} :
+    (x ∈ if h : p then [] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_dite_nil_right {x : α} [Decidable p] {l : p → List α} :
+    (x ∈ if h : p then l h else []) ↔ ∃ h : p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_nil_left {x : α} [Decidable p] {l : List α} :
+    (x ∈ if p then [] else l) ↔ ¬ p ∧ x ∈ l := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_nil_right {x : α} [Decidable p] {l : List α} :
+    (x ∈ if p then l else []) ↔ p ∧ x ∈ l := by
+  split <;> simp_all
+
 theorem eq_of_mem_singleton : a ∈ [b] → a = b
   | .head .. => rfl
 

src/Init/Data/Option/Lemmas.lean

@@ -389,6 +389,22 @@ end beq
 /-! ### ite -/
 section ite
 
+@[simp] theorem mem_dite_none_left {x : α} [Decidable p] {l : ¬ p → Option α} :
+    (x ∈ if h : p then none else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_dite_none_right {x : α} [Decidable p] {l : p → Option α} :
+    (x ∈ if h : p then l h else none) ↔ ∃ h : p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_none_left {x : α} [Decidable p] {l : Option α} :
+    (x ∈ if p then none else l) ↔ ¬ p ∧ x ∈ l := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
+    (x ∈ if p then l else none) ↔ p ∧ x ∈ l := by
+  split <;> simp_all
+
 @[simp] theorem isSome_dite {p : Prop} [Decidable p] {b : p → β} :
     (if h : p then some (b h) else none).isSome = true ↔ p := by
   split <;> simpa