From 0a86911bd0957ecd33bf00aee18e4700efc72f4e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Aug 2019 13:59:31 -0700
Subject: [PATCH] fix(library/init/data/persistenthashmap/basic): `isUnaryNode`

---
 library/init/data/persistenthashmap/basic.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/init/data/persistenthashmap/basic.lean b/library/init/data/persistenthashmap/basic.lean
index 03e0456884..eb278fcbe1 100644
--- a/library/init/data/persistenthashmap/basic.lean
+++ b/library/init/data/persistenthashmap/basic.lean
@@ -165,8 +165,9 @@ partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Opti
 def isUnaryNode : Node α β → Option (α × β)
 | (Node.entries entries)         := isUnaryEntries entries 0 none
 | (Node.collision keys vals heq) :=
-  if h : 0 < keys.size then
-    some (keys.fget ⟨0, h⟩, vals.fget ⟨0, heq ▸ h⟩)
+  if h : 1 = keys.size then
+    have 0 < keys.size from h ▸ (Nat.zeroLtSucc _);
+    some (keys.fget ⟨0, this⟩, vals.fget ⟨0, heq ▸ this⟩)
   else
     none