Trigger CI for leanprover/lean4#3714

Batteries/Data/Fin/Lemmas.lean

@@ -9,10 +9,6 @@ namespace Fin
 
 attribute [norm_cast] val_last
 
-/-! ### last -/
-
-@[simp] theorem last_zero : last 0 = 0 := rfl
-
 /-! ### clamp -/
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl

Batteries/Data/List/Lemmas.lean

@@ -590,37 +590,6 @@ theorem insertP_loop (a : α) (l r : List α) :
   induction l with simp [insertP, insertP.loop, cond]
   | cons _ _ ih => split <;> simp [insertP_loop, ih]
 
-/-! ### merge -/
-
-theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
-    merge (a::l) (b::r) s = if s a b then a :: merge l (b::r) s else b :: merge (a::l) r s := by
-  simp only [merge]
-
-@[simp] theorem cons_merge_cons_pos (s : α → α → Bool) (l r) (h : s a b) :
-    merge (a::l) (b::r) s = a :: merge l (b::r) s := by
-  rw [cons_merge_cons, if_pos h]
-
-@[simp] theorem cons_merge_cons_neg (s : α → α → Bool) (l r) (h : ¬ s a b) :
-    merge (a::l) (b::r) s = b :: merge (a::l) r s := by
-  rw [cons_merge_cons, if_neg h]
-
-@[simp] theorem length_merge (s : α → α → Bool) (l r) :
-    (merge l r s).length = l.length + r.length := by
-  match l, r with
-  | [], r => simp
-  | l, [] => simp
-  | a::l, b::r =>
-    rw [cons_merge_cons]
-    split
-    · simp_arith [length_merge s l (b::r)]
-    · simp_arith [length_merge s (a::l) r]
-
-theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge l r s :=
-  mem_merge.2 <| .inl h
-
-theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge l r s :=
-  mem_merge.2 <| .inr h
-
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :

Batteries/Lean/HashSet.lean

@@ -54,7 +54,7 @@ instance : BEq (HashSet α) where
 `O(1)` amortized. Similar to `insert`, but also returns a Boolean flag indicating whether an
 existing entry has been replaced with `a => b`.
 -/
-@[inline]
+@[inline, deprecated containsThenInsert (since := "2024-09-17")]
 def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
   let oldSize := s.size
   let s := s.insert a

test/lint_lean.lean

@@ -15,14 +15,13 @@ but it is useful to run locally to see what the linters would catch.
 -- attribute [nolint dupNamespace] Lean.Elab.Tactic.Tactic
 -- attribute [nolint dupNamespace] Lean.Parser.Parser Lean.Parser.Parser.rec Lean.Parser.Parser.mk
 --   Lean.Parser.Parser.info Lean.Parser.Parser.fn
+-- attribute [nolint explicitVarsOfIff] Iff.refl
 
 /-! Failing lints that need work. -/
 
--- #lint only explicitVarsOfIff in all -- Found 156 errors
-
--- Many fixed in https://github.com/leanprover/lean4/pull/4620
+-- Many fixed in https://github.com/leanprover/lean4/pull/4620 and subsequent PRs
 -- and should be checked again.
--- #lint only simpNF in all -- Found 12 errors
+-- #lint only simpNF in all -- Found 22 errors
 
 /-! Lints that fail, but that we're not intending to do anything about. -/
 
@@ -41,6 +40,7 @@ but it is useful to run locally to see what the linters would catch.
 
 /-! Lints that have succeeded in the past, and hopefully still do! -/
 
+-- #lint only explicitVarsOfIff in all -- Found 1 errors, `Iff.refl`, which could be nolinted.
 -- #lint only impossibleInstance  in all -- Found 0 errors
 -- #lint only simpVarHead in all -- Found 0 error
 -- #lint only unusedHavesSuffices in all  -- Found 0 errors