diff --git a/src/Std/Data/DHashMap/Internal/List/Perm.lean b/src/Std/Data/DHashMap/Internal/List/Perm.lean
index 172cd24a71..c5bc1faa9b 100644
--- a/src/Std/Data/DHashMap/Internal/List/Perm.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Perm.lean
@@ -92,7 +92,7 @@ theorem Perm.map (f : α → β) {l₁ l₂ : List α} (h : Perm l₁ l₂) : Pe
   induction h
   · exact .refl _
   · exact .cons _ ‹_›
-  . exact .swap _ _ ‹_›
+  · exact .swap _ _ ‹_›
   · exact .trans ‹_› ‹_›
 
 theorem reverse_perm {l : List α} : Perm l.reverse l := by
diff --git a/src/Std/Data/DHashMap/Internal/List/Sublist.lean b/src/Std/Data/DHashMap/Internal/List/Sublist.lean
index bf8c666904..2c6d1d4622 100644
--- a/src/Std/Data/DHashMap/Internal/List/Sublist.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Sublist.lean
@@ -43,7 +43,7 @@ theorem Sublist.length_le {l₁ l₂ : List α} (h : Sublist l₁ l₂) : l₁.l
 theorem Sublist.of_cons_left {l₁ l₂ : List α} {a : α} (h : Sublist (a::l₁) l₂) : Sublist l₁ l₂ := by
   cases h
   · exact .cons_right .refl
-  . exact .cons_right ‹_›
+  · exact .cons_right ‹_›
   · next h t ih => exact .cons_right (Sublist.of_cons_left ‹_›)
 
 @[simp]