From bb6cbe0fe0c415fee1ece7980b0667055b0ed2db Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 17 Dec 2024 20:00:48 +0100
Subject: Remove useless simp_wf tactic calls

---
 Day10.lean | 1 -
 1 file changed, 1 deletion(-)

(limited to 'Day10.lean')

diff --git a/Day10.lean b/Day10.lean
index 720b7b9..c746ed1 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -1007,7 +1007,6 @@ private def removePathsMet {area : Area} : (List $ Area.PathHead area) → (List
 termination_by x => x.length
 decreasing_by
   all_goals
-    simp_wf
     exact Nat.lt_succ.mpr $ List.listFilterSmallerOrEqualList _ _
 
 
-- 
cgit v1.2.3

