chore: upstream List.eraseIdx lemmas (leanprover#4865)

src/Init/ByCases.lean

@@ -67,12 +67,8 @@ theorem ite_some_none_eq_none [Decidable P] :
 -- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
 theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
     (if h : P then some (x h) else none) = none ↔ ¬P := by
-  simp only [dite_eq_right_iff]
-  rfl
+  simp
 
 @[simp] theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
     (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
-  by_cases h : P <;> simp only [h, dite_cond_eq_true, dite_cond_eq_false, Option.some.injEq,
-    false_iff, not_exists]
-  case pos => exact ⟨fun h_eq ↦ Exists.intro h h_eq, fun h_exists => h_exists.2⟩
-  case neg => exact fun h_false _ ↦ h_false
+  by_cases h : P <;> simp [h]

src/Init/Data/List/Erase.lean

@@ -1,7 +1,8 @@
 /-
 Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
+  Yury Kudryashov
 -/
 prelude
 import Init.Data.List.Pairwise
@@ -387,4 +388,58 @@ theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i)
     simp [eraseIdx, ← Nat.add_one]
     rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
 
+@[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl
+
+theorem eraseIdx_eq_take_drop_succ :
+    ∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1)
+  | nil, _ => by simp
+  | a::l, 0 => by simp
+  | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]
+
+theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
+  | [], _ => by simp
+  | a::l, 0 => by simp
+  | a::l, k + 1 => by simp [eraseIdx_sublist l k]
+
+theorem eraseIdx_subset (l : List α) (k : Nat) : eraseIdx l k ⊆ l := (eraseIdx_sublist l k).subset
+
+@[simp]
+theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ length l ≤ k
+  | [], _ => by simp
+  | a::l, 0 => by simp [(cons_ne_self _ _).symm]
+  | a::l, k + 1 => by simp [eraseIdx_eq_self]
+
+theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l := by
+  rw [eraseIdx_eq_self.2 h]
+
+theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
+    eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
+  induction l generalizing k with
+  | nil => simp_all
+  | cons x l ih =>
+    cases k with
+    | zero => rfl
+    | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_lt_succ_iff]
+
+theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤ k) (l' : List α) :
+    eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l) := by
+  induction l generalizing k with
+  | nil => simp_all
+  | cons x l ih =>
+    cases k with
+    | zero => simp_all
+    | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_sub_succ]
+
+protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
+    eraseIdx l k <+: eraseIdx l' k := by
+  rcases h with ⟨t, rfl⟩
+  if hkl : k < length l then
+    simp [eraseIdx_append_of_lt_length hkl]
+  else
+    rw [Nat.not_lt] at hkl
+    simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl]
+
+-- See also `mem_eraseIdx_iff_getElem` and `mem_eraseIdx_iff_getElem?` in
+-- `Init/Data/List/Nat/Basic.lean`.
+
 end List

src/Init/Data/List/Nat/Basic.lean

@@ -34,6 +34,28 @@ theorem leftpad_length (n : Nat) (a : α) (l : List α) :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
+/-! ### eraseIdx -/
+
+theorem mem_eraseIdx_iff_getElem {x : α} :
+    ∀ {l} {k}, x ∈ eraseIdx l k ↔ ∃ i h, i ≠ k ∧ l[i]'h = x
+  | [], _ => by
+    simp only [eraseIdx, not_mem_nil, false_iff]
+    rintro ⟨i, h, -⟩
+    exact Nat.not_lt_zero _ h
+  | a::l, 0 => by simp [mem_iff_getElem, Nat.succ_lt_succ_iff]
+  | a::l, k+1 => by
+    rw [← Nat.or_exists_add_one]
+    simp [mem_eraseIdx_iff_getElem, @eq_comm _ a, succ_inj', Nat.succ_lt_succ_iff]
+
+theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x := by
+  simp only [mem_eraseIdx_iff_getElem, getElem_eq_iff, exists_and_left]
+  refine exists_congr fun i => and_congr_right' ?_
+  constructor
+  · rintro ⟨_, h⟩; exact h
+  · rintro h;
+    obtain ⟨h', -⟩ := getElem?_eq_some.1 h
+    exact ⟨h', h⟩
+
 /-! ### minimum? -/
 
 -- A specialization of `minimum?_eq_some_iff` to Nat.

src/Init/Data/Nat/Basic.lean

@@ -102,6 +102,13 @@ def blt (a b : Nat) : Bool :=
 attribute [simp] Nat.zero_le
 attribute [simp] Nat.not_lt_zero
 
+theorem and_forall_add_one {p : Nat → Prop} : p 0 ∧ (∀ n, p (n + 1)) ↔ ∀ n, p n :=
+  ⟨fun h n => Nat.casesOn n h.1 h.2, fun h => ⟨h _, fun _ => h _⟩⟩
+
+theorem or_exists_add_one : p 0 ∨ (Exists fun n => p (n + 1)) ↔ Exists p :=
+  ⟨fun h => h.elim (fun h0 => ⟨0, h0⟩) fun ⟨n, hn⟩ => ⟨n + 1, hn⟩,
+    fun ⟨n, h⟩ => match n with | 0 => Or.inl h | n+1 => Or.inr ⟨n, h⟩⟩
+
 /-! # Helper "packing" theorems -/
 
 @[simp] theorem zero_eq : Nat.zero = 0 := rfl

src/Init/Data/Nat/Lemmas.lean

@@ -20,7 +20,12 @@ and later these lemmas should be organised into other files more systematically.
 
 namespace Nat
 
-attribute [simp] not_lt_zero
+@[deprecated and_forall_add_one (since := "2024-07-30")] abbrev and_forall_succ := @and_forall_add_one
+@[deprecated or_exists_add_one (since := "2024-07-30")] abbrev or_exists_succ := @or_exists_add_one
+
+@[simp] theorem exists_ne_zero {P : Nat → Prop} : (∃ n, ¬ n = 0 ∧ P n) ↔ ∃ n, P (n + 1) :=
+  ⟨fun ⟨n, h, w⟩ => by cases n with | zero => simp at h | succ n => exact ⟨n, w⟩,
+    fun ⟨n, w⟩ => ⟨n + 1, by simp, w⟩⟩
 
 /-! ## add -/
 

src/Init/PropLemmas.lean

@@ -202,6 +202,17 @@ theorem exists_imp : ((∃ x, p x) → b) ↔ ∀ x, p x → b := forall_exists_
 @[simp] theorem exists_const (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b :=
   ⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩
 
+@[congr]
+theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
+    Exists q ↔ ∃ h : p', q' (hp.2 h) :=
+  ⟨fun ⟨_, _⟩ ↦ ⟨hp.1 ‹_›, (hq _).1 ‹_›⟩, fun ⟨_, _⟩ ↦ ⟨_, (hq _).2 ‹_›⟩⟩
+
+theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (Exists fun h' : p => q h') ↔ q h :=
+  @exists_const (q h) p ⟨h⟩
+
+@[simp] theorem exists_true_left (p : True → Prop) : Exists p ↔ p True.intro :=
+  exists_prop_of_true _
+
 section forall_congr
 
 theorem forall_congr' (h : ∀ a, p a ↔ q a) : (∀ a, p a) ↔ ∀ a, q a :=

tests/lean/run/simp_cache_perf_issue.lean

@@ -1,7 +1,3 @@
-@[congr]
-theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
-    Exists q ↔ ∃ h : p', q' (hp.2 h) := sorry
-
 set_option maxHeartbeats 1000 in
 example (x : Nat) :
   ∃ (h : x = x)