From b1179d5cc3f0f32af026b444430fc885b29e873b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 16 Sep 2024 13:28:14 +1000
Subject: [PATCH] chore: fix implicitness of List.getElem_mem (#5331)

---
 src/Init/Data/List/Attach.lean | 6 +++---
 src/Init/Data/List/Lemmas.lean | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 76c16eefdc..0a3b83f0ba 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -235,7 +235,7 @@ theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
     (hn : n < (pmap f l h).length) :
     (pmap f l h)[n] =
       f (l[n]'(@length_pmap _ _ p f l h ▸ hn))
-        (h _ (getElem_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
+        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
   induction l generalizing n with
   | nil =>
     simp only [length, pmap] at hn
@@ -266,12 +266,12 @@ theorem getElem?_attach {xs : List α} {i : Nat} :
 @[simp]
 theorem getElem_attachWith {xs : List α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
     {i : Nat} (h : i < (xs.attachWith P H).length) :
-    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem xs i (by simpa using h))⟩ :=
+    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
   getElem_pmap ..
 
 @[simp]
 theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
-    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem xs i (by simpa using h)⟩ :=
+    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
 @[simp] theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 89c76cb928..1598ae582d 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -483,9 +483,9 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
-theorem getElem_mem : ∀ (l : List α) n (h : n < l.length), l[n]'h ∈ l
+theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
   | _ :: _, 0, _ => .head ..
-  | _ :: l, _+1, _ => .tail _ (getElem_mem l ..)
+  | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
 theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
   | _ :: _, 0, _ => .head ..
@@ -527,7 +527,7 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
       · simpa
       · apply w
         simp only [getElem_cons_succ]
-        exact getElem_mem l n (lt_of_succ_lt_succ h)
+        exact getElem_mem (lt_of_succ_lt_succ h)
 
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by