Adjust simp spacing

leanprover · Dec 3, 2024 · bddf6fb · bddf6fb
1 parent 7f4bc44
commit bddf6fb
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -480,7 +480,7 @@ theorem insertMany_eq_insertListₘ [BEq α] [Hashable α](m : Raw₀ α β) (l
     t.val.insertListₘ l from this _
   intro t
   induction l generalizing m with
-  | nil => simp[insertListₘ]
+  | nil => simp [insertListₘ]
   | cons hd tl ih =>
     simp only [List.foldl_cons,insertListₘ]
     apply ih
@@ -524,7 +524,7 @@ theorem Const.insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α
     Const.insertListₘ t.val l from this _
   intro t
   induction l generalizing m with
-  | nil => simp[insertListₘ]
+  | nil => simp [insertListₘ]
   | cons hd tl ih =>
     simp only [List.foldl_cons,insertListₘ]
     apply ih
@@ -538,7 +538,7 @@ theorem Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ [BEq α] [Hashable
     Const.insertListIfNewUnitₘ t.val l from this _
   intro t
   induction l generalizing m with
-  | nil => simp[insertListIfNewUnitₘ]
+  | nil => simp [insertListIfNewUnitₘ]
   | cons hd tl ih =>
     simp only [List.foldl_cons,insertListIfNewUnitₘ]
     apply ih

diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean
@@ -201,11 +201,11 @@ theorem filter_val [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) →
 
 theorem insertMany_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} :
     m.insertMany l = Raw₀.insertMany ⟨m, h.size_buckets_pos⟩ l := by
-  simp[Raw.insertMany, h.size_buckets_pos]
+  simp [Raw.insertMany, h.size_buckets_pos]
 
 theorem insertMany_val [BEq α][Hashable α] {m : Raw₀ α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} :
     m.val.insertMany l = m.insertMany l := by
-  simp[Raw.insertMany, m.2]
+  simp [Raw.insertMany, m.2]
 
 section
 

diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -723,7 +723,7 @@ theorem toListModel_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHas
     Perm (toListModel (insertListₘ m l).1.buckets) (List.insertList (toListModel m.1.buckets) l) := by
   induction l generalizing m with
   | nil =>
-    simp[insertListₘ, List.insertList]
+    simp [insertListₘ, List.insertList]
   | cons hd tl ih =>
     simp only [insertListₘ, List.insertList]
     apply Perm.trans