Day 5 of #AdventofCode in Lean: https://github.com/chenson2018/advent-of-code/blob/main/2024/lean/AoC/Day05.lean

One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.