feat: HashSet.ofArray (unverified)

src/Init/Data/BitVec/Basic.lean

@@ -173,10 +173,6 @@ instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
 theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
   x[i] = x.toNat.testBit i := rfl
 
-theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
-    x.getLsbD i = x[i] := by
-  simp [getLsbD, getElem_eq_testBit_toNat]
-
 end getElem
 
 section Int

src/Init/Data/BitVec/Lemmas.lean

@@ -273,30 +273,8 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
-@[simp] theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
-  simp [getElem_eq_testBit_toNat]
-
-@[simp] theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
-  simp [getElem_eq_testBit_toNat, h]
-
-@[simp] theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by
-  simp [getElem?_eq_getElem]
-
-@[simp] theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
-  simp [getElem?_eq_getElem]
-
-@[simp] theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
-  simp [ofBool, cond_eq_if]
-  split <;> simp_all
-
-@[simp] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
-  rw [getElem_eq_iff, getElem?_zero_ofBool]
-
-@[simp] theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by
-  simp [ofBool]
-
 @[simp]
-theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && b) := by
+theorem getLsbD_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsbD i = ((i = 0) && b) := by
   rcases b with rfl | rfl
   · simp [ofBool]
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
@@ -352,10 +330,6 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 
 @[simp] theorem getMsbD_cast (h : w = v) (x : BitVec w) : (cast h x).getMsbD i = x.getMsbD i := by
   subst h; simp
-
-@[simp] theorem getElem_cast (h : w = v) (x : BitVec w) (p : i < v) : (cast h x)[i] = x[i] := by
-  subst h; simp
-
 @[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
   simp [BitVec.msb]
 
@@ -549,15 +523,6 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
   all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
 
-@[simp]
-theorem getElem_truncate (m : Nat) (x : BitVec n) (i : Nat) (hi : i < m) :
-    (truncate m x)[i] = x.getLsbD i := by
-  simp only [getElem_zeroExtend]
-
-theorem getElem?_truncate (m : Nat) (x : BitVec n) (i : Nat) :
-    (truncate m x)[i]? = if i < m then some (x.getLsbD i) else none :=
-  getElem?_zeroExtend m x i
-
 theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (truncate m x) i = (decide (i < m) && getLsbD x i) :=
   getLsbD_zeroExtend m x i
@@ -674,9 +639,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 @[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
   simp [allOnes]
 
-@[simp] theorem getElem_allOnes (i : Nat) (h : i < v) : (allOnes v)[i] = true := by
-  simp [getElem_eq_testBit_toNat, h]
-
 @[simp] theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n := by
   ext
   simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_True]
@@ -704,9 +666,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_or {x y : BitVec w} {i : Nat} (h : i < w) : (x ||| y)[i] = (x[i] || y[i]) := by
-  simp [getElem_eq_testBit_toNat]
-
 @[simp] theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb) := by
   simp [BitVec.msb]
 
@@ -745,9 +704,6 @@ instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_com
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_and {x y : BitVec w} {i : Nat} (h : i < w) : (x &&& y)[i] = (x[i] && y[i]) := by
-  simp [getElem_eq_testBit_toNat]
-
 @[simp] theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb) := by
   simp [BitVec.msb]
 
@@ -788,9 +744,6 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (xor x[i] y[i]) := by
-  simp [getElem_eq_testBit_toNat]
-
 @[simp] theorem msb_xor {x y : BitVec w} :
     (x ^^^ y).msb = (xor x.msb y.msb) := by
   simp [BitVec.msb]
@@ -844,12 +797,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 @[simp] theorem getLsbD_not {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && ! x.getLsbD i) := by
   by_cases h' : i < v <;> simp_all [not_def]
 
-@[simp] theorem getElem_not {x : BitVec w} {i : Nat} (h : i < w) : (~~~x)[i] = !x[i] := by
-  simp only [getElem_eq_testBit_toNat, toNat_not]
-  rw [← Nat.sub_add_eq, Nat.add_comm 1]
-  rw [Nat.testBit_two_pow_sub_succ x.isLt]
-  simp [h]
-
 @[simp] theorem truncate_not {x : BitVec w} (h : k ≤ w) :
     (~~~x).truncate k = ~~~(x.truncate k) := by
   ext
@@ -1006,10 +953,6 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
     getLsbD (x >>> i) j = getLsbD x (i+j) := by
   unfold getLsbD ; simp
 
-@[simp] theorem getElem_ushiftRight (x : BitVec w) (i n : Nat) (h : i < w) :
-    (x >>> n)[i] = x.getLsbD (n + i) := by
-  simp [getElem_eq_testBit_toNat, toNat_ushiftRight, Nat.testBit_shiftRight, getLsbD]
-
 theorem ushiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) >>> n = (x >>> n) ^^^ (y >>> n) := by
   ext

src/Init/Data/List/Attach.lean

