diff options
| author | Andreas Grois <andi@grois.info> | 2025-01-07 23:32:53 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-01-07 23:32:53 +0100 |
| commit | 2390fe0a2fbbdd283d21049a1e997026d7d1948c (patch) | |
| tree | 2e529367592943cd38a04e0a87fc3f22a87b4cc8 /Day16.lean | |
| parent | 4749b3ca572618fa1a7cdb17e2abba9b498279ca (diff) | |
Lean 4.15
Diffstat (limited to 'Day16.lean')
| -rw-r--r-- | Day16.lean | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |