From 2390fe0a2fbbdd283d21049a1e997026d7d1948c Mon Sep 17 00:00:00 2001 From: Andreas Grois 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