Remove useless simp_wf tactic callsHEADmain

3 files changed, 0 insertions, 3 deletions

diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 348db25..637f807 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -103,7 +103,6 @@ protected def RectangularGrid.parseSingleLine (parseCharacter : Char → Except
       RectangularGrid.parseSingleLine parseCharacter (alreadyParsed.push element) (remainingLine.drop 1)
 termination_by remainingLine.bsize
 decreasing_by
-  simp_wf
   simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at _h₁
   simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.add_byteIdx, Nat.sub_eq]
   split
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 _ _
 
 
diff --git a/Day12.lean b/Day12.lean
index a9aa172..63410be 100644
--- a/Day12.lean
+++ b/Day12.lean
@@ -72,7 +72,6 @@ where
       | .ok v => parseLeftBlock (s.drop 1) $ v :: p
   termination_by s => s.bsize
   decreasing_by
-    simp_wf
     rename_i h₁
     apply Substring.drop_bsize_dec _ _ h₁ Nat.one_ne_zero
   parseMaskChar : Char → Except ParsingError SpringState := λ