chore: adapt to by mvars restriction

Kha · Kha · commit 3fe3eeb2c32a · 2025-05-28T17:41:33.000+02:00
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -3179,7 +3179,7 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
   · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
-@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
+@[simp] theorem getElem_concat_zero (x : BitVec w) : (concat x b)[0] = b := by
   simp [getElem_concat]
 
 theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean
@@ -184,8 +184,9 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
     rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
     conv => rhs; rw [←bind_pure (f 0 x)]
     congr
-    funext
-    simp [foldrM_loop_zero]
+    try  -- TODO: block can be deleted after bootstrapping
+      funext
+      simp [foldrM_loop_zero]
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..
diff --git a/src/Init/Data/List/Nat/Pairwise.lean b/src/Init/Data/List/Nat/Pairwise.lean
@@ -55,7 +55,7 @@ theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (F
     simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ']
 
 set_option linter.listVariables false in
-theorem pairwise_iff_getElem : Pairwise R l ↔
+theorem pairwise_iff_getElem (l : List α) : Pairwise R l ↔
     ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
   rw [pairwise_iff_forall_sublist]
   constructor <;> intro h
diff --git a/src/Init/Data/List/Nat/Sublist.lean b/src/Init/Data/List/Nat/Sublist.lean
@@ -30,7 +30,7 @@ theorem IsSuffix.getElem {xs ys : List α} (h : xs <:+ ys) {i} (hn : i < xs.leng
   have := h.length_le
   omega
 
-theorem suffix_iff_getElem? : l₁ <:+ l₂ ↔
+theorem suffix_iff_getElem? (l₁ l₂ : List α) : l₁ <:+ l₂ ↔
     l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] := by
   suffices l₁.length ≤ l₂.length ∧ l₁ <:+ l₂ ↔
       l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] by
@@ -78,7 +78,7 @@ theorem suffix_iff_getElem {l₁ l₂ : List α} :
     rw [getElem?_eq_getElem]
     simpa using w
 
-theorem infix_iff_getElem? : l₁ <:+: l₂ ↔
+theorem infix_iff_getElem? (l₁ l₂ : List α) : l₁ <:+: l₂ ↔
     ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + k]? = some l₁[i] := by
   constructor
   · intro h
diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean
@@ -153,12 +153,12 @@ where
     mergeTR (run' r) (run l) le
 
 theorem splitRevInTwo'_fst (l : { l : List α // l.length = n }) :
-    (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩ := by
+    (splitRevInTwo' l).1 = ⟨(splitInTwo (n := n) ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩ := by
   simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_snd]
   congr
   omega
 theorem splitRevInTwo'_snd (l : { l : List α // l.length = n }) :
-    (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩ := by
+    (splitRevInTwo' l).2 = ⟨(splitInTwo (n := n) ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩ := by
   simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_fst, reverse_reverse]
   congr 2
   simp
diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean
@@ -905,7 +905,8 @@ theorem infix_concat_iff {l₁ l₂ : List α} {a : α} :
   rw [← reverse_infix, reverse_concat, infix_cons_iff, reverse_infix,
     ← reverse_prefix, reverse_concat]
 
-theorem prefix_iff_getElem? : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
+theorem prefix_iff_getElem? (l₁ l₂ : List α) :
+    l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
   induction l₁ generalizing l₂ with
   | nil => simp
   | cons a l₁ ih =>
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
@@ -1767,8 +1767,10 @@ instance decidableExistsLT' {p : (m : Nat) → m < k → Prop} [I : ∀ m h, Dec
 /-- Dependent version of `decidableExistsLE`. -/
 instance decidableExistsLE' {p : (m : Nat) → m ≤ k → Prop} [I : ∀ m h, Decidable (p m h)] :
     Decidable (∃ m : Nat, ∃ h : m ≤ k, p m h) :=
-  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) (exists_congr fun _ =>
-    ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩)
+  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) <| by
+    apply exists_congr
+    intro
+    exact ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩
 
 /-! ### Results about `List.sum` specialized to `Nat` -/
 
