From 2390fe0a2fbbdd283d21049a1e997026d7d1948c Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 7 Jan 2025 23:32:53 +0100
Subject: Lean 4.15

---
 Day16.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Day16.lean')

diff --git a/Day16.lean b/Day16.lean
index d91f6ad..ec602ca 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -226,7 +226,7 @@ private def SeenExitDirections.countExitDirections {table : OpticsTable} (seenDi
   let c := seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0
   have h₁ : c ≤ 4 * seenDirections.width * seenDirections.height := by
     have : c = seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0 := (rfl : c = seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0)
-    rw[this, Array.foldl_eq_foldl_toList]
+    rw[this, ←Array.foldl_toList]
     have : seenDirections.elements.toList.length = seenDirections.elements.size :=  Array.length_toList
     rw[seenDirections.size_valid] at this
     rw[Nat.mul_assoc,←this]
@@ -266,7 +266,7 @@ private theorem SeenExitDirections.countExitDirections_increasesWhenSet {table :
   simp at h₁ ⊢
   unfold Parsing.RectangularGrid.Coordinate.toIndex at h₁ ⊢
   unfold Array.set
-  simp[Array.foldl_eq_foldl_toList] at h₁ ⊢
+  simp[←Array.foldl_toList] at h₁ ⊢
   rw[Array.getElem_eq_getElem_toList] at h₁ ⊢
   apply countExitDirections_increasesWhenSet_Aux
   assumption
-- 
cgit v1.2.3

