chore: clear remaining nightly build warnings

* `AlternatingFaceMapComplex`: `not_lt_zero'` deprecated, use `not_lt_zero`.
* `Finsupp/Single`: `Finsupp.support_single_ne_zero` deprecated, use the
  unprimed `Finsupp.support_single`.
* `Probability/Independence/Basic`: drop the `beta_reduce` step that no
  longer fires.
* `MeasureSpace.eq_zero_of_isEmpty` and `VectorMeasure.eq_zero_of_isEmpty`:
  these are `@[nontriviality]` (a scoped simp set), so the new
  `warning.simp.varHead` lint about `μ` being a variable LHS is exactly
  the "acceptable for scoped simp lemmas" case — suppress per-declaration.
* `Over.mapId` / `Under.mapId`: the outer `variable
  [P.IsStableUnderComposition]` is redundant with the per-decl
  `[P.IsMultiplicative]`, but is needed by the surrounding `Over.map`
  / `Under.map` declarations. Suppress the
  `linter.overlappingInstances` lint on the two `mapId` definitions.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: kim-em

Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -101,7 +101,7 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'
     refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
     · rintro rfl
-      simp only [Fin.val_zero, not_lt_zero'] at hij'
+      simp only [Fin.val_zero, not_lt_zero] at hij'
     · simpa [S] using! Nat.le_sub_one_of_lt hij'
     · simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]
   · -- identification of corresponding terms in both sums

Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

@@ -58,6 +58,7 @@ def Over.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
   NatIso.ofComponents (fun Y ↦ Over.isoMk (Iso.refl _))
 
 set_option backward.defeqAttrib.useBackward true in
+set_option linter.overlappingInstances false in
 /-- `Over.map` preserves identities. -/
 @[simps!]
 def Over.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)
@@ -237,6 +238,7 @@ def Under.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
   NatIso.ofComponents (fun Y ↦ Under.isoMk (Iso.refl _))
 
 set_option backward.defeqAttrib.useBackward true in
+set_option linter.overlappingInstances false in
 /-- `Under.map` preserves identities. -/
 @[simps!]
 def Under.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)

Mathlib/Data/Finsupp/Single.lean

@@ -162,7 +162,7 @@ lemma apply_surjective (a : α) : Surjective fun f : α →₀ M ↦ f a :=
   RightInverse.surjective fun _ ↦ single_eq_same
 
 theorem support_single_ne_bot (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥ := by
-  simpa only [support_single_ne_zero _ h] using! singleton_ne_empty _
+  simpa only [support_single _ h] using! singleton_ne_empty _
 
 theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
     Disjoint (single i b).support (single j b').support ↔ i ≠ j := by

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -853,6 +853,7 @@ lemma apply_eq_zero_of_isEmpty [IsEmpty α] {_ : MeasurableSpace α} (μ : Measu
 instance instSubsingleton [IsEmpty α] {m : MeasurableSpace α} : Subsingleton (Measure α) :=
   ⟨fun μ ν => by ext1 s _; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
 
+set_option warning.simp.varHead false in
 @[nontriviality]
 theorem eq_zero_of_isEmpty [IsEmpty α] {_m : MeasurableSpace α} (μ : Measure α) : μ = 0 :=
   Subsingleton.elim μ 0

Mathlib/MeasureTheory/VectorMeasure/Basic.lean

@@ -290,6 +290,7 @@ lemma apply_eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) (s : Set 
 instance [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
   ⟨fun μ ν => by ext; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
 
+set_option warning.simp.varHead false in
 @[nontriviality]
 theorem eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) : μ = 0 :=
   Subsingleton.elim μ 0

Mathlib/Probability/Independence/Basic.lean

@@ -877,7 +877,7 @@ theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
       simp
   intro h S s hs
   specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
-    fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
+    fun i ↦ by split_ifs with hiS <;> simp [hiS, hs]
   simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
     Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
     Measure.pi_pi] at h₀