diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean
index 7b56aedf69..de648d6b05 100644
--- a/src/Init/Internal/Order/Lemmas.lean
+++ b/src/Init/Internal/Order/Lemmas.lean
@@ -351,7 +351,7 @@ theorem monotone_forIn'_loop {α : Type uu}
     monotone (fun x => Array.forIn'.loop as (f x) i h b) := by
   induction i, h, b using Array.forIn'.loop.induct with
   | case1 => apply monotone_const
-  | case2 _ _ _ _ _ _ _ ih =>
+  | case2 _ _ _ _ _ _ ih =>
     apply monotone_bind
     · apply monotone_apply
       apply monotone_apply
@@ -424,7 +424,7 @@ theorem monotone_foldrM_fold
     unfold Array.foldrM.fold
     simp only [↓reduceIte, *]
     apply monotone_const
-  | case3 _ _ _ _ _ _ ih =>
+  | case3 _ _ _ _ _ ih =>
     unfold Array.foldrM.fold
     simp only [reduceCtorEq, ↓reduceIte, *]
     apply monotone_bind
@@ -601,7 +601,7 @@ theorem monotone_findSomeRevM?
   | case1 =>
     unfold Array.findSomeRevM?.find
     apply monotone_const
-  | case2 _ _ _ _ ih =>
+  | case2 _ _ _ ih =>
     unfold Array.findSomeRevM?.find
     apply monotone_bind
     · apply monotone_apply
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index 8118f46c30..b8ad779026 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -245,25 +245,25 @@ theorem toListModel_updateCell [Ord α] [TransOrd α] {k : α}
   induction l, hlb using updateCell.induct k f
   · simp_all [updateCell]
   · simp_all [updateCell]
-  · rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup hb' ih
+  · rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup ih
     simp only [updateCell, hcmp]
     split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
     rw [toListModel_balance, toListModel_filter_gt_of_lt hcmp hlo,
       toListModel_filter_lt_of_lt hcmp hlo, findCell_of_lt hcmp hlo, ih hlo.left]
     simp
-  · rename_i sz k' v' l r hl hcmp hf hl'
+  · rename_i sz k' v' l r hl hcmp hf
     simp only [updateCell, hcmp, hf]
     split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
     rw [toListModel_glue, toListModel_filter_gt_of_eq hcmp hlo, findCell_of_eq hcmp hlo,
       hf, toListModel_filter_lt_of_eq hcmp hlo]
     simp
-  · rename_i sz k' v' l r hl hcmp k'' v'' hf hl'
+  · rename_i sz k' v' l r hl hcmp k'' v'' hf
     simp only [updateCell, hcmp, hf]
     split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
     rw [toListModel_inner, toListModel_filter_gt_of_eq hcmp hlo, findCell_of_eq hcmp hlo,
       toListModel_filter_lt_of_eq hcmp hlo, hf]
     simp
-  · rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup hb' ih
+  · rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup ih
     simp only [updateCell, hcmp]
     split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
     rw [toListModel_filter_gt_of_gt hcmp hlo, findCell_of_gt hcmp hlo,