spaces

Author: kim-em

src/Init/Data/Array/Lemmas.lean

@@ -2798,7 +2798,7 @@ theorem reverse_eq_iff {xs ys : Array α} : xs.reverse = ys ↔ xs = ys.reverse
   cases xs
   simp
 
-@[grind _=_]theorem filterMap_reverse {f : α → Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
+@[grind _=_] theorem filterMap_reverse {f : α → Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
   cases xs
   simp
 
@@ -3527,7 +3527,7 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
     (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) :=
   foldrM_append' w
 
-@[grind _=_]theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
+@[grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
     (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) :=
   foldlM_append
 

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

@@ -56,7 +56,7 @@ theorem getElem?_take_eq_none {l : List α} {i j : Nat} (h : i ≤ j) :
     (l.take i)[j]? = none :=
   getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
-@[grind =]theorem getElem?_take {l : List α} {i j : Nat} :
+@[grind =] theorem getElem?_take {l : List α} {i j : Nat} :
     (l.take i)[j]? = if j < i then l[j]? else none := by
   split
   · next h => exact getElem?_take_of_lt h

src/Init/Data/Vector/Lemmas.lean

@@ -2105,7 +2105,7 @@ abbrev forall_mem_mkVector := @forall_mem_replicate
 @[deprecated getElem_replicate (since := "2025-03-18")]
 abbrev getElem_mkVector := @getElem_replicate
 
-@[grind]theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
+@[grind] theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
   simp [getElem?_def]
 
 @[deprecated getElem?_replicate (since := "2025-03-18")]

src/Std/Data/DTreeMap/Lemmas.lean

@@ -3961,7 +3961,7 @@ theorem getKey?_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.getKey? t.maxKey! = some t.maxKey! :=
   Impl.getKey?_maxKey! t.wf he
 
-@[grind =]theorem getKey_maxKey! [TransCmp cmp] [Inhabited α] {hc} :
+@[grind =] theorem getKey_maxKey! [TransCmp cmp] [Inhabited α] {hc} :
     t.getKey t.maxKey! hc = t.maxKey! :=
   Impl.getKey_maxKey! t.wf
 

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -305,7 +305,7 @@ theorem get_eq_get_get? [LawfulBEq α] {a : α} {h} :
     m.get a h = (m.get? a).get (mem_iff_isSome_get?.mp h) :=
   m.inductionOn (fun _ _ => DHashMap.get_eq_get_get?) h
 
-@[grind =]theorem get_get? [LawfulBEq α] {a : α} {h} :
+@[grind =] theorem get_get? [LawfulBEq α] {a : α} {h} :
     (m.get? a).get h = m.get a (mem_iff_isSome_get?.mpr h) :=
   m.inductionOn (fun _ _ => DHashMap.get_get?) h
 
@@ -405,7 +405,7 @@ variable {β : Type v} {m : ExtDHashMap α (fun _ => β)}
 theorem get!_empty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : get! (∅ : ExtDHashMap α (fun _ => β)) a = default :=
   DHashMap.Const.get!_empty
 
-@[grind =]theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
+@[grind =] theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
     get! (m.insert k v) a = if k == a then v else get! m a :=
   m.inductionOn fun _ => DHashMap.Const.get!_insert
 
@@ -462,7 +462,7 @@ theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} :
     (∅ : ExtDHashMap α β).getD a fallback = fallback :=
   DHashMap.getD_empty
 
-@[grind =]theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
+@[grind =] theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
     (m.insert k v).getD a fallback =
       if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback :=
   m.inductionOn fun _ => DHashMap.getD_insert

src/Std/Data/HashSet/RawLemmas.lean

@@ -167,7 +167,7 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : 
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : k ∈ m.insert k :=
   HashMap.Raw.mem_insertIfNew_self h.out
 
-@[grind =]theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+@[grind =] theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
   HashMap.Raw.size_insertIfNew h.out
 

src/Std/Data/TreeMap/Lemmas.lean

@@ -2001,7 +2001,7 @@ theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
     (t.modify k f).minKey? = t.minKey? :=
   DTreeMap.Const.minKey?_modify_eq_minKey?
 
-@[grind =]theorem isSome_minKey?_modify [TransCmp cmp] {k f} :
+@[grind =] theorem isSome_minKey?_modify [TransCmp cmp] {k f} :
     (t.modify k f).minKey?.isSome = !t.isEmpty :=
   DTreeMap.Const.isSome_minKey?_modify
 

src/Std/Data/TreeSet/Lemmas.lean

@@ -347,7 +347,7 @@ theorem getD_of_isEmpty [TransCmp cmp] {a fallback : α} :
     t.isEmpty = true → t.getD a fallback = fallback :=
   TreeMap.getKeyD_of_isEmpty
 
-@[grind =]theorem getD_insert [TransCmp cmp] {k a fallback : α} :
+@[grind =] theorem getD_insert [TransCmp cmp] {k a fallback : α} :
     (t.insert k).getD a fallback =
       if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getD a fallback :=
   TreeMap.getKeyD_insertIfNew