more cleanups

src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean

@@ -221,7 +221,7 @@ namespace Const
 variable {β : Type v}
 
 theorem toList_alter [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β}
-    {l : AssocList α (fun _ => β) } : Perm (alter a f l).toList (Const.alterKey a f l.toList) := by
+    {l : AssocList α (fun _ => β)} : Perm (alter a f l).toList (Const.alterKey a f l.toList) := by
   rw [Const.alterKey]
   split
   · next heq =>
@@ -256,7 +256,7 @@ theorem toList_alter [BEq α] [EquivBEq α] {a : α} {f : Option β → Option 
         refine insertEntry_cons_of_false (Bool.not_eq_true _ ▸ heq₂) |>.symm |> Perm.trans ?_
         exact Perm.cons _ <| ih heq
 
-theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α (fun _ => β) } :
+theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α (fun _ => β)} :
     modify a f l = alter a (·.map f) l := by
   induction l
   · rfl

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -969,7 +969,8 @@ def insertEntry [BEq α]  (k : α) (v : β k) (l : List ((a : α) × β a)) : Li
 
 @[simp]
 theorem insertEntry_nil [BEq α] {k : α} {v : β k} :
-    insertEntry k v ([] : List ((a : α) × β a)) = [⟨k, v⟩] := by simp [insertEntry]
+    insertEntry k v ([] : List ((a : α) × β a)) = [⟨k, v⟩] :=
+  by simp [insertEntry]
 
 theorem insertEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
     {v' : β k'} (h : (k' == k) = false) :
@@ -1902,9 +1903,9 @@ theorem alterKey_nil [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Opt
     | none => []
     | some b => [⟨a, b⟩] := rfl
 
-theorem containsKey_alterKey_iff [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
+theorem containsKey_alterKey [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
     {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
-    containsKey a (alterKey a f l) ↔ (f (getValueCast? a l)).isSome := by
+    containsKey a (alterKey a f l) = (f (getValueCast? a l)).isSome := by
   match l with
   | [] =>
     simp only [getValueCast?_nil, Bool.coe_iff_coe, alterKey_nil]
@@ -2012,10 +2013,10 @@ def alterKey [BEq α] (k : α) (f : Option β → Option β)
 
 theorem length_alterKey [BEq α] [EquivBEq α] {k : α} {f : Option β → Option β}
     {l : List ((_ : α) × β)} : (alterKey k f l).length =
-    if h : containsKey k l then
-      if f (some (getValue k l h)) |>.isSome then l.length else l.length - 1
-    else
-      if f none |>.isSome then l.length + 1 else l.length := by
+      if h : containsKey k l then
+        if f (some (getValue k l h)) |>.isSome then l.length else l.length - 1
+      else
+        if f none |>.isSome then l.length + 1 else l.length := by
   rw [alterKey]
   cases h : getValue? k l <;> split <;> simp_all [length_eraseKey, length_insertEntry,
     containsKey_eq_isSome_getValue?, ← getValue?_eq_some_getValue, -getValue?_eq_none]
@@ -2082,8 +2083,8 @@ theorem mem_insertEntry_of_key_ne [BEq α] [EquivBEq α] {a : α} {b : β}
     exact fun x => hne (beq_of_eq x.1) |> False.elim
 
 theorem mem_eraseKey_of_key_ne [BEq α] [EquivBEq α] {a : α}
-    {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.1 == a) = false)
-    : p ∈ eraseKey a l ↔ p ∈ l := by
+    {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.1 == a) = false) :
+    p ∈ eraseKey a l ↔ p ∈ l := by
   induction l
   · simp only [eraseKey_nil]
   · next ih =>

src/Std/Data/DHashMap/Internal/WF.lean

@@ -563,7 +563,7 @@ theorem wfImp_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
       simp only [buckets_withComputedSize]
       simp only [containsKey_of_perm <| toListModel_updateBucket_alter h]
       rw [← getValueCast?_eq_some_getValueCast h₁]
-      conv => lhs; congr; rw [containsKey_alterKey_iff (a := a) (f := f) h.distinct];
+      conv => lhs; congr; rw [containsKey_alterKey h.distinct];
     · next h₁ =>
       rw [containsₘ_eq_containsKey h] at h₁
       rw [alterKey]
@@ -586,7 +586,7 @@ variable {β : Type v}
 theorem toListModel_updateBucket_alter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
     {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} :
     Perm (toListModel (updateBucket m.1.buckets m.2 a (AssocList.Const.alter a f)))
-    (Const.alterKey a f (toListModel m.1.buckets)) := by
+      (Const.alterKey a f (toListModel m.1.buckets)) := by
   exact toListModel_updateBucket h AssocList.Const.toList_alter List.Const.alterKey_of_perm
     List.Const.alterKey_append_of_containsKey_right_eq_false