diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean
index 253fb096d4..016ffa59fa 100644
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -285,8 +285,8 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
     contradiction
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h
-    have ihl := ihl bl
-    have ihr := ihr br
+    specialize ihl bl
+    specialize ihr br
     by_cases' k < key; by_cases' key < k
     have_eq key k
     by_cases' k' < k; by_cases' k  < k'