@@ -130,6 +130,24 @@ theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a
     (l.attachWith p H).map Subtype.val = l :=
   (attachWith_map_coe _ _ _).trans (List.map_id _)
 
+theorem countP_attach (l : List α) (p : α → Bool) :
+    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
+  simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val]
+
+theorem countP_attachWith {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (q : α → Bool) :
+    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
+  simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val]
+
+@[simp]
+theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) :
+    l.attach.count a = l.count ↑a :=
+  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
+
+@[simp]
+theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
+    (l.attachWith p H).count a = l.count ↑a :=
+  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
+
 @[simp]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
   | ⟨a, h⟩ => by
@@ -294,20 +312,6 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
   | nil => simp at h
   | cons x xs => simp [head_attach, h]
 
-@[simp] theorem tail_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
-    (H : ∀ (a : α), a ∈ xs → P a) :
-    (xs.pmap f H).tail = xs.tail.pmap f (fun a h => H a (mem_of_mem_tail h)) := by
-  cases xs <;> simp
-
-@[simp] theorem tail_attachWith {P : α → Prop} {xs : List α}
-    {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).tail = xs.tail.attachWith P (fun a h => H a (mem_of_mem_tail h)) := by
-  cases xs <;> simp
-
-@[simp] theorem tail_attach (xs : List α) :
-    xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
-  cases xs <;> simp
-
 theorem attach_map {l : List α} (f : α → β) :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
   induction l <;> simp [*]
@@ -488,24 +492,4 @@ theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) :
     xs.attach.getLast h = ⟨xs.getLast (by simpa using h), getLast_mem (by simpa using h)⟩ := by
   simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach]
 
-@[simp]
-theorem countP_attach (l : List α) (p : α → Bool) :
-    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
-  simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val]
-
-@[simp]
-theorem countP_attachWith {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (q : α → Bool) :
-    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
-  simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val]
-
-@[simp]
-theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) :
-    l.attach.count a = l.count ↑a :=
-  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
-
-@[simp]
-theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
-    (l.attachWith p H).count a = l.count ↑a :=
-  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
-
 end List

src/Init/Data/List/Count.lean

@@ -115,13 +115,6 @@ theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂
 theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _
 theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _
 
--- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`.
-
-theorem countP_tail_le (l) : countP p l.tail ≤ countP p l :=
-  (tail_sublist l).countP_le _
-
--- See `Init.Data.List.Nat.Count` for `le_countP_tail : countP p l - 1 ≤ countP p l.tail`.
-
 theorem countP_filter (l : List α) :
     countP p (filter q l) = countP (fun a => p a && q a) l := by
   simp only [countP_eq_length_filter, filter_filter]
@@ -214,13 +207,6 @@ theorem IsPrefix.count_le (h : l₁ <+: l₂) (a : α) : count a l₁ ≤ count
 theorem IsSuffix.count_le (h : l₁ <:+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.sublist.count_le _
 theorem IsInfix.count_le (h : l₁ <:+: l₂) (a : α) : count a l₁ ≤ count a l₂ := h.sublist.count_le _
 
--- See `Init.Data.List.Nat.Count` for `Sublist.le_count : count a l₂ - (l₂.length - l₁.length) ≤ countP a l₁`.
-
-theorem count_tail_le (a : α) (l) : count a l.tail ≤ count a l :=
-  (tail_sublist l).count_le _
-
--- See `Init.Data.List.Nat.Count` for `le_count_tail : count a l - 1 ≤ count a l.tail`.
-
 theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) :=
   (sublist_cons_self _ _).count_le _
 

src/Init/Data/List/Lemmas.lean

@@ -1045,11 +1045,6 @@ theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]?
   | [] => rfl
   | a :: l => by simp
 
-theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos.mpr h) := by
-  cases l with
-  | nil => simp at h
-  | cons _ _ => simp
-
 theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h
@@ -1110,55 +1105,6 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t
 theorem mem_of_mem_tail {a : α} {l : List α} (h : a ∈ tail l) : a ∈ l := by
   induction l <;> simp_all
 
-theorem ne_nil_of_tail_ne_nil {l : List α} : l.tail ≠ [] → l ≠ [] := by
-  cases l <;> simp
-
-@[simp] theorem getElem_tail (l : List α) (i : Nat) (h : i < l.tail.length) :
-    (tail l)[i] = l[i + 1]'(add_lt_of_lt_sub (by simpa using h)) := by
-  cases l with
-  | nil => simp at h
-  | cons _ l => simp
-
-@[simp] theorem getElem?_tail (l : List α) (i : Nat) :
-    (tail l)[i]? = l[i + 1]? := by
-  cases l <;> simp
-
-@[simp] theorem set_tail (l : List α) (i : Nat) (a : α) :
-    l.tail.set i a = (l.set (i + 1) a).tail := by
-  cases l <;> simp
-
-theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.length := by
-  cases l with
-  | nil => simp at h
-  | cons _ l =>
-    simp only [tail_cons, ne_eq] at h
-    exact Nat.lt_add_of_pos_left (length_pos.mpr h)
-
-@[simp] theorem head_tail (l : List α) (h : l.tail ≠ []) :
-    (tail l).head h = l[1]'(one_lt_length_of_tail_ne_nil h) := by
-  cases l with
-  | nil => simp at h
-  | cons _ l => simp [head_eq_getElem]
-
-@[simp] theorem head?_tail (l : List α) : (tail l).head? = l[1]? := by
-  simp [head?_eq_getElem?]
-
-@[simp] theorem getLast_tail (l : List α) (h : l.tail ≠ []) :
-    (tail l).getLast h = l.getLast (ne_nil_of_tail_ne_nil h) := by
-  simp only [getLast_eq_getElem, length_tail, getElem_tail]
-  congr
-  match l with
-  | _ :: _ :: l => simp
-
-theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then none else l.getLast? := by
-  match l with
-  | [] => simp
-  | [a] => simp
-  | _ :: _ :: l =>
-    simp only [tail_cons, length_cons, getLast?_cons_cons]
-    rw [if_neg]
-    rintro ⟨⟩
-
 /-! ## Basic operations -/
 
 /-! ### map -/
@@ -2901,12 +2847,6 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (
     dropLast (a :: replicate n a) = replicate n a := by
   rw [← replicate_succ, dropLast_replicate, Nat.add_sub_cancel]
 
-@[simp] theorem tail_reverse (l : List α) : l.reverse.tail = l.dropLast.reverse := by
-  apply ext_getElem
-  · simp
-  · intro i h₁ h₂
-    simp [Nat.add_comm i, Nat.sub_add_eq]
-
 /-!
 ### splitAt
 

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

@@ -18,26 +18,6 @@ open Nat
 
 namespace List
 
-/-! ### dropLast -/
-
-theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l) := by
-  ext1
-  simp only [getElem?_tail, getElem?_dropLast, length_tail]
-  split <;> split
-  · rfl
-  · omega
-  · omega
-  · rfl
-
-@[simp] theorem dropLast_reverse (l : List α) : l.reverse.dropLast = l.tail.reverse := by
-  apply ext_getElem
-  · simp
-  · intro i h₁ h₂
-    simp only [getElem_dropLast, getElem_reverse, length_tail, getElem_tail]
-    congr
-    simp only [length_dropLast, length_reverse, length_tail] at h₁ h₂
-    omega
-
 /-! ### filter -/
 
 theorem length_filter_lt_length_iff_exists {l} :

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

@@ -28,59 +28,4 @@ theorem count_set [BEq α] (a b : α) (l : List α) (i : Nat) (h : i < l.length)
     (l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
   simp [count_eq_countP, countP_set, h]
 
-/--
-The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list,
-minus the difference in the lengths.
--/
-theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ := by
-  match s with
-  | .slnil => simp
-  | .cons a s =>
-    rename_i l
-    simp only [countP_cons, length_cons]
-    have := s.le_countP p
-    have := s.length_le
-    split <;> omega
-  | .cons₂ a s =>
-    rename_i l₁ l₂
-    simp only [countP_cons, length_cons]
-    have := s.le_countP p
-    have := s.length_le
-    split <;> omega
-
-theorem IsPrefix.le_countP (s : l₁ <+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
-  s.sublist.le_countP _
-
-theorem IsSuffix.le_countP (s : l₁ <:+ l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
-  s.sublist.le_countP _
-
-theorem IsInfix.le_countP (s : l₁ <:+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
-  s.sublist.le_countP _
-
-/--
-The number of elements satisfying a predicate in the tail of a list is
-at least one less than the number of elements satisfying the predicate in the list.
--/
-theorem le_countP_tail (l) : countP p l - 1 ≤ countP p l.tail := by
-  have := (tail_sublist l).le_countP p
-  simp only [length_tail] at this
-  omega
-
-variable [BEq α]
-
-theorem Sublist.le_count (s : l₁ <+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.le_countP _
-
-theorem IsPrefix.le_count (s : l₁ <+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.sublist.le_count _
-
-theorem IsSuffix.le_count (s : l₁ <:+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.sublist.le_count _
-
-theorem IsInfix.le_count (s : l₁ <:+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.sublist.le_count _
-
-theorem le_count_tail (a : α) (l) : count a l - 1 ≤ count a l.tail :=
-  le_countP_tail _
-
 end List

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

@@ -258,9 +258,6 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) :=
   | zero => simp at h
   | succ n => simp
 
-@[simp] theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1) := by
-  cases n <;> simp
-
 @[simp] theorem reverse_iota : reverse (iota n) = range' 1 n := by
   induction n with
   | zero => simp
@@ -451,9 +448,6 @@ theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) :
     l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a) := by
   simp [getLast?_eq_getElem?]
 
-@[simp] theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail := by
-  simp [enum]
-
 theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = x := by
   simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]
 

src/Init/Data/List/Range.lean

@@ -35,16 +35,11 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step)
 theorem range'_ne_nil (s : Nat) {n : Nat} : range' s n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp] theorem range'_zero : range' s 0 step = [] := by
+@[simp] theorem range'_zero : range' s 0 = [] := by
   simp
 
 @[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
 
-@[simp] theorem tail_range' (n : Nat) : (range' s n step).tail = range' (s + step) (n - 1) step := by
-  cases n with
-  | zero => simp
-  | succ n => simp [range'_succ]
-
 @[simp] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
   constructor
   · intro h
@@ -158,9 +153,6 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
 theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp] theorem tail_range (n : Nat) : (range n).tail = range' 1 (n - 1) := by
-  rw [range_eq_range', tail_range']
-
 @[simp]
 theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
   simp only [range_eq_range', range'_sublist_right]
@@ -227,12 +219,6 @@ theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).len
   simp only [getElem?_enumFrom, getElem?_eq_getElem h]
   simp
 
-@[simp]
-theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail := by
-  induction l generalizing n with
-  | nil => simp
-  | cons _ l ih => simp [ih, enumFrom_cons]
-
 theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
     map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
   ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl

src/Init/Data/List/Zip.lean

@@ -31,10 +31,6 @@ theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
 theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
     zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
 
-@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
-    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
-  cases l₁ <;> cases l₂ <;> simp
-
 theorem zip_append :
     ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
       zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
@@ -233,7 +229,6 @@ theorem drop_zipWith : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n
 
 @[deprecated drop_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_drop := @drop_zipWith
 
-@[simp]
 theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
   rw [← drop_one]; simp [drop_zipWith]
 
@@ -289,16 +284,12 @@ theorem head?_zipWithAll {f : Option α → Option β → γ} :
       | none, none => .none | a?, b? => some (f a? b?) := by
   simp [head?_eq_getElem?, getElem?_zipWithAll]
 
-@[simp] theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
+theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
     (zipWithAll f as bs).head h = f as.head? bs.head? := by
   apply Option.some.inj
   rw [← head?_eq_head, head?_zipWithAll]
   split <;> simp_all
 
-@[simp] theorem tail_zipWithAll {f : Option α → Option β → γ} :
-    (zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail := by
-  cases as <;> cases bs <;> simp
-
 theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
     zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
@@ -367,12 +358,6 @@ theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp
     (hr : lp.map Prod.snd = l') : lp = l.zip l' := by
   rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 := by
-  cases l <;> simp
-
-@[simp] theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2 := by
-  cases l <;> simp
-
 @[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -199,8 +199,9 @@ Performs a possibly type-changing transformation to a `MatcherApp`.
 If `useSplitter` is true, the matcher is replaced with the splitter.
 NB: Not all operations on `MatcherApp` can handle one `matcherName` is a splitter.
 
-If `addEqualities` is true, then equalities connecting the discriminant to the parameters of the
-alternative (like in `match h : x with …`) are be added, if not already there.
+The array `addEqualities`, if provided, indicates for which of the discriminants an equality
+connecting the discriminant to the parameters of the alternative (like in `match h : x with …`)
+should be added (if it is isn't already there).
 
 This function works even if the the type of alternatives do *not* fit the inferred type. This
 allows you to post-process the `MatcherApp` with `MatcherApp.inferMatchType`, which will
@@ -211,13 +212,20 @@ def transform
     [AddMessageContext n] [MonadOptions n]
     (matcherApp : MatcherApp)
     (useSplitter := false)
-    (addEqualities : Bool := false)
+    (addEqualities : Array Bool := mkArray matcherApp.discrs.size false)
     (onParams : Expr → n Expr := pure)
     (onMotive : Array Expr → Expr → n Expr := fun _ e => pure e)
     (onAlt : Expr → Expr → n Expr := fun _ e => pure e)
     (onRemaining : Array Expr → n (Array Expr) := pure) :
     n MatcherApp := do
 
+  if addEqualities.size != matcherApp.discrs.size then
+    throwError "MatcherApp.transform: addEqualities has wrong size"
+
+  -- Do not add equalities when the matcher already does so
+  let addEqualities := Array.zipWith addEqualities matcherApp.discrInfos fun b di =>
+    if di.hName?.isSome then false else b
+
   -- We also handle CasesOn applications here, and need to treat them specially in a
   -- few places.
   -- TODO: Expand MatcherApp with the necessary fields to make this more uniform
@@ -233,26 +241,17 @@ def transform
   let params' ← matcherApp.params.mapM onParams
   let discrs' ← matcherApp.discrs.mapM onParams
 
-  let (motive', uElim, addHEqualities) ← lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
+
+  let (motive', uElim) ← lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
     unless motiveArgs.size == matcherApp.discrs.size do
       throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
     let mut motiveBody' ← onMotive motiveArgs motiveBody
 
-    -- Prepend `(x = e) →` or `(HEq x e) → ` to the motive when an equality is requested
-    -- and not already present, and remember whether we added an Eq or a HEq
-    let mut addHEqualities : Array (Option Bool) := #[]
-    for arg in motiveArgs, discr in discrs', di in matcherApp.discrInfos do
-      if addEqualities && di.hName?.isNone then
-        if ← isProof arg then
-          addHEqualities := addHEqualities.push none
-        else
-          let heq ← mkEqHEq discr arg
-          motiveBody' ← liftMetaM <| mkArrow heq motiveBody'
-          addHEqualities := addHEqualities.push heq.isHEq
-      else
-        addHEqualities := addHEqualities.push none
+    -- Prepend (x = e) → to the motive when an equality is requested
+    for arg in motiveArgs, discr in discrs', b in addEqualities do if b then
+      motiveBody' ← liftMetaM <| mkArrow (← mkEq discr arg) motiveBody'
 
-    return (← mkLambdaFVars motiveArgs motiveBody', ← getLevel motiveBody', addHEqualities)
+    return (← mkLambdaFVars motiveArgs motiveBody', ← getLevel motiveBody')
 
   let matcherLevels ← match matcherApp.uElimPos? with
     | none     => pure matcherApp.matcherLevels
@@ -262,14 +261,15 @@ def transform
   -- (and count them along the way)
   let mut remaining' := #[]
   let mut extraEqualities : Nat := 0
-  for discr in discrs'.reverse, b in addHEqualities.reverse do
-    match b with
-    | none => pure ()
-    | some is_heq =>
-        remaining' := remaining'.push (← (if is_heq then mkHEqRefl else mkEqRefl) discr)
-        extraEqualities := extraEqualities + 1
+  for discr in discrs'.reverse, b in addEqualities.reverse do if b then
+    remaining' := remaining'.push (← mkEqRefl discr)
+    extraEqualities := extraEqualities + 1
 
   if useSplitter && !isCasesOn then
+    -- We replace the matcher with the splitter
+    let matchEqns ← Match.getEquationsFor matcherApp.matcherName
+    let splitter := matchEqns.splitterName
+
     let aux1 := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params'
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
@@ -278,10 +278,6 @@ def transform
       check aux1
     let origAltTypes ← inferArgumentTypesN matcherApp.alts.size aux1
 
-    -- We replace the matcher with the splitter
-    let matchEqns ← Match.getEquationsFor matcherApp.matcherName
-    let splitter := matchEqns.splitterName
-
     let aux2 := mkAppN (mkConst splitter matcherLevels.toList) params'
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'

src/Lean/Meta/Tactic/FunInd.lean

@@ -8,6 +8,7 @@ prelude
 import Lean.Meta.Basic
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Check
+import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Subst
 import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
@@ -401,51 +402,19 @@ def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do
     mvarid ← mvarid.assert (.mkSimple s!"ih{i+1}") (← inferType v) v
   return mvarid
 
+
 /--
-Goal cleanup:
-Substitutes equations (with `substVar`) to remove superfluous varialbes, and clears unused
-let bindings.
-
-Substitutes from the outside in so that the inner-bound variable name wins, but does a first pass
-looking only at variables with names with macro scope, so that preferably they disappear.
-
-Careful to only touch the context after the motives (given by the index) as the motive could depend
-on anything before, and `substVar` would happily drop equations about these fixed parameters.
+Substitutes equations, but makes sure to only substitute variables introduced after the motives
+(given by the index) as the motive could depend on anything before, and `substVar` would happily
+drop equations about these fixed parameters.
 -/
-partial def cleanupAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do
-  let mvarId ← go mvarId index true
-  let mvarId ← go mvarId index false
-  return mvarId
-where
-  go (mvarId : MVarId) (index : Nat) (firstPass : Bool) : MetaM MVarId := do
-    if let some mvarId ← cleanupAfter? mvarId index firstPass then
-      go mvarId index firstPass
-    else
-      return mvarId
-
-  allHeqToEq (mvarId : MVarId) (index : Nat) : MetaM MVarId :=
-    mvarId.withContext do
-      let mut mvarId := mvarId
-      for localDecl in (← getLCtx) do
-        if localDecl.index > index then
-          let (_, mvarId') ← heqToEq mvarId localDecl.fvarId
-          mvarId := mvarId'
-      return mvarId
-
-  cleanupAfter? (mvarId : MVarId) (index : Nat) (firstPass : Bool)  : MetaM (Option MVarId) := do
-    mvarId.withContext do
-      for localDecl in (← getLCtx) do
-        if localDecl.index > index && (!firstPass || localDecl.userName.hasMacroScopes) then
-          if localDecl.isLet then
-            if let some mvarId' ← observing? <| mvarId.clear localDecl.fvarId then
-              return some mvarId'
-          if let some mvarId' ← substVar? mvarId localDecl.fvarId then
-            -- After substituting, some HEq might turn into Eqs, and we want to be able to substitute
-            -- them as well
-            let mvarId' ← allHeqToEq mvarId' index
-            return some mvarId'
-      return none
-
+def substVarAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do
+  mvarId.withContext do
+    let mut mvarId := mvarId
+    for localDecl in (← getLCtx) do
+      if localDecl.index > index then
+        mvarId ← trySubstVar mvarId localDecl.fvarId
+    return mvarId
 
 /--
 Second helper monad collecting the cases as mvars
@@ -460,7 +429,7 @@ def M2.branch {α} (act : M2 α) : M2 α :=
 
 
 /-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis.  -/
-def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (toClear : Array FVarId)
+def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (toClear toPreserve : Array FVarId)
     (goal : Expr)  (e : Expr) : M2 Expr := do
   let _e' ← foldAndCollect oldIH newIH isRecCall e
   let IHs : Array Expr ← M.ask
@@ -472,6 +441,8 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr)
   trace[Meta.FunInd] "Goal before cleanup:{mvarId}"
   for fvarId in toClear do
     mvarId ← mvarId.clear fvarId
+  mvarId ← mvarId.cleanup (toPreserve := toPreserve)
+  trace[Meta.FunInd] "Goal after cleanup (toClear := {toClear.map mkFVar}) (toPreserve := {toPreserve.map mkFVar}):{mvarId}"
   modify (·.push mvarId)
   let mvar ← instantiateMVars mvar
   pure mvar
@@ -486,7 +457,7 @@ Like `mkLambdaFVars (usedOnly := true)`, but
 The result `r` can be applied with `r.beta (maskArray mask args)`.
 
 We use this when generating the functional induction principle to refine the goal through a `match`,
-here `xs` are the discriminants of the `match`.
+here `xs` are the discriminans of the `match`.
 We do not expect non-trivial discriminants to appear in the goal (and if they do, the user will
 get a helpful equality into the context).
 -/
@@ -516,7 +487,7 @@ Builds an expression of type `goal` by replicating the expression `e` into its t
 where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
 as `MVars` as it goes.
 -/
-partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
+partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
     (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M2 Expr := do
 
   -- if-then-else cause case split:
@@ -525,10 +496,10 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
     let c' ← foldAndCollect oldIH newIH isRecCall c
     let h' ← foldAndCollect oldIH newIH isRecCall h
     let t' ← withLocalDecl `h .default c' fun h => M2.branch do
