cleanup test

src/Init/Data/Array/Attach.lean

@@ -5,6 +5,7 @@ Authors: Joachim Breitner, Mario Carneiro
 -/
 prelude
 import Init.Data.Array.Mem
+import Init.Data.Array.Lemmas
 import Init.Data.List.Attach
 
 namespace Array
@@ -26,4 +27,154 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   with the same elements but in the type `{x // x ∈ xs}`. -/
 @[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
 
+@[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
+    l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray := by
+  simp [attachWith]
+
+@[simp] theorem _root_.List.attach_toArray {l : List α} :
+    l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
+  simp [attach]
+
+@[simp] theorem toList_attachWith {l : Array α} {P : α → Prop} {H : ∀ x ∈ l, P x} :
+   (l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H) := by
+  simp [attachWith]
+
+@[simp] theorem toList_attach {α : Type _} {l : Array α} :
+    l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
+  simp [attach]
+
+/-! ## unattach
+
+`Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
+
+We use it by providing a simp lemma `l.attach.unattach = l`, and simp lemmas which recognize higher order
+functions applied to `l : Array { x // p x }` which only depend on the value, not the predicate, and rewrite these
+in terms of a simpler function applied to `l.unattach`.
+
+Further, we provide simp lemmas that push `unattach` inwards.
+-/
+
+/--
+A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
+It is introduced as in intermediate step by lemmas such as `map_subtype`,
+and is ideally subsequently simplified away by `unattach_attach`.
+
+If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]` to unfold.
+-/
+def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (·.val)
+
+@[simp] theorem unattach_nil {α : Type _} {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := rfl
+@[simp] theorem unattach_push {α : Type _} {p : α → Prop} {a : { x // p x }} {l : Array { x // p x }} :
+    (l.push a).unattach = l.unattach.push a.1 := by
+  simp [unattach]
+
+@[simp] theorem size_unattach {α : Type _} {p : α → Prop} {l : Array { x // p x }} :
+    l.unattach.size = l.size := by
+  unfold unattach
+  simp
+
+@[simp] theorem _root_.List.unattach_toArray {α : Type _} {p : α → Prop} {l : List { x // p x }} :
+    l.toArray.unattach = l.unattach.toArray := by
+  simp [unattach, List.unattach]
+
+@[simp] theorem toList_unattach {α : Type _} {p : α → Prop} {l : Array { x // p x }} :
+    l.unattach.toList = l.toList.unattach := by
+  simp [unattach, List.unattach]
+
+@[simp] theorem unattach_attach {α : Type _} (l : Array α) : l.attach.unattach = l := by
+  cases l
+  simp
+
+@[simp] theorem unattach_attachWith {α : Type _} {p : α → Prop} {l : Array α}
+    {H : ∀ a ∈ l, p a} :
+    (l.attachWith p H).unattach = l := by
+  cases l
+  simp
+
+/-! ### Recognizing higher order functions using a function that only depends on the value. -/
+
+/--
+This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+theorem foldl_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : β → { x // p x } → β} {g : β → α → β} {x : β}
+    {hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
+    l.foldl f x = l.unattach.foldl g x := by
+  cases l
+  simp only [List.foldl_toArray', List.unattach_toArray]
+  rw [List.foldl_subtype] -- Why can't simp do this?
+  simp [hf]
+
+/-- Variant of `foldl_subtype` with side condition to check `stop = l.size`. -/
+@[simp] theorem foldl_subtype' {p : α → Prop} {l : Array { x // p x }}
+    {f : β → { x // p x } → β} {g : β → α → β} {x : β}
+    {hf : ∀ b x h, f b ⟨x, h⟩ = g b x} (h : stop = l.size) :
+    l.foldl f x 0 stop = l.unattach.foldl g x := by
+  subst h
+  rwa [foldl_subtype]
+
+/--
+This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+theorem foldr_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → β → β} {g : α → β → β} {x : β}
+    {hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
+    l.foldr f x = l.unattach.foldr g x := by
+  cases l
+  simp only [List.foldr_toArray', List.unattach_toArray]
+  rw [List.foldr_subtype]
+  simp [hf]
+
+/-- Variant of `foldr_subtype` with side condition to check `stop = l.size`. -/
+@[simp] theorem foldr_subtype' {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → β → β} {g : α → β → β} {x : β}
+    {hf : ∀ x h b, f ⟨x, h⟩ b = g x b} (h : start = l.size) :
+    l.foldr f x start 0 = l.unattach.foldr g x := by
+  subst h
+  rwa [foldr_subtype]
+
+/--
+This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem map_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    l.map f = l.unattach.map g := by
+  cases l
+  simp only [List.map_toArray, List.unattach_toArray]
+  rw [List.map_subtype]
+  simp [hf]
+
+@[simp] theorem filterMap_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Option β} {g : α → Option β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    l.filterMap f = l.unattach.filterMap g := by
+  cases l
+  simp only [size_toArray, List.filterMap_toArray', List.unattach_toArray, List.length_unattach,
+    mk.injEq]
+  rw [List.filterMap_subtype]
+  simp [hf]
+
+@[simp] theorem unattach_filter {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    (l.filter f).unattach = l.unattach.filter g := by
+  cases l
+  simp [hf]
+  rw [List.unattach_filter]
+  simp [hf]
+
+/-! ### Simp lemmas pushing `unattach` inwards. -/
+
+@[simp] theorem unattach_reverse {p : α → Prop} {l : Array { x // p x }} :
+    l.reverse.unattach = l.unattach.reverse := by
+  cases l
+  simp
+
+@[simp] theorem unattach_append {p : α → Prop} {l₁ l₂ : Array { x // p x }} :
+    (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
+  cases l₁
+  cases l₂
+  simp
+
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -108,23 +108,52 @@ theorem toArray_concat {as : List α} {x : α} :
   funext a
   simp
 
-@[simp] theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
+theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList]
   simp
 
-@[simp] theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
+theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
   rw [foldlM_eq_foldlM_toList]
 
-@[simp] theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
+theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
   rw [foldr_eq_foldr_toList]
 
-@[simp] theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
+theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
   rw [foldl_eq_foldl_toList]
 
+/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
+@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
+    (h : start = l.toArray.size) :
+    l.toArray.foldrM f init start 0 = l.foldrM f init := by
+  subst h
+  rw [foldrM_eq_reverse_foldlM_toList]
+  simp
+
+/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/
+@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.foldlM f init 0 stop = l.foldlM f init := by
+  subst h
+  rw [foldlM_eq_foldlM_toList]
+
+/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
+@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
+    (h : start = l.toArray.size) :
+    l.toArray.foldr f init start 0 = l.foldr f init := by
+  subst h
+  rw [foldr_eq_foldr_toList]
+
+/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
+@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.foldl f init 0 stop = l.foldl f init := by
+  subst h
+  rw [foldl_eq_foldl_toList]
+
 @[simp] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'
@@ -730,6 +759,18 @@ theorem foldr_induction
   simp [foldr, foldrM]; split; {exact go _ h0}
   · next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)
 
+@[congr]
+theorem foldl_congr {as bs : Array α} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g)
+     {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') :
+    as.foldl f a start stop = bs.foldl g b start' stop' := by
+  congr
+
+@[congr]
+theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β} (h₁ : f = g)
+     {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') :
+    as.foldr f a start stop = bs.foldr g b start' stop' := by
+  congr
+
 /-! ### map -/
 
 @[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
@@ -814,6 +855,13 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
     (as.map f)[i]? = as[i]?.map f := by
   simp [getElem?_def]
 
+@[simp] theorem map_push {f : α → β} {as : Array α} {x : α} :
+    (as.push x).map f = (as.map f).push (f x) := by
+  ext
+  · simp
+  · simp only [getElem_map, get_push, size_map]
+    split <;> rfl
+
 /-! ### mapIdx -/
 
 -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
@@ -920,6 +968,13 @@ abbrev filter_data := @toList_filter
 theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   (mem_filter.mp h).1
 
+@[congr]
+theorem filter_congr {as bs : Array α} (h : as = bs)
+    {f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
+    (h₁ : start = start') (h₂ : stop = stop') :
+    filter f as start stop = filter g bs start' stop' := by
+  congr
+
 /-! ### filterMap -/
 
 @[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
@@ -942,6 +997,13 @@ abbrev filterMap_data := @toList_filterMap
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
   simp only [mem_def, toList_filterMap, List.mem_filterMap]
 
+@[congr]
+theorem filterMap_congr {as bs : Array α} (h : as = bs)
+    {f : α → Option β} {g : α → Option β} (h' : f = g) {start stop start' stop' : Nat}
+    (h₁ : start = start') (h₂ : stop = stop') :
+    filterMap f as start stop = filterMap g bs start' stop' := by
+  congr
+
 /-! ### empty -/
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
@@ -1432,18 +1494,44 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   · simp
   · simp_all [List.set_eq_of_length_le]
 
-@[simp] theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
     l.toArray.anyM p = l.anyM p := by
   rw [← anyM_toList]
 
-@[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
   rw [any_toList]
 
-@[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
     l.toArray.allM p = l.allM p := by
   rw [← allM_toList]
 
-@[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [all_toList]
+
+/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
+@[simp] theorem anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.anyM p 0 stop = l.anyM p := by
+  subst h
+  rw [← anyM_toList]
+
+/-- Variant of `any_toArray` with a side condition on `stop`. -/
+@[simp] theorem any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.any p 0 stop = l.any p := by
+  subst h
+  rw [any_toList]
+
+/-- Variant of `allM_toArray` with a side condition on `stop`. -/
+@[simp] theorem allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.allM p 0 stop = l.allM p := by
+  subst h
+  rw [← allM_toList]
+
+/-- Variant of `all_toArray` with a side condition on `stop`. -/
+@[simp] theorem all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.all p 0 stop = l.all p := by
+  subst h
   rw [all_toList]
 
 @[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
@@ -1459,15 +1547,25 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem filter_toArray (p : α → Bool) (l : List α) :
-    l.toArray.filter p = (l.filter p).toArray := by
+@[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.filter p 0 stop = (l.filter p).toArray := by
+  subst h
   apply ext'
-  erw [toList_filter] -- `erw` required to unify `l.length` with `l.toArray.size`.
+  rw [toList_filter]
 
-@[simp] theorem filterMap_toArray (f : α → Option β) (l : List α) :
-    l.toArray.filterMap f = (l.filterMap f).toArray := by
+@[simp] theorem filterMap_toArray' (f : α → Option β) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
+  subst h
   apply ext'
-  erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
+  rw [toList_filterMap]
+
+theorem filter_toArray (p : α → Bool) (l : List α) :
+    l.toArray.filter p = (l.filter p).toArray := by
+  simp
+
+theorem filterMap_toArray (f : α → Option β) (l : List α) :
+    l.toArray.filterMap f = (l.filterMap f).toArray := by
+  simp
 
 @[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.join.toArray := by
   apply ext'

src/Init/Data/List/Attach.lean

@@ -647,7 +647,7 @@ and simplifies these to the function directly taking the value.
   | nil => simp
   | cons a l ih => simp [ih, hf]
 
-@[simp] theorem filter_unattach {p : α → Prop} {l : List { x // p x }}
+@[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
     (l.filter f).unattach = l.unattach.filter g := by
   induction l with
@@ -658,20 +658,20 @@ and simplifies these to the function directly taking the value.
 
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
-@[simp] theorem reverse_unattach {p : α → Prop} {l : List { x // p x }} :
+@[simp] theorem unattach_reverse {p : α → Prop} {l : List { x // p x }} :
     l.reverse.unattach = l.unattach.reverse := by
   simp [unattach, -map_subtype]
 
-@[simp] theorem append_unattach {p : α → Prop} {l₁ l₂ : List { x // p x }} :
+@[simp] theorem unattach_append {p : α → Prop} {l₁ l₂ : List { x // p x }} :
     (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
   simp [unattach, -map_subtype]
 
-@[simp] theorem join_unattach {p : α → Prop} {l : List (List { x // p x })} :
+@[simp] theorem unattach_join {p : α → Prop} {l : List (List { x // p x })} :
     l.join.unattach = (l.map unattach).join := by
   unfold unattach
   induction l <;> simp_all
 
-@[simp] theorem replicate_unattach {p : α → Prop} {n : Nat} {x : { x // p x }} :
+@[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
     (List.replicate n x).unattach = List.replicate n x.1 := by
   simp [unattach, -map_subtype]
 

src/Lean/Meta/Tactic/Clear.lean

@@ -43,31 +43,9 @@ def _root_.Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVar
   mvarId.clear fvarId <|> pure mvarId
 
 /--
-Try to clear the given fvars from the local context.
-
-The fvars must be given in the order they appear in the local context.
-
-See also `tryClearMany'` which takes care of reordering internally,
-and returns the cleared hypotheses along with the new goal.
+Try to erase the given free variables from the goal `mvarId`.
 -/
 def _root_.Lean.MVarId.tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
   fvarIds.foldrM (init := mvarId) fun fvarId mvarId => mvarId.tryClear fvarId
 
-/--
-Try to clear the given fvars from the local context. Returns the new goal and
-the hypotheses that were cleared.
-
-Does not require the `hyps` to be given in the order in which they
-appear in the local context.
--/
-def _root_.Lean.MVarId.tryClearMany' (goal : MVarId) (fvarIds : Array FVarId) :
-    MetaM (MVarId × Array FVarId) :=
-  goal.withContext do
-    let fvarIds := (← getLCtx).sortFVarsByContextOrder fvarIds
-    fvarIds.foldrM (init := (goal, Array.mkEmpty fvarIds.size))
-      fun h (goal, cleared) => do
-        let goal' ← goal.tryClear h
-        let cleared := if goal == goal' then cleared else cleared.push h
-        return (goal', cleared)
-
 end Lean.Meta

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -248,7 +248,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
       let goals ← ci.runMetaM {} (do
         let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
         let goals ← goals.mapM Widget.goalToInteractive
-        return ⟨goals⟩
+        return {goals}
       )
       -- compute the goal diff
       ciAfter.runMetaM {} (do

src/Std/Data/DHashMap/Basic.lean

@@ -75,9 +75,6 @@ instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
     (b : β a) : DHashMap α β :=
   ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩
 
-instance : Singleton (Σ a, β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ => DHashMap.empty.insert a b⟩
-instance : Insert (Σ a, β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩
-
 @[inline, inherit_doc Raw.insertIfNew] def insertIfNew (m : DHashMap α β)
     (a : α) (b : β a) : DHashMap α β :=
   ⟨Raw₀.insertIfNew ⟨m.1, m.2.size_buckets_pos⟩ a b, .insertIfNew₀ m.2⟩
@@ -264,12 +261,6 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     DHashMap α β :=
   insertMany ∅ l
 
-/-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
-@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : DHashMap α β) : DHashMap α β :=
-  m₂.fold (init := m₁) fun acc x => acc.insert x
-
-instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩
-
 @[inline, inherit_doc Raw.Const.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
     (l : List (α × β)) : DHashMap α (fun _ => β) :=
   Const.insertMany ∅ l

src/Std/Data/HashMap/Basic.lean

@@ -76,9 +76,6 @@ instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
     (b : β) : HashMap α β :=
   ⟨m.inner.insert a b⟩
 
-instance : Singleton (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ => HashMap.empty.insert a b⟩
-instance : Insert (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩
-
 @[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew (m : HashMap α β)
     (a : α) (b : β) : HashMap α β :=
   ⟨m.inner.insertIfNew a b⟩
@@ -254,12 +251,6 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     HashMap α β :=
   ⟨DHashMap.Const.ofList l⟩
 
-/-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
-@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashMap α β) : HashMap α β :=
-  m₂.fold (init := m₁) fun acc x => acc.insert x
-
-instance [BEq α] [Hashable α] : Union (HashMap α β) := ⟨union⟩
-
 @[inline, inherit_doc DHashMap.Const.unitOfList] def unitOfList [BEq α] [Hashable α] (l : List α) :
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩

src/Std/Data/HashSet/Basic.lean

@@ -77,9 +77,6 @@ equal (with regard to `==`) to the given element, then the hash set is returned
 @[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
   ⟨m.inner.insertIfNew a ()⟩
 
-instance : Singleton α (HashSet α) := ⟨fun a => HashSet.empty.insert a⟩
-instance : Insert α (HashSet α) := ⟨fun a s => s.insert a⟩
-
 /--
 Checks whether an element is present in a set and inserts the element if it was not found.
 If the hash set already contains an element that is equal (with regard to `==`) to the given
@@ -195,18 +192,6 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForM m (HashSet α) α
 instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α) α where
   forIn m init f := m.forIn f init
 
-/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
-@[inline] def all (m : HashSet α) (p : α → Bool) : Bool := Id.run do
-  for a in m do
-    if ¬ p a then return false
-  return true
-
-/-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds. -/
-@[inline] def any (m : HashSet α) (p : α → Bool) : Bool := Id.run do
-  for a in m do
-    if p a then return true
-  return false
-
 /-- Transforms the hash set into a list of elements in some order. -/
 @[inline] def toList (m : HashSet α) : List α :=
   m.inner.keys
@@ -240,12 +225,10 @@ 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, by traversing `m₂` and inserting its elements into `m₁`. -/
+/-- 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
 
-instance [BEq α] [Hashable α] : Union (HashSet α) := ⟨union⟩
-
 /--
 Returns the number of buckets in the internal representation of the hash set. This function may
 be useful for things like monitoring system health, but it should be considered an internal

src/stdlib.make.in

@@ -70,7 +70,6 @@ ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: $
 	@echo "[    ] Building $@"
 ifeq "${CMAKE_SYSTEM_NAME}" "Windows"
 # on Windows, must remove file before writing a new one (since the old one may be in use)
-	@rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
 	@rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
 # "half-way point" DLL to avoid symbol limit
 # include Lean.Meta.WHNF and leancpp except for `initialize.cpp`
@@ -105,8 +104,6 @@ Lake:
 
 ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/temp/libLake.a.export
 	@echo "[    ] Building $@"
-# on Windows, must remove file before writing a new one (since the old one may be in use)
-	@rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
 	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \
 	  ${LAKESHARED_LINKER_FLAGS} -lleanshared -lleanshared_1 -lInit_shared ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 

tests/lean/run/hashmap.lean

@@ -332,10 +332,6 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
 #guard_msgs in
 #eval HashMap.ofList [(1, 2), (1, 4)]
 
-/-- info: Std.HashMap.ofList [(37, 37), (4, 5), (3, 6), (2, 4), (1, 2)] -/
-#guard_msgs in
-#eval m ∪ {(4, 5), (37, 37)}
-
 end HashMap
 
 namespace HashSet.Raw
@@ -428,22 +424,6 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
     ans := k :: ans
   return ans
 
-/-- info: true -/
-#guard_msgs in
-#eval m.any fun x => x > 4
-
-/-- info: false -/
-#guard_msgs in
-#eval m.any fun x => x = 0
-
-/-- info: true -/
-#guard_msgs in
-#eval m.all fun x => x < 2^30
-
-/-- info: false -/
-#guard_msgs in
-#eval m.all fun x => x > 4
-
 /-- info: [1000000000, 2, 1] -/
 #guard_msgs in
 #eval m.toList
@@ -452,10 +432,6 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
 #guard_msgs in
 #eval m.toArray
 
-/-- info: Std.HashSet.ofList [1000000000, 2, 1, 16] -/
-#guard_msgs in
-#eval m ∪ {16, 16}
-
 /-- info: [1000000000, 2, 1, 16] -/
 #guard_msgs in
 #eval (m.insertMany [16, 16]).toList

tests/lean/run/nested_inductive.lean

@@ -47,3 +47,37 @@ def depth : Tree → Nat
 end Tree
 
 end List
+
+namespace Array
+
+inductive Tree where | node : Array Tree → Tree
+
+namespace Tree
+
+def rev : Tree → Tree
+  | node ts => .node (ts.attach.reverse.map (fun ⟨t, _⟩ => t.rev))
+
+-- Note that `simp` now automatically removes the `attach`.
+@[simp] theorem rev_def (ts : Array Tree) :
+    Tree.rev (.node ts) = .node (ts.reverse.map rev) := by
+  simp [Tree.rev]
+
+/-- Define `size` using a `foldl` over `attach`. -/
+def size : Tree → Nat
+  | node ts => 1 + ts.attach.foldl (fun acc ⟨t, _⟩ => acc + t.size) 0
+
+@[simp] theorem size_def (ts : Array Tree) :
+    size (.node ts) = 1 + ts.foldl (fun acc t => acc + t.size) 0 := by
+  simp [size]
+
+/-- Define `depth` using a `foldr` over `attach`. -/
+def depth : Tree → Nat
+  | node ts => 1 + ts.attach.foldr (fun ⟨t, _⟩ acc => acc + t.depth) 0
+
+@[simp] theorem depth_def (ts : Array Tree) :
+    depth (.node ts) = 1 + ts.foldr (fun t acc => acc + t.depth) 0 := by
+  simp [depth]
+
+end Tree
+
+end Array