diff options
Diffstat (limited to 'Day10.lean')
| -rw-r--r-- | Day10.lean | 6 |
1 files changed, 4 insertions, 2 deletions
@@ -440,13 +440,14 @@ private theorem Except.get_pure {α : Type u1} (ε : Type u2) (v : α) : Except. private theorem Array.getElem!_eq_getElem {α : Type u} [Inhabited α] {a : Array α} {index : Nat} (h : index < a.size ): a[index] = a[index]! := by unfold getElem getElem! Array.instGetElemNatLtSize Array.instGetElem?NatLtSize Array.get!Internal Array.getInternal Array.getD - simp + simp only split <;> rfl private theorem Array.get_push {α : Type u} (arr : Array α) (v : α) (index : Nat) (h₁ : index < arr.size) : arr[index] = (arr.push v)[index]'(by simp[Nat.lt_succ.mpr (Nat.le_of_lt h₁)]) := by cases arr unfold Array.push getElem Array.instGetElemNatLtSize + simp only [List.size_toArray] at h₁ simp[List.getElem_append, h₁] private theorem Area.ParseLine_leaves_start_if_some (previous : Area.Raw) (pos : Nat) (line : Substring) (h₁ : previous.height > 0) {res : (Nat × Area.Raw)} (h₂ : (Area.parseLine previous pos line h₁) = Except.ok res) (h₃ : previous.start.isSome) : Fin.val <$> res.2.start = Fin.val <$> previous.start := by @@ -516,7 +517,8 @@ private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) ( case isFalse h₇ => have h₈ : (previous.fields.push t)[previous.width * (previous.height - 1) + pos]! = t := by have : (previous.fields.push t)[previous.fields.size] = t := Array.getElem_push_eq - simp[h₂, Array.getElem!_eq_getElem] at this + simp[h₂] at this + rw[Array.getElem!_eq_getElem] at this assumption have : t = Tile.start := beq_iff_eq.mp h₆ subst t |