diff --git a/Std/Data/RBMap/Lemmas.lean b/Std/Data/RBMap/Lemmas.lean
index 44ca1b0003..124837fc26 100644
--- a/Std/Data/RBMap/Lemmas.lean
+++ b/Std/Data/RBMap/Lemmas.lean
@@ -601,8 +601,8 @@ theorem mem_insert [@TransCmp α cmp] {t : RBNode α} (ht : Balanced t c n) (ht
       let ⟨_, _, h₁, h₂⟩ := exists_insert_toList_zoom_node ht e
       simp [← mem_toList, h₂] at h; simp [← mem_toList, h₁]; rw [or_left_comm] at h ⊢
       rcases h with _|h <;> simp [*]
-      refine .inl fun h => ?_
-      rw [find?_eq_zoom, e] at h; cases h
+      refine .inl fun h' => ?_
+      rw [find?_eq_zoom, e] at h'; cases h'
       suffices cmpLT cmp v' v' by cases OrientedCmp.cmp_refl.symm.trans this.1
       have := ht₂.toList_sorted; simp [h₁, List.pairwise_append] at this
       exact h.elim (this.2.2 _ · |>.1) (this.2.1.1 _)