Lean 4.21

4 files changed, 7 insertions, 7 deletions

diff --git a/Common/Function.lean b/Common/Function.lean
index f497baa..691a068 100644
--- a/Common/Function.lean
+++ b/Common/Function.lean
@@ -1,3 +1 @@
 theorem Function.comp_assoc (f : γ → δ) (g : β → γ) (h : α → β) : (f∘g)∘h = f∘g∘h := rfl
-theorem Function.comp_id (f : α → β) : f ∘ id = f := rfl
-theorem Function.id_comp (f : α → β) : id ∘ f = f := rfl
diff --git a/Day10.lean b/Day10.lean
index cea307b..6787658 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -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
diff --git a/lakefile.lean b/lakefile.lean
index 15276ee..e89dba4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -32,7 +32,7 @@ lean_exe «aoc-2023» where
   supportInterpreter := true
 
 require BinaryHeap from git
-  "http://git.grois.info/BinaryHeap"@"79f6af06385585087f08a7d77eb43d8674c16948"
+  "http://git.grois.info/BinaryHeap"@"ff5c64836ede27d87dbc56b3869021ad8b0d255b"
 
 require «lean-astar» from git
-  "http://git.grois.info/lean-astar"@"eebf50562af5de9779aa11ab2671bc1c917e6000"
+  "http://git.grois.info/lean-astar"@"2539ac49ab6af74b31d91e03d7dbfceedc9c1f02"
diff --git a/lean-toolchain b/lean-toolchain
index 6c721df..893a7f3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.20.1
+leanprover/lean4:4.21.0