From 671ccf18e506398fd8eb65ebac92ec6d2fd03ccd Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 13 Apr 2025 20:43:15 +0200
Subject: Lean 4.17

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

(limited to 'Day16.lean')

diff --git a/Day16.lean b/Day16.lean
index ec602ca..7e5d3a9 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -267,7 +267,7 @@ private theorem SeenExitDirections.countExitDirections_increasesWhenSet {table :
   unfold Parsing.RectangularGrid.Coordinate.toIndex at h₁ ⊢
   unfold Array.set
   simp[←Array.foldl_toList] at h₁ ⊢
-  rw[Array.getElem_eq_getElem_toList] at h₁ ⊢
+  rw[←Array.getElem_toList] at h₁ ⊢
   apply countExitDirections_increasesWhenSet_Aux
   assumption
 
-- 
cgit v1.2.3