Lean 4.19

1 files changed, 3 insertions, 3 deletions

diff --git a/Common/List.lean b/Common/List.lean
index 1c8f4a6..f6c0de5 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -54,7 +54,7 @@ instance {α : Type} [Ord α] : Ord (List α) where
 def not_empty_iff_size_gt_zero {list : List α} : list.isEmpty = false ↔ list.length > 0 :=
   match list with
   | [] => ⟨nofun, nofun⟩
-  | l :: ls => ⟨λ_ ↦ (List.length_cons l ls).substr (Nat.succ_pos ls.length), λ_ => rfl⟩
+  | _l :: ls => ⟨λ_ ↦ (List.length_cons).substr (Nat.succ_pos ls.length), λ_ => rfl⟩
 
 def ne_nil_of_not_empty {list : List α} : list.isEmpty = false ↔ list ≠ [] :=
   match list with
@@ -79,14 +79,14 @@ where
   | [], _, bs => bs.reverse
   | a :: as, f, bs =>
     let g : (e : α) → (e ∈ as) → β := λ e h ↦ f e (List.mem_cons_of_mem a h)
-    worker as g (f a (List.mem_cons_self _ _) :: bs)
+    worker as g (f a (List.mem_cons_self) :: bs)
 
 protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : List α) (f : (e : α) → (e ∈ list) → β) (acc : List β) : list.length + acc.length = (List.mapWithProof.worker list f acc).length := by
   induction list generalizing acc
   case nil => unfold mapWithProof.worker; simp only [length_nil, Nat.zero_add, length_reverse]
   case cons l ls hi =>
     unfold mapWithProof.worker
-    have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self _ _) :: acc)
+    have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self) :: acc)
     simp +arith[←hi]
 
 theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length :=