chore: adaptations for batteries#1486 (#31182)

After [batteries#1486](leanprover-community/batteries#1486) is merged:

- [x] Edit the lakefile to point to leanprover-community/batteries:main
- [x] Run lake update batteries
- [x] Merge leanprover-community/mathlib4:master
- [ ] Wait for CI and merge

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

Author: fgdorais

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -32,29 +32,6 @@ section Monoid
 
 variable [Monoid M] [Monoid N] [Monoid P] {l l₁ l₂ : List M} {a : M}
 
-@[to_additive]
-theorem prod_eq_foldl : ∀ {l : List M}, l.prod = foldl (· * ·) 1 l
-  | [] => rfl
-  | cons a l => by
-    rw [prod_cons, prod_eq_foldl, ← foldl_assoc (α := M) (op := (· * ·))]
-    simp
-
-@[to_additive (attr := simp)]
-theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod :=
-  calc
-    (l₁ ++ l₂).prod = foldr (· * ·) (1 * foldr (· * ·) 1 l₂) l₁ := by simp [List.prod]
-    _ = l₁.prod * l₂.prod := foldr_assoc
-
-@[to_additive]
-theorem prod_concat : (l.concat a).prod = l.prod * a := by
-  rw [concat_eq_append, prod_append, prod_singleton]
-
-@[to_additive (attr := simp)]
-theorem prod_flatten {l : List (List M)} : l.flatten.prod = (l.map List.prod).prod := by
-  induction l with
-  | nil => simp
-  | cons head tail ih => simp only [*, List.flatten_cons, map, prod_append, prod_cons]
-
 open scoped Relator in
 @[to_additive]
 theorem rel_prod {R : M → N → Prop} (h : R 1 1) (hf : (R ⇒ R ⇒ R) (· * ·) (· * ·)) :
@@ -82,8 +59,8 @@ theorem prod_hom₂_nonempty {l : List ι} (f : M → N → P)
 theorem prod_hom₂ (l : List ι) (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d)
     (hf' : f 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) :
     (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by
-  rw [prod, prod, prod, foldr_map, foldr_map, foldr_map,
-    ← l.foldr_hom₂ f _ _ (fun x y => f (f₁ x) (f₂ x) * y) _ _ (by simp [hf]), hf']
+  simp only [prod_eq_foldr, foldr_map]
+  rw [← foldr_hom₂ l f _ _ ((fun x y => f (f₁ x) (f₂ x) * y) ) _ _ (by simp [hf]), hf']
 
 @[to_additive (attr := simp)]
 theorem prod_map_mul {M : Type*} [CommMonoid M] {l : List ι} {f g : ι → M} :
@@ -302,7 +279,7 @@ variable [Group G]
 @[to_additive /-- This is the `List.sum` version of `add_neg_rev` -/]
 theorem prod_inv_reverse : ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).reverse.prod
   | [] => by simp
-  | x :: xs => by simp [prod_inv_reverse xs]
+  | x :: xs => by simp [prod_append, prod_inv_reverse xs]
 
 /-- A non-commutative variant of `List.prod_reverse` -/
 @[to_additive /-- A non-commutative variant of `List.sum_reverse` -/]
@@ -324,8 +301,7 @@ theorem prod_range_div' (n : ℕ) (f : ℕ → G) :
     ((range n).map fun k ↦ f k / f (k + 1)).prod = f 0 / f n := by
   induction n with
   | zero => exact (div_self' (f 0)).symm
-  | succ n h =>
-    rw [range_succ, map_append, map_singleton, prod_append, prod_singleton, h, div_mul_div_cancel]
+  | succ n h => simp [range_succ, prod_append, map_append, h]
 
 end Group
 

Mathlib/Algebra/BigOperators/Group/List/Defs.lean

@@ -18,12 +18,9 @@ variable {ι M N : Type*}
 namespace List
 section Defs
 
-/-- Product of a list.
-
-`List.prod [a, b, c] = a * (b * (c * 1))` -/
-@[to_additive existing]
-def prod {α} [Mul α] [One α] : List α → α :=
-  foldr (· * ·) 1
+set_option linter.existingAttributeWarning false in
+attribute [to_additive existing] prod prod_nil prod_cons prod_one_cons prod_append prod_concat
+  prod_flatten prod_eq_foldl
 
 /-- The alternating sum of a list. -/
 def alternatingSum {G : Type*} [Zero G] [Add G] [Neg G] : List G → G
@@ -44,13 +41,6 @@ section Mul
 
 variable [Mul M] [One M] {a : M} {l : List M}
 
-@[to_additive existing, simp]
-theorem prod_nil : ([] : List M).prod = 1 :=
-  rfl
-
-@[to_additive existing, simp]
-theorem prod_cons : (a :: l).prod = a * l.prod := rfl
-
 @[to_additive]
 lemma prod_induction
     (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ l, p x) :
@@ -68,20 +58,10 @@ section MulOneClass
 
 variable [MulOneClass M] {l : List M} {a : M}
 
-@[to_additive]
-theorem prod_singleton : [a].prod = a :=
-  mul_one a
-
-@[to_additive]
-theorem prod_one_cons : (1 :: l).prod = l.prod := by
-  rw [prod, foldr, one_mul]
-
 @[to_additive]
 theorem prod_map_one {l : List ι} :
     (l.map fun _ => (1 : M)).prod = 1 := by
-  induction l with
-  | nil => rfl
-  | cons hd tl ih => rw [map_cons, prod_one_cons, ih]
+  induction l with simp [*]
 
 @[to_additive]
 lemma prod_induction_nonempty
@@ -102,9 +82,6 @@ section Monoid
 
 variable [Monoid M] [Monoid N]
 
-@[to_additive]
-theorem prod_eq_foldr {l : List M} : l.prod = foldr (· * ·) 1 l := rfl
-
 @[to_additive (attr := simp)]
 theorem prod_replicate (n : ℕ) (a : M) : (replicate n a).prod = a ^ n := by
   induction n with

Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

@@ -44,7 +44,7 @@ theorem prod_map_erase [DecidableEq ι] {a : ι} (h : a ∈ m) :
 
 @[to_additive (attr := simp, grind =)]
 theorem prod_add (s t : Multiset M) : prod (s + t) = prod s * prod t :=
-  Quotient.inductionOn₂ s t fun l₁ l₂ => by simp
+  Quotient.inductionOn₂ s t fun l₁ l₂ => by simp [List.prod_append]
 
 @[to_additive]
 theorem prod_nsmul (m : Multiset M) : ∀ n : ℕ, (n • m).prod = m.prod ^ n

Mathlib/Algebra/Group/Basic.lean

@@ -80,6 +80,11 @@ section MulOneClass
 
 variable [MulOneClass M]
 
+@[to_additive]
+instance Semigroup.to_isLawfulIdentity : Std.LawfulIdentity (α := M) (· * ·) 1 where
+  left_id := one_mul
+  right_id := mul_one
+
 @[to_additive]
 theorem ite_mul_one {P : Prop} [Decidable P] {a b : M} :
     ite P (a * b) 1 = ite P a 1 * ite P b 1 := by

Mathlib/Algebra/Order/BigOperators/Ring/List.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stuart Presnell
 -/
 import Mathlib.Algebra.Order.Ring.Canonical
-import Mathlib.Algebra.BigOperators.Group.List.Defs
 
 /-!
 # Big operators on a list in ordered rings

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

@@ -355,7 +355,7 @@ lemma natDegree_eq_one : p.natDegree = 1 ↔ ∃ a ≠ 0, ∃ b, C a * X + C b =
   · rintro ⟨a, ha, b, rfl⟩
     simp [ha]
 
-theorem subsingleton_isRoot_of_natDegree_eq_one [IsLeftCancelMulZero R] [IsRightCancelAdd R]
+theorem subsingleton_isRoot_of_natDegree_eq_one [IsLeftCancelMulZero R]
     (h : p.natDegree = 1) : { x | IsRoot p x }.Subsingleton := by
   intro r₁
   obtain ⟨r₂, hr₂, r₃, rfl⟩ : ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p := by rwa [natDegree_eq_one] at h

Mathlib/Algebra/Polynomial/Div.lean

@@ -756,7 +756,7 @@ lemma _root_.Irreducible.isRoot_eq_bot_of_natDegree_ne_one
     (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) : p.IsRoot = ⊥ :=
   le_bot_iff.mp fun _ ↦ hi.not_isRoot_of_natDegree_ne_one hdeg
 
-lemma _root_.Irreducible.subsingleton_isRoot [IsLeftCancelMulZero R] [IsRightCancelAdd R]
+lemma _root_.Irreducible.subsingleton_isRoot [IsLeftCancelMulZero R]
     (hi : Irreducible p) : { x | p.IsRoot x }.Subsingleton :=
   fun _ hx ↦ (subsingleton_isRoot_of_natDegree_eq_one <| natDegree_eq_of_degree_eq_some <|
     degree_eq_one_of_irreducible_of_root hi hx) hx

Mathlib/Data/List/Prime.lean

@@ -55,10 +55,10 @@ theorem perm_of_prod_eq_prod :
     ∀ {l₁ l₂ : List M}, l₁.prod = l₂.prod → (∀ p ∈ l₁, Prime p) → (∀ p ∈ l₂, Prime p) → Perm l₁ l₂
   | [], [], _, _, _ => Perm.nil
   | [], a :: l, h₁, _, h₃ =>
-    have ha : a ∣ 1 := prod_nil (M := M) ▸ h₁.symm ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
+    have ha : a ∣ 1 := prod_nil (α := M) ▸ h₁.symm ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
     absurd ha (Prime.not_dvd_one (h₃ a mem_cons_self))
   | a :: l, [], h₁, h₂, _ =>
-    have ha : a ∣ 1 := prod_nil (M := M) ▸ h₁ ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
+    have ha : a ∣ 1 := prod_nil (α := M) ▸ h₁ ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
     absurd ha (Prime.not_dvd_one (h₂ a mem_cons_self))
   | a :: l₁, b :: l₂, h, hl₁, hl₂ => by
     classical

Mathlib/Data/List/ToFinsupp.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Yakov Pechersky. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
-import Mathlib.Algebra.BigOperators.Group.List.Basic
 import Mathlib.Algebra.Group.Embedding
 import Mathlib.Algebra.Group.Finsupp
 import Mathlib.Algebra.Group.Nat.Defs
@@ -126,6 +125,6 @@ theorem toFinsupp_eq_sum_mapIdx_single {R : Type*} [AddMonoid R] (l : List R)
   induction l using List.reverseRecOn with
   | nil => exact toFinsupp_nil
   | append_singleton x xs ih =>
-    classical simp [toFinsupp_concat_eq_toFinsupp_add_single, ih]
+    classical simp [toFinsupp_concat_eq_toFinsupp_add_single, sum_append, ih]
 
 end List

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -3,10 +3,11 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Algebra.BigOperators.Group.List.Basic
 import Mathlib.Algebra.Group.Pi.Basic
 import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.Data.List.Chain
+import Mathlib.Algebra.Group.Int.Defs
+import Mathlib.Algebra.BigOperators.Group.List.Basic
 
 /-!
 # Free groups
@@ -662,7 +663,7 @@ def Lift.aux : List (α × Bool) → β := fun L =>
 
 @[to_additive]
 theorem Red.Step.lift {f : α → β} (H : Red.Step L₁ L₂) : Lift.aux f L₁ = Lift.aux f L₂ := by
-  obtain @⟨_, _, _, b⟩ := H; cases b <;> simp [Lift.aux]
+  obtain @⟨_, _, _, b⟩ := H; cases b <;> simp [Lift.aux, List.prod_append]
 
 /-- If `β` is a group, then any function from `α` to `β` extends uniquely to a group homomorphism
 from the free group over `α` to `β` -/
@@ -672,9 +673,9 @@ from the free group over `α` to `β` -/
 def lift : (α → β) ≃ (FreeGroup α →* β) where
   toFun f :=
     MonoidHom.mk' (Quot.lift (Lift.aux f) fun _ _ => Red.Step.lift) <| by
-      rintro ⟨L₁⟩ ⟨L₂⟩; simp [Lift.aux]
+      rintro ⟨L₁⟩ ⟨L₂⟩; simp [Lift.aux, List.prod_append]
   invFun g := g ∘ of
-  left_inv f := List.prod_singleton
+  left_inv f := by ext; simp [of, Lift.aux]
   right_inv g := by ext; simp [of, Lift.aux]
 
 variable {f}
@@ -684,8 +685,7 @@ theorem lift_mk : lift f (mk L) = List.prod (L.map fun x => cond x.2 (f x.1) (f
   rfl
 
 @[to_additive (attr := simp)]
-theorem lift_apply_of {x} : lift f (of x) = f x :=
-  List.prod_singleton
+theorem lift_apply_of {x} : lift f (of x) = f x := by simp [of]
 
 @[to_additive]
 theorem lift_unique (g : FreeGroup α →* β) (hg : ∀ x, g (FreeGroup.of x) = f x) {x} :