From 5339692f488c39af081210ae5e2668ee4fdafc52 Mon Sep 17 00:00:00 2001
From: Quang Dao <quangdao@umich.edu>
Date: Mon, 2 Dec 2024 17:03:29 -0700
Subject: [PATCH] fixed error

---
 Batteries/Data/Fin/Fold.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean
index 8bcb1d644a..a7923ca34f 100644
--- a/Batteries/Data/Fin/Fold.lean
+++ b/Batteries/Data/Fin/Fold.lean
@@ -80,7 +80,7 @@ theorem dfoldrM_loop [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Typ
   | zero =>
     rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind]
     conv => rhs; rw [←bind_pure (f 0 x)]
-    congr; funext; exact dfoldrM_loop_zero ..
+    congr
   | succ i ih =>
     rw [dfoldrM_loop_succ _ h, dfoldrM_loop_succ _ (Nat.succ_lt_succ_iff.mp h), bind_assoc]
     congr; funext; exact ih ..