-      let t' ← buildInductionBody toClear goal oldIH newIH isRecCall t
+      let t' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
-      let f' ← buildInductionBody toClear goal oldIH newIH isRecCall f
+      let f' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -537,11 +508,11 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
     let h' ← foldAndCollect oldIH newIH isRecCall h
     let t' ← withLocalDecl `h .default c' fun h => M2.branch do
       let t ← instantiateLambda t #[h]
-      let t' ← buildInductionBody toClear goal oldIH newIH isRecCall t
+      let t' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
       let f ← instantiateLambda f #[h]
-      let f' ← buildInductionBody toClear goal oldIH newIH isRecCall f
+      let f' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -552,8 +523,8 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
   match_expr goal with
   | And goal₁ goal₂ => match_expr e with
     | PProd.mk _α _β e₁ e₂ =>
-      let e₁' ← buildInductionBody toClear goal₁ oldIH newIH isRecCall e₁
-      let e₂' ← buildInductionBody toClear goal₂ oldIH newIH isRecCall e₂
+      let e₁' ← buildInductionBody toClear toPreserve goal₁ oldIH newIH isRecCall e₁
+      let e₂' ← buildInductionBody toClear toPreserve goal₂ oldIH newIH isRecCall e₂
       return mkApp4 (.const ``And.intro []) goal₁ goal₂ e₁' e₂'
     | _ =>
       throwError "Goal is PProd, but expression is:{indentExpr e}"
@@ -572,14 +543,14 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
     -- so we need to replace that IH
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform (useSplitter := true)
-        (addEqualities := true)
+        (addEqualities := mask.map not)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => M2.branch do
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let alt' ← buildInductionBody (toClear.push newIH'.fvarId!) goal' oldIH' newIH'.fvarId! isRecCall alt
+              let alt' ← buildInductionBody (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! isRecCall alt
               mkLambdaFVars #[newIH'] alt')
         (onRemaining := fun _ => pure #[.fvar newIH])
       return matcherApp'.toExpr
@@ -591,34 +562,32 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
       let (mask, absMotiveBody) ← mkLambdaFVarsMasked matcherApp.discrs goal
 
       let matcherApp' ← matcherApp.transform (useSplitter := true)
-        (addEqualities := true)
+        (addEqualities := mask.map not)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => M2.branch do
-          buildInductionBody toClear expAltType oldIH newIH isRecCall alt)
+          buildInductionBody toClear toPreserve expAltType oldIH newIH isRecCall alt)
       return matcherApp'.toExpr
 
   if let .letE n t v b _ := e then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
     return ← withLetDecl n t' v' fun x => M2.branch do
-      let b' ← buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
+      let b' ← buildInductionBody toClear toPreserve goal oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFVars #[x] b'
 
   if let some (n, t, v, b) := e.letFun? then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
     return ← withLocalDecl n .default t' fun x => M2.branch do
-      let b' ← buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
+      let b' ← buildInductionBody toClear toPreserve goal oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFun x v' b'
 
-  liftM <| buildInductionCase oldIH newIH isRecCall toClear goal e
+  liftM <| buildInductionCase oldIH newIH isRecCall toClear toPreserve goal e
 
 /--
-Given an expression `e` with metavariables `mvars`
-* performs more cleanup:
-  * removes unused let-expressions after index `index`
-  * tries to substitute variables after index `index`
+Given an expression `e` with metavariables
+* collects all these meta-variables,
 * lifts them to the current context by reverting all local declarations after index `index`
 * introducing a local variable for each of the meta variable
 * assigning that local variable to the mvar
@@ -636,7 +605,7 @@ do not handle delayed assignemnts correctly.
 def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : MetaM Expr := do
   trace[Meta.FunInd] "abstractIndependentMVars, to revert after {index}, original mvars: {mvars}"
   let mvars ← mvars.mapM fun mvar => do
-    let mvar ← cleanupAfter mvar index
+    let mvar ← substVarAfter mvar index
     mvar.withContext do
       let fvarIds := (← getLCtx).foldl (init := #[]) (start := index+1) fun fvarIds decl => fvarIds.push decl.fvarId
       let (_, mvar) ← mvar.revert fvarIds
@@ -693,7 +662,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
             let body ← instantiateLambda body targets
             removeLamda body fun oldIH body => do
               let body ← instantiateLambda body extraParams
-              let body' ← buildInductionBody #[genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
+              let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
               if body'.containsFVar oldIH then
                 throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
               mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
@@ -1003,7 +972,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
                 removeLamda body fun oldIH body => do
                   trace[Meta.FunInd] "replacing {Expr.fvar oldIH} with {genIH}"
                   let body ← instantiateLambda body extraParams
-                  let body' ← buildInductionBody #[genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
+                  let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
                   if body'.containsFVar oldIH then
                     throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
                   mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')

src/Std/Data/DHashMap/Basic.lean

@@ -186,15 +186,6 @@ section Unverified
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : (a : α) → β a → Bool)
-    (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
-  m.fold (init := (∅, ∅)) fun ⟨l, r⟩  a b =>
-    if f a b then
-      (l.insert a b, r)
-    else
-      (l, r.insert a b)
-
 @[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f
@@ -269,6 +260,10 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     DHashMap α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
+@[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    DHashMap α (fun _ => Unit) :=
+  Const.insertManyUnit ∅ l
+
 @[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
     (m : DHashMap α β) : Nat :=
   Raw.Internal.numBuckets m.1

src/Std/Data/DHashMap/Raw.lean

@@ -411,6 +411,14 @@ This is mainly useful to implement `HashSet.ofList`, so if you are considering u
     Raw α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
+/-- Creates a hash map from an array of keys, associating the value `()` with each key.
+
+This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
+`HashSet` or `HashSet.Raw` might be a better fit for you. -/
+@[inline] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    Raw α (fun _ => Unit) :=
+  Const.insertManyUnit ∅ l
+
 /--
 Returns the number of buckets in the internal representation of the hash map. This function may be
 useful for things like monitoring system health, but it should be considered an internal

src/Std/Data/HashMap/Basic.lean

@@ -190,11 +190,6 @@ section Unverified
     (m : HashMap α β) : HashMap α β :=
   ⟨m.inner.filter f⟩
 
-@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
-    (m : HashMap α β) : HashMap α β × HashMap α β :=
-  let ⟨l, r⟩ := m.inner.partition f
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 @[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init
@@ -255,6 +250,10 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
+@[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    HashMap α Unit :=
+  ⟨DHashMap.Const.unitOfArray l⟩
+
 @[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
     (m : HashMap α β) : Nat :=
   DHashMap.Internal.numBuckets m.inner

src/Std/Data/HashSet/Basic.lean

@@ -158,11 +158,6 @@ section Unverified
 @[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : α → Bool) (m : HashSet α) : HashSet α × HashSet α :=
-  let ⟨l, r⟩ := m.inner.partition fun a _ => f a
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
@@ -217,6 +212,14 @@ in the collection will be present in the returned hash set.
 @[inline] def ofList [BEq α] [Hashable α] (l : List α) : HashSet α :=
   ⟨HashMap.unitOfList l⟩
 
+/--
+Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
+collection contains multiple elements that are equal (with regard to `==`), then the last element
+in the collection will be present in the returned hash set.
+-/
+@[inline] def ofArray [BEq α] [Hashable α] (l : Array α) : HashSet α :=
+  ⟨HashMap.unitOfArray l⟩
+
 /-- Computes the union of the given hash sets. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α :=
   m₂.fold (init := m₁) fun acc x => acc.insert x

tests/lean/run/funind_structural.lean

@@ -54,7 +54,7 @@ termination_by structural x => x
 
 /--
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
-  (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t [])
+  (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (x : List α), (x = [] → False) → motive x [])
   (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
   ∀ (a : List α) (a_1 : List β), motive a a_1
 -/

tests/lean/run/funind_tests.lean

@@ -109,7 +109,11 @@ def let_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
+  (case2 :
+    ∀ (n : Nat),
+      let h2 := ⋯;
+      motive n → motive n.succ) :
   ∀ (a : Nat), motive a
 -/
 #guard_msgs in
@@ -527,7 +531,7 @@ termination_by xs => xs
 
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
 #check bar.induct
@@ -682,11 +686,12 @@ def foo : Nat → Nat → (k : Nat) → Fin k → Nat
 termination_by n => n
 
 /--
-info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop) (case1 : ∀ (k x : Nat) (x_1 : Fin k), motive 0 x k x_1)
-  (case2 : ∀ (k x : Nat), (x = 0 → False) → ∀ (x_2 : Fin k), motive x 0 k x_2)
-  (case3 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 0), motive x x_1 0 a)
-  (case4 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 1), motive x x_1 1 a)
-  (case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a) :
+info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop)
+  (case1 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), motive 0 x x_1 x_2)
+  (case2 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), (x = 0 → False) → motive x 0 x_1 x_2)
+  (case3 : ∀ (x x_1 : Nat) (x_2 : Fin 0), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 0 x_2)
+  (case4 : ∀ (x x_1 : Nat) (x_2 : Fin 1), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 1 x_2)
+  (case5 : ∀ (n m k : Nat) (x : Fin (k + 2)), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ x) :
   ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2
 -/
 #guard_msgs in

tests/lean/run/issue4146.lean

@@ -1,49 +0,0 @@
-set_option linter.unusedVariables false
-
-def bar (n : Nat) : Bool :=
-  if h : n = 0 then
-    true
-  else
-    match n with -- NB: the elaborator adds `h` as an discriminant
-    | m+1 => bar m
-termination_by n
-
--- set_option pp.match false
--- #print bar
--- #check bar.match_1
--- #print bar.induct
-
--- NB: The induction theorem has both `h` in scope, as its original type mentioning `x`,
--- and a refined `h` mentioning `m+1`.
--- The former is redundant here, but will we always know that?
--- No HEq betwen the two `h`s due to proof irrelevance
-
-/--
-info: bar.induct (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (m : Nat), ¬m + 1 = 0 → ¬m.succ = 0 → motive m → motive m.succ) (n : Nat) : motive n
--/
-#guard_msgs in
-#check bar.induct
-
-def baz (n : Nat) (i : Fin (n+1)) : Bool :=
-  if h : n = 0 then
-    true
-  else
-    match n, i + 1 with
-    | 1, _ => true
-    | m+2, j => baz (m+1) ⟨j.1-1, by omega⟩
-termination_by n
-
--- #print baz._unary
-
-/--
-info: baz.induct (motive : (n : Nat) → Fin (n + 1) → Prop) (case1 : ∀ (i : Fin (0 + 1)), motive 0 i)
-  (case2 : ¬1 = 0 → ∀ (i : Fin (1 + 1)), ¬1 = 0 → motive 1 i)
-  (case3 :
-    ∀ (m : Nat),
-      ¬m + 2 = 0 →
-        ∀ (i : Fin (m.succ.succ + 1)), ¬m.succ.succ = 0 → motive (m + 1) ⟨↑(i + 1) - 1, ⋯⟩ → motive m.succ.succ i)
-  (n : Nat) (i : Fin (n + 1)) : motive n i
--/
-#guard_msgs in
-#check baz.induct

tests/lean/run/issue5347.lean

@@ -9,9 +9,11 @@ def test (x: Nat): Nat :=
 
 -- set_option trace.Meta.FunInd true
 
+-- At the time of writing, the induction princpile misses the `f x = some k` assumptions:
+
 /--
-info: test.induct (motive : Nat → Prop) (case1 : ∀ (t k : Nat), f t = some k → motive t) (case2 : f 0 = none → motive 0)
-  (case3 : ∀ (n : Nat), f n.succ = none → motive n → motive n.succ) (x : Nat) : motive x
+info: test.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), motive x) (case2 : motive 0)
+  (case3 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check test.induct