chore: update batteries dependency (including fixes for batteries#1220) (#25478)

kim-em · jcommelin · leanprover-community-mathlib4-bot · kim-em · commit 6437a62646ab · 2025-06-05T23:26:55.000Z
Co-authored-by: Johan Commelin &lt;johan@commelin.net&gt;
Co-authored-by: leanprover-community-mathlib4-bot &lt;leanprover-community-mathlib4-bot@users.noreply.github.com&gt;
Co-authored-by: Jovan Gerbscheid &lt;jovan.gerbscheid@gmail.com&gt;
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@@ -72,7 +72,7 @@ theorem prod_pair [DecidableEq ι] {a b : ι} (h : a ≠ b) :
 
 @[to_additive (attr := simp)]
 theorem prod_image [DecidableEq ι] {s : Finset κ} {g : κ → ι} :
-    (∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) :=
+    Set.InjOn g s → ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) :=
   fold_image
 
 @[to_additive]
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean
@@ -26,7 +26,7 @@ lemma prod_preimage' (f : ι → κ) [DecidablePred (· ∈ Set.range f)] (s : F
   classical
   calc
     ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
-      Eq.symm <| prod_image <| by simpa only [mem_preimage, Set.InjOn] using hf
+      Eq.symm <| prod_image <| by simpa [mem_preimage, Set.InjOn] using hf
     _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]
 
 @[to_additive]
diff --git a/Mathlib/Algebra/BigOperators/Intervals.lean b/Mathlib/Algebra/BigOperators/Intervals.lean
@@ -147,7 +147,7 @@ theorem prod_Ico_reflect (f : ℕ → M) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1)
   rcases lt_or_le k m with hkm | hkm
   · rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
     refine (prod_image ?_).symm
-    simp only [mem_Ico]
+    simp only [mem_Ico, Set.InjOn, mem_coe]
     rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
     rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
   · have : n + 1 - k ≤ n + 1 - m := by
diff --git a/Mathlib/Algebra/Group/Submonoid/Basic.lean b/Mathlib/Algebra/Group/Submonoid/Basic.lean
@@ -302,7 +302,7 @@ theorem disjoint_def' {p₁ p₂ : Submonoid M} :
 
 variable {t : Set M}
 
-@[to_additive (attr := simp)]
+@[to_additive] -- this must not be a simp-lemma as the conclusion applies to `hts`, causing loops
 lemma closure_sdiff_eq_closure (hts : t ⊆ closure (s \ t)) : closure (s \ t) = closure s := by
   refine (closure_mono Set.diff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_
   by_cases hxt : x ∈ t
diff --git a/Mathlib/Algebra/GroupWithZero/Basic.lean b/Mathlib/Algebra/GroupWithZero/Basic.lean
@@ -262,14 +262,14 @@ theorem GroupWithZero.mul_left_injective (h : x ≠ 0) :
     Function.Injective fun y => y * x := fun y y' w => by
   simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_right`
 theorem inv_mul_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b⁻¹ * b = a :=
   calc
     a * b⁻¹ * b = a * (b⁻¹ * b) := mul_assoc _ _ _
     _ = a := by simp [h]
 
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_left`
 theorem inv_mul_cancel_left₀ (h : a ≠ 0) (b : G₀) : a⁻¹ * (a * b) = b :=
   calc
     a⁻¹ * (a * b) = a⁻¹ * a * b := (mul_assoc _ _ _).symm
diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -205,7 +205,7 @@ variable [GroupWithZero G₀] {a : G₀}
 
 @[simp] lemma inv_zero : (0 : G₀)⁻¹ = 0 := GroupWithZero.inv_zero
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel`
 lemma mul_inv_cancel₀ (h : a ≠ 0) : a * a⁻¹ = 1 := GroupWithZero.mul_inv_cancel a h
 
 -- See note [lower instance priority]
@@ -232,13 +232,13 @@ section GroupWithZero
 
 variable [GroupWithZero G₀] {a b : G₀}
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_right`
 theorem mul_inv_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a :=
   calc
     a * b * b⁻¹ = a * (b * b⁻¹) := mul_assoc _ _ _
     _ = a := by simp [h]
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_left`
 theorem mul_inv_cancel_left₀ (h : a ≠ 0) (b : G₀) : a * (a⁻¹ * b) = b :=
   calc
     a * (a⁻¹ * b) = a * a⁻¹ * b := (mul_assoc _ _ _).symm
diff --git a/Mathlib/Algebra/GroupWithZero/NeZero.lean b/Mathlib/Algebra/GroupWithZero/NeZero.lean
@@ -48,7 +48,7 @@ theorem inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 := fun a_eq_0 => by
   have := mul_inv_cancel₀ h
   simp only [a_eq_0, mul_zero, zero_ne_one] at this
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.inv_mul_cancel`
 theorem inv_mul_cancel₀ (h : a ≠ 0) : a⁻¹ * a = 1 :=
   calc
     a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ := by simp [inv_ne_zero h]
diff --git a/Mathlib/Algebra/Homology/DifferentialObject.lean b/Mathlib/Algebra/Homology/DifferentialObject.lean
@@ -41,14 +41,18 @@ abbrev objEqToHom {i j : β} (h : i = j) :
 theorem objEqToHom_refl (i : β) : X.objEqToHom (refl i) = 𝟙 _ :=
   rfl
 
-@[reassoc (attr := simp)]
+-- Removing `@[simp]`, because it is in the opposite direction of `eqToHom_naturality`.
+-- Having both causes an infinite loop in the simpNF linter.
+@[reassoc]
 theorem objEqToHom_d {x y : β} (h : x = y) :
     X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom (by cases h; rfl) := by cases h; simp
 
 @[reassoc (attr := simp)]
 theorem d_squared_apply {x : β} : X.d x ≫ X.d _ = 0 := congr_fun X.d_squared _
 
-@[reassoc (attr := simp)]
+-- Removing `@[simp]`, because it is in the opposite direction of `eqToHom_naturality`.
+-- Having both causes an infinite loop in the simpNF linter.
+@[reassoc]
 theorem eqToHom_f' {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}
     (h : x = y) : X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h := by cases h; simp
 
@@ -79,7 +83,7 @@ def dgoToHomologicalComplex :
       shape := fun i j w => by dsimp at w; convert dif_neg w
       d_comp_d' := fun i j k hij hjk => by
         dsimp at hij hjk; substs hij hjk
-        simp }
+        simp [objEqToHom_d_assoc] }
   map {X Y} f :=
     { f := f.f
       comm' := fun i j h => by
diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean
@@ -177,10 +177,15 @@ lemma slope_of_Y_eq {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ = W.
   rw [slope, if_pos hx, if_pos hy]
 
 @[simp]
+lemma slope_of_Y_ne' {x₂ y₁ y₂ : F} (hy : ¬y₁ = -y₂ - W.a₁ * x₂ - W.a₃) :
+    W.slope x₂ x₂ y₁ y₂ =
+      (3 * x₂ ^ 2 + 2 * W.a₂ * x₂ + W.a₄ - W.a₁ * y₁) / (y₁ - (-y₁ - W.a₁ * x₂ - W.a₃)) := by
+  simp [slope, hy]
+
 lemma slope_of_Y_ne {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
     W.slope x₁ x₂ y₁ y₂ =
       (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) := by
-  rw [slope, if_pos hx, if_neg hy]
+  simp_all
 
 @[simp]
 lemma slope_of_X_ne {x₁ x₂ y₁ y₂ : F} (hx : x₁ ≠ x₂) :
diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
@@ -544,7 +544,7 @@ lemma add_of_Y_eq {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h
     (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) : some h₁ + some h₂ = 0 := by
   simpa only [add_def, add] using dif_pos ⟨hx, hy⟩
 
-@[simp]
+-- Removing `@[simp]`, because `hy` causes a maximum recursion depth error in the simpNF linter.
 lemma add_self_of_Y_eq {x₁ y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ = W.negY x₁ y₁) :
     some h₁ + some h₁ = 0 :=
   add_of_Y_eq rfl hy
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean b/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
@@ -57,7 +57,7 @@ The difference between the characteristic functions of `f` and `f - const` simpl
 difference between the proximity functions.
 -/
 @[simp]
-lemma characteristic_sub_characteristic_eq_proximity_sub_proximity (h : MeromorphicOn f ⊤)
+lemma characteristic_sub_characteristic_eq_proximity_sub_proximity (h : MeromorphicOn f Set.univ)
     (a₀ : E) :
     characteristic f ⊤ - characteristic (f · - a₀) ⊤ = proximity f ⊤ - proximity (f · - a₀) ⊤ := by
   rw [(by rfl : (f · - a₀) = f - fun _ ↦ a₀)]
diff --git a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean
@@ -292,7 +292,7 @@ end LinearMap
 
 section Nonneg
 
-@[simp]
+-- Cannot be @[simp] because the LHS is not in simp normal form
 theorem inner_product_apply_eigenvector {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E}
     (h : T v = μ • v) : ⟪v, T v⟫ = μ * (‖v‖ : 𝕜) ^ 2 := by
   simp only [h, inner_smul_right, inner_self_eq_norm_sq_to_K]
diff --git a/Mathlib/Data/Finset/Fold.lean b/Mathlib/Data/Finset/Fold.lean
@@ -60,7 +60,7 @@ theorem fold_map {g : γ ↪ α} {s : Finset γ} : (s.map g).fold op b f = s.fol
 
 @[simp]
 theorem fold_image [DecidableEq α] {g : γ → α} {s : Finset γ}
-    (H : ∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) : (s.image g).fold op b f = s.fold op b (f ∘ g) := by
+    (H : Set.InjOn g s) : (s.image g).fold op b f = s.fold op b (f ∘ g) := by
   simp only [fold, image_val_of_injOn H, Multiset.map_map]
 
 @[congr]
diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
@@ -559,7 +559,6 @@ theorem filterMap_mono (h : s ⊆ t) :
   rw [← val_le_iff] at h ⊢
   exact Multiset.filterMap_le_filterMap f h
 
-@[simp]
 theorem _root_.List.toFinset_filterMap [DecidableEq α] [DecidableEq β]
     (f_inj : ∀ (a a' : α) (b : β), f a = some b → f a' = some b → a = a') (s : List α) :
     (s.filterMap f).toFinset = s.toFinset.filterMap f f_inj := by
diff --git a/Mathlib/Data/Int/Init.lean b/Mathlib/Data/Int/Init.lean
@@ -307,7 +307,16 @@ lemma sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign
 
 /-! ### toNat -/
 
-@[simp] lemma toNat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.toNat - 1 : ℕ) : ℤ) = i - 1 := by
+/-
+The following lemma is non-confluent with
+```
+simp only [*, @Int.lt_toNat, CharP.cast_eq_zero, @Nat.cast_pred, Int.ofNat_toNat]
+```
+from the default simp set, which simplifies the LHS to `max i 0 - 1`.
+Therefore we mark this lemma as `@[simp high]`.
+-/
+@[simp high]
+lemma toNat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.toNat - 1 : ℕ) : ℤ) = i - 1 := by
   simp only [lt_toNat, Int.cast_ofNat_Int, h, natCast_pred_of_pos, Int.le_of_lt h, toNat_of_nonneg]
 
 lemma toNat_lt_of_ne_zero {n : ℕ} (hn : n ≠ 0) : m.toNat < n ↔ m < n := by omega
diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -63,7 +63,6 @@ lemma prod_primeFactors_prod_factorization {β : Type*} [CommMonoid β] (f : ℕ
 
 
 /-- The multiplicity of prime `p` in `p` is `1` -/
-@[simp]
 theorem Prime.factorization_self {p : ℕ} (hp : Prime p) : p.factorization p = 1 := by simp [hp]
 
 /-- If the factorization of `n` contains just one number `p` then `n` is a power of `p` -/
@@ -88,15 +87,13 @@ theorem factorizationEquiv_inv_apply {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.supp
     (factorizationEquiv.symm ⟨f, hf⟩).1 = f.prod (· ^ ·) :=
   rfl
 
-@[simp]
 theorem ordProj_of_not_prime (n p : ℕ) (hp : ¬p.Prime) : ordProj[p] n = 1 := by
-  simp [factorization_eq_zero_of_non_prime n hp]
+  simp [hp]
 
 @[deprecated (since := "2024-10-24")] alias ord_proj_of_not_prime := ordProj_of_not_prime
 
-@[simp]
 theorem ordCompl_of_not_prime (n p : ℕ) (hp : ¬p.Prime) : ordCompl[p] n = n := by
-  simp [factorization_eq_zero_of_non_prime n hp]
+  simp [hp]
 
 @[deprecated (since := "2024-10-24")] alias ord_compl_of_not_prime := ordCompl_of_not_prime
 
diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
@@ -249,6 +249,9 @@ theorem injOn_singleton (f : α → β) (a : α) : InjOn f {a} :=
 
 @[simp] lemma injOn_pair {b : α} : InjOn f {a, b} ↔ f a = f b → a = b := by unfold InjOn; aesop
 
+@[simp low] lemma injOn_of_eq_iff_eq (s : Set α) (h : ∀ x y, f x = f y ↔ x = y) : Set.InjOn f s :=
+  fun x _ y _ => (h x y).mp
+
 theorem InjOn.eq_iff {x y} (h : InjOn f s) (hx : x ∈ s) (hy : y ∈ s) : f x = f y ↔ x = y :=
   ⟨h hx hy, fun h => h ▸ rfl⟩
 
diff --git a/Mathlib/Data/Vector/MapLemmas.lean b/Mathlib/Data/Vector/MapLemmas.lean
@@ -290,21 +290,22 @@ If an accumulation function `f`, produces the same output bits regardless of acc
 then the state is redundant and can be optimized out.
 -/
 @[simp]
-theorem mapAccumr_eq_map_of_unused_state (f : α → σ → σ × β) (s : σ)
-    (h : ∀ a s s', (f a s).snd = (f a s').snd) :
-    (mapAccumr f xs s).snd = (map (fun x => (f x s).snd) xs) :=
-  mapAccumr_eq_map (fun _ => true) rfl (fun _ _ _ => rfl) (fun a s s' _ _ => h a s s')
+theorem mapAccumr_eq_map_of_unused_state (f : α → σ → σ × β) (f' : α → β) (s : σ)
+    (h : ∀ a s, (f a s).snd = f' a) :
+    (mapAccumr f xs s).snd = (map f' xs) := by
+  rw [mapAccumr_eq_map (fun _ => true) rfl (fun _ _ _ => rfl) (fun a s s' _ _ => by rw [h, h])]
+  simp_all
 
 
 /--
 If an accumulation function `f`, produces the same output bits regardless of accumulation state,
 then the state is redundant and can be optimized out.
 -/
 @[simp]
-theorem mapAccumr₂_eq_map₂_of_unused_state (f : α → β → σ → σ × γ) (s : σ)
-    (h : ∀ a b s s', (f a b s).snd = (f a b s').snd) :
+theorem mapAccumr₂_eq_map₂_of_unused_state (f : α → β → σ → σ × γ) (f' : α → β → γ) (s : σ)
+    (h : ∀ a b s, (f a b s).snd = f' a b) :
     (mapAccumr₂ f xs ys s).snd = (map₂ (fun x y => (f x y s).snd) xs ys) :=
-  mapAccumr₂_eq_map₂ (fun _ => true) rfl (fun _ _ _ _ => rfl) (fun a b s s' _ _ => h a b s s')
+  mapAccumr₂_eq_map₂ (fun _ => true) rfl (fun _ _ _ _ => rfl) (fun a b s s' _ _ => by rw [h, h])
 
 
 /-- If `f` takes a pair of states, but always returns the same value for both elements of the
@@ -346,9 +347,9 @@ If `f` returns the same output and next state for every value of it's first argu
 `xs : Vector` is ignored, and we can rewrite `mapAccumr₂` into `map`.
 -/
 @[simp]
-theorem mapAccumr₂_unused_input_left [Inhabited α] (f : α → β → σ → σ × γ)
-    (h : ∀ a b s, f default b s = f a b s) :
-    mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s := by
+theorem mapAccumr₂_unused_input_left (f : α → β → σ → σ × γ) (f' : β → σ → σ × γ)
+    (h : ∀ a b s, f a b s = f' b s) :
+    mapAccumr₂ f xs ys s = mapAccumr f' ys s := by
   induction xs, ys using Vector.revInductionOn₂ generalizing s with
   | nil => rfl
   | snoc xs ys x y ih => simp [h x y s, ih]
@@ -358,9 +359,9 @@ If `f` returns the same output and next state for every value of it's second arg
 `ys : Vector` is ignored, and we can rewrite `mapAccumr₂` into `map`.
 -/
 @[simp]
-theorem mapAccumr₂_unused_input_right [Inhabited β] (f : α → β → σ → σ × γ)
-    (h : ∀ a b s, f a default s = f a b s) :
-    mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s := by
+theorem mapAccumr₂_unused_input_right (f : α → β → σ → σ × γ) (f' : α → σ → σ × γ)
+    (h : ∀ a b s, f a b s = f' a s) :
+    mapAccumr₂ f xs ys s = mapAccumr f' xs s := by
   induction xs, ys using Vector.revInductionOn₂ generalizing s with
   | nil => rfl
   | snoc xs ys x y ih => simp [h x y s, ih]
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
@@ -1221,13 +1221,14 @@ section AddGroup
 variable {α : Type*} [AddGroup α] {n : ℕ}
 
 @[simp]
-lemma nsmul_zmod_val_inv_nsmul (hn : (Nat.card α).Coprime n) (a : α) :
+lemma nsmul_zmod_val_inv_nsmul (hn : (Nat.card α).gcd n = 1) (a : α) :
     n • (n⁻¹ : ZMod (Nat.card α)).val • a = a := by
+  replace hn : (Nat.card α).Coprime n := hn
   rw [← mul_nsmul', ← mod_natCard_nsmul, ← ZMod.val_natCast, Nat.cast_mul,
     ZMod.mul_val_inv hn.symm, ZMod.val_one_eq_one_mod, mod_natCard_nsmul, one_nsmul]
 
 @[simp]
-lemma zmod_val_inv_nsmul_nsmul (hn : (Nat.card α).Coprime n) (a : α) :
+lemma zmod_val_inv_nsmul_nsmul (hn : (Nat.card α).gcd n = 1) (a : α) :
     (n⁻¹ : ZMod (Nat.card α)).val • n • a = a := by
   rw [nsmul_left_comm, nsmul_zmod_val_inv_nsmul hn]
 
@@ -1238,13 +1239,14 @@ variable {α : Type*} [Group α] {n : ℕ}
 
 -- TODO: we can't use `to_additive`, because it tries to translate `n⁻¹` into `-n`
 @[simp]
-lemma pow_zmod_val_inv_pow (hn : (Nat.card α).Coprime n) (a : α) :
+lemma pow_zmod_val_inv_pow (hn : (Nat.card α).gcd n = 1) (a : α) :
     (a ^ (n⁻¹ : ZMod (Nat.card α)).val) ^ n = a := by
+  replace hn : (Nat.card α).Coprime n := hn
   rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
     ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
 
 @[simp]
-lemma pow_pow_zmod_val_inv (hn : (Nat.card α).Coprime n) (a : α) :
+lemma pow_pow_zmod_val_inv (hn : (Nat.card α).gcd n = 1) (a : α) :
     (a ^ n) ^ (n⁻¹ : ZMod (Nat.card α)).val = a := by rw [pow_right_comm, pow_zmod_val_inv_pow hn]
 
 end Group
diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -545,7 +545,7 @@ theorem map_one {f : ArithmeticFunction R} (h : f.IsMultiplicative) : f 1 = 1 :=
 
 @[simp]
 theorem map_mul_of_coprime {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ}
-    (h : m.Coprime n) : f (m * n) = f m * f n :=
+    (h : m.gcd n = 1) : f (m * n) = f m * f n :=
   hf.2 h
 
 end MonoidWithZero
@@ -560,7 +560,7 @@ theorem map_prod {ι : Type*} [CommMonoidWithZero R] (g : ι → ℕ) {f : Arith
     | insert _ _ has ih =>
       rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs
       rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
-      exact .prod_right fun i hi => hs.2 _ hi (hi.ne_of_notMem has).symm
+      exact Coprime.prod_right fun i hi => hs.2 _ hi (hi.ne_of_notMem has).symm
 
 theorem map_prod_of_prime [CommMonoidWithZero R] {f : ArithmeticFunction R}
     (h_mult : ArithmeticFunction.IsMultiplicative f)
diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean
@@ -584,7 +584,7 @@ theorem prod_div_divisors {α : Type*} [CommMonoid α] (n : ℕ) (f : ℕ → α
   rw [← prod_image]
   · exact prod_congr (image_div_divisors_eq_divisors n) (by simp)
   · intro x hx y hy h
-    rw [mem_divisors] at hx hy
+    rw [mem_coe, mem_divisors] at hx hy
     exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h
 
 theorem disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) :
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
@@ -449,8 +449,7 @@ theorem HasProd.nat_mul_neg {f : ℤ → M} (hf : HasProd f m) :
         suffices x = 0 by simp only [this, eq_self_iff_true, if_true]
         omega
     _ = (∏ x ∈ u1, f x) * ∏ x ∈ u2, f x := prod_union_inter
-    _ = (∏ b ∈ v', f b) * ∏ b ∈ v', f (-b) := by
-      simp only [u1, u2, Nat.cast_inj, imp_self, implies_true, forall_const, prod_image, neg_inj]
+    _ = (∏ b ∈ v', f b) * ∏ b ∈ v', f (-b) := by simp [u1, u2]
     _ = ∏ b ∈ v', (f b * f (-b)) := prod_mul_distrib.symm⟩
 
 @[to_additive]
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "08681ddeb7536a50dea8026c6693cb9b07f01717",
+   "rev": "4765a4ee7ab89f407e4bc1d2aa1dbae83bd95e16",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
