Merge remote-tracking branch 'origin/master' into byAsSorry_fixes

src/Init/Data/Array/Attach.lean

@@ -251,7 +251,7 @@ theorem getElem?_attach {xs : Array α} {i : Nat} :
 theorem getElem_attachWith {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
     {i : Nat} (h : i < (xs.attachWith P H).size) :
     (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
-  getElem_pmap ..
+  getElem_pmap _ _ h
 
 @[simp]
 theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :

src/Init/Data/Int/DivModLemmas.lean

@@ -125,7 +125,7 @@ theorem eq_one_of_mul_eq_one_right {a b : Int} (H : 0 ≤ a) (H' : a * b = 1) :
   eq_one_of_dvd_one H ⟨b, H'.symm⟩
 
 theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
-  eq_one_of_mul_eq_one_right H <| by rw [Int.mul_comm, H']
+  eq_one_of_mul_eq_one_right (b := a) H <| by rw [Int.mul_comm, H']
 
 /-! ### *div zero  -/
 

src/Init/Data/List/BasicAux.lean

@@ -155,7 +155,8 @@ def mapMono (as : List α) (f : α → α) : List α :=
 
 /-! ## Additional lemmas required for bootstrapping `Array`. -/
 
-theorem getElem_append_left {as bs : List α} (h : i < as.length) {h'} : (as ++ bs)[i] = as[i] := by
+theorem getElem_append_left {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} :
+    (as ++ bs)[i] = as[i] := by
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>

src/Init/Data/List/Lemmas.lean

@@ -416,8 +416,9 @@ theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (n : Nat) (h : n
   | _, _ :: _, .head .. => ⟨0, Nat.succ_pos _, rfl⟩
   | _, _ :: _, .tail _ m => let ⟨n, h, e⟩ := getElem_of_mem m; ⟨n+1, Nat.succ_lt_succ h, e⟩
 
-theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a :=
-  let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
+theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a := by
+  let ⟨n, _, e⟩ := getElem_of_mem h
+  exact ⟨n, e ▸ getElem?_eq_getElem _⟩
 
 theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
@@ -949,7 +950,7 @@ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
   | _ :: _ :: _, _ => by
     simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]
 
-theorem getElem_length_sub_one_eq_getLast (l : List α) (h) :
+theorem getElem_length_sub_one_eq_getLast (l : List α) (h : l.length - 1 < l.length) :
     l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
   rw [← getLast_eq_getElem]
 
@@ -1077,7 +1078,8 @@ theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_p
   | nil => simp at h
   | cons _ _ => simp
 
-theorem getElem_zero_eq_head (l : List α) (h) : l[0] = head l (by simpa [length_pos] using h) := by
+theorem getElem_zero_eq_head (l : List α) (h : 0 < l.length) :
+    l[0] = head l (by simpa [length_pos] using h) := by
   cases l with
   | nil => simp at h
   | cons _ _ => simp
@@ -1669,7 +1671,7 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 @[simp] theorem cons_append_fun (a : α) (as : List α) :
     (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
 
-theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h) :
+theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h : n < (l₁ ++ l₂).length) :
     (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
   split <;> rename_i h'
   · rw [getElem_append_left h']
@@ -2867,7 +2869,7 @@ are often used for theorems about `Array.pop`.
 @[simp] theorem getElem_dropLast : ∀ (xs : List α) (i : Nat) (h : i < xs.dropLast.length),
     xs.dropLast[i] = xs[i]'(Nat.lt_of_lt_of_le h (length_dropLast .. ▸ Nat.pred_le _))
   | _::_::_, 0, _ => rfl
-  | _::_::_, i+1, _ => getElem_dropLast _ i _
+  | _::_::_, i+1, h => getElem_dropLast _ i (Nat.add_one_lt_add_one_iff.mp h)
 
 @[deprecated getElem_dropLast (since := "2024-06-12")]
 theorem get_dropLast (xs : List α) (i : Fin xs.dropLast.length) :

src/Init/Data/List/Sublist.lean

@@ -841,7 +841,7 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
 theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
     l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ x (hx : x < l₁.length),
       l₁[x] = l₂[x]'(Nat.lt_of_lt_of_le hx h) where
-  mp h := ⟨h.length_le, fun _ _ ↦ h.getElem _⟩
+  mp h := ⟨h.length_le, fun _ h' ↦ h.getElem h'⟩
   mpr h := by
     obtain ⟨hl, h⟩ := h
     induction l₂ generalizing l₁ with

src/Init/Data/List/TakeDrop.lean

@@ -65,13 +65,13 @@ theorem lt_length_of_take_ne_self {l : List α} {n} (h : l.take n ≠ l) : n < l
 theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length),
     l[i] :: drop (i + 1) l = drop i l
   | _::_, 0, _ => rfl
-  | _::_, i+1, _ => getElem_cons_drop _ i _
+  | _::_, i+1, h => getElem_cons_drop _ i (Nat.add_one_lt_add_one_iff.mp h)
 
 @[deprecated getElem_cons_drop (since := "2024-06-12")]
 theorem get_cons_drop (l : List α) (i) : get l i :: drop (i + 1) l = drop i l := by
   simp
 
-theorem drop_eq_getElem_cons {n} {l : List α} (h) : drop n l = l[n] :: drop (n + 1) l :=
+theorem drop_eq_getElem_cons {n} {l : List α} (h : n < l.length) : drop n l = l[n] :: drop (n + 1) l :=
   (getElem_cons_drop _ n h).symm
 
 @[deprecated drop_eq_getElem_cons (since := "2024-06-12")]

src/Init/Data/Nat/Dvd.lean

@@ -39,9 +39,9 @@ protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k
 protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by
   rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h
 
-theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m :=
-  have := Nat.dvd_add_iff_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
-  by rwa [mod_add_div] at this
+theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m := by
+  have := Nat.dvd_add_iff_left (m := m % n) <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
+  rwa [mod_add_div] at this
 
 theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n
   | ⟨k, e⟩ => by

src/Init/GetElem.lean

@@ -231,7 +231,7 @@ theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.leng
     as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl
-  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _
+  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) (Nat.add_one_lt_add_one_iff.mp h)
 
 @[deprecated getElem_cons_drop_succ_eq_drop (since := "2024-11-05")]
 abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop