From 1d5da634822f4c2e7dfd06f1bb0f3d0bb6a61a0f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Feb 2022 16:51:47 -0800
Subject: [PATCH] chore: simplify `Array.isEqvAux`

---
 src/Init/Data/Array/Basic.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 6b56e5ff22..d5a434ddcc 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -514,11 +514,7 @@ namespace Array
 @[specialize]
 def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
   if h : i < a.size then
-     let aidx : Fin a.size := ⟨i, h⟩;
-     let bidx : Fin b.size := ⟨i, hsz ▸ h⟩;
-     match p (a.get aidx) (b.get bidx) with
-     | true  => isEqvAux a b hsz p (i+1)
-     | false => false
+     p (a.get ⟨i, h⟩) (b.get ⟨i, hsz ▸ h⟩) && isEqvAux a b hsz p (i+1)
   else
     true
 termination_by _ => a.size - i