From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 10 Oct 2025 00:30:19 +0200
Subject: Lean 4.18

---
 Day13.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Day13.lean')

diff --git a/Day13.lean b/Day13.lean
index 22dc0b5..25f1f37 100644
--- a/Day13.lean
+++ b/Day13.lean
@@ -51,7 +51,7 @@ match parse input with
   <;> simp only [Bool.false_eq_true, ↓reduceIte, gt_iff_lt]
   rw[←List.mapM'_eq_mapM]
   unfold List.mapM'
-  have h₂ : (input.toSubstring.splitOn "\n\n") ≠ [] := List.isEmpty_eq_false.mp h₁
+  have h₂ : (input.toSubstring.splitOn "\n\n") ≠ [] := List.isEmpty_eq_false_iff.mp h₁
   cases h₃ : input.toSubstring.splitOn "\n\n"
   case false.nil => contradiction
   case false.cons b bs =>
-- 
cgit v1.2.3