[Merged by Bors] - chore: adaptations for nightly-2024-01-25

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -355,11 +355,11 @@ theorem gcd_assoc' [GCDMonoid α] (m n k : α) : Associated (gcd (gcd m n) k) (g
       ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))
 #align gcd_assoc' gcd_assoc'
 
-instance [NormalizedGCDMonoid α] : IsCommutative α gcd :=
-  ⟨gcd_comm⟩
+instance [NormalizedGCDMonoid α] : Std.Commutative (α := α) gcd where
+  comm := gcd_comm
 
-instance [NormalizedGCDMonoid α] : IsAssociative α gcd :=
-  ⟨gcd_assoc⟩
+instance [NormalizedGCDMonoid α] : Std.Associative (α := α) gcd where
+  assoc := gcd_assoc
 
 theorem gcd_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : gcd a b ∣ c)
     (hcab : c ∣ gcd a b) : gcd a b = normalize c :=
@@ -783,11 +783,11 @@ theorem lcm_assoc' [GCDMonoid α] (m n k : α) : Associated (lcm (lcm m n) k) (l
       (lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))
 #align lcm_assoc' lcm_assoc'
 
-instance [NormalizedGCDMonoid α] : IsCommutative α lcm :=
-  ⟨lcm_comm⟩
+instance [NormalizedGCDMonoid α] : Std.Commutative (α := α) lcm where
+  comm := lcm_comm
 
-instance [NormalizedGCDMonoid α] : IsAssociative α lcm :=
-  ⟨lcm_assoc⟩
+instance [NormalizedGCDMonoid α] : Std.Associative (α := α) lcm where
+  assoc := lcm_assoc
 
 theorem lcm_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : lcm a b ∣ c)
     (hcab : c ∣ lcm a b) : lcm a b = normalize c :=

Mathlib/Algebra/Group/Basic.lean

@@ -76,7 +76,7 @@ section Semigroup
 variable [Semigroup α]
 
 @[to_additive]
-instance Semigroup.to_isAssociative : IsAssociative α (· * ·) := ⟨mul_assoc⟩
+instance Semigroup.to_isAssociative : Std.Associative (α := α)  (· * ·) := ⟨mul_assoc⟩
 #align semigroup.to_is_associative Semigroup.to_isAssociative
 #align add_semigroup.to_is_associative AddSemigroup.to_isAssociative
 
@@ -105,7 +105,7 @@ theorem comp_mul_right (x y : α) : (· * x) ∘ (· * y) = (· * (y * x)) := by
 end Semigroup
 
 @[to_additive]
-instance CommMagma.to_isCommutative [CommMagma G] : IsCommutative G (· * ·) := ⟨mul_comm⟩
+instance CommMagma.to_isCommutative [CommMagma G] : Std.Commutative (α := G) (· * ·) := ⟨mul_comm⟩
 #align comm_semigroup.to_is_commutative CommMagma.to_isCommutative
 #align add_comm_semigroup.to_is_commutative AddCommMagma.to_isCommutative
 

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -184,8 +184,8 @@ attribute [elab_as_elim] WithZero.cases_on
 instance mulOneClass [Mul α] : MulOneClass (WithOne α) where
   mul := (· * ·)
   one := 1
-  one_mul := (Option.liftOrGet_isLeftId _).1
-  mul_one := (Option.liftOrGet_isRightId _).1
+  one_mul := (Option.liftOrGet_isId _).left_id
+  mul_one := (Option.liftOrGet_isId _).right_id
 
 @[to_additive (attr := simp, norm_cast)]
 lemma coe_mul [Mul α] (a b : α) : (↑(a * b) : WithOne α) = a * b := rfl

Mathlib/Algebra/Lie/Abelian.lean

@@ -89,8 +89,9 @@ theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : T
 #align lie_abelian_iff_equiv_lie_abelian lie_abelian_iff_equiv_lie_abelian
 
 theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :
-    IsCommutative A (· * ·) ↔ IsLieAbelian A := by
-  have h₁ : IsCommutative A (· * ·) ↔ ∀ a b : A, a * b = b * a := ⟨fun h => h.1, fun h => ⟨h⟩⟩
+    Std.Commutative (α := A) (· * ·) ↔ IsLieAbelian A := by
+  have h₁ : Std.Commutative (α := A) (· * ·) ↔ ∀ a b : A, a * b = b * a :=
+    ⟨fun h => h.1, fun h => ⟨h⟩⟩
   have h₂ : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
   simp only [h₁, h₂, LieRing.of_associative_ring_bracket, sub_eq_zero]
 #align commutative_ring_iff_abelian_lie_ring commutative_ring_iff_abelian_lie_ring

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -54,7 +54,7 @@ section BooleanRing
 
 variable [BooleanRing α] (a b : α)
 
-instance : IsIdempotent α (· * ·) :=
+instance : Std.IdempotentOp (α := α) (· * ·) :=
   ⟨BooleanRing.mul_self⟩
 
 @[simp]

Mathlib/Algebra/Ring/Idempotents.lean

@@ -42,8 +42,8 @@ def IsIdempotentElem (p : M) : Prop :=
 
 namespace IsIdempotentElem
 
-theorem of_isIdempotent [IsIdempotent M (· * ·)] (a : M) : IsIdempotentElem a :=
-  IsIdempotent.idempotent a
+theorem of_isIdempotent [Std.IdempotentOp (α := M) (· * ·)] (a : M) : IsIdempotentElem a :=
+  Std.IdempotentOp.idempotent a
 #align is_idempotent_elem.of_is_idempotent IsIdempotentElem.of_isIdempotent
 
 theorem eq {p : M} (h : IsIdempotentElem p) : p * p = p :=

Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean

@@ -64,8 +64,10 @@ theorem isUnital_leftAdd : EckmannHilton.IsUnital (· +ₗ ·) 0 := by
     ext
     · aesop_cat
     · simp [biprod.lift_snd, Category.assoc, biprod.inl_snd, comp_zero]
-  exact ⟨⟨fun f => by simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc]⟩,
-    ⟨fun f => by simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]⟩⟩
+  exact {
+    left_id := fun f => by simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc],
+    right_id := fun f => by simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]
+  }
 #align category_theory.semiadditive_of_binary_biproducts.is_unital_left_add CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_leftAdd
 
 theorem isUnital_rightAdd : EckmannHilton.IsUnital (· +ᵣ ·) 0 := by
@@ -79,8 +81,10 @@ theorem isUnital_rightAdd : EckmannHilton.IsUnital (· +ᵣ ·) 0 := by
     ext
     · aesop_cat
     · simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]
-  exact ⟨⟨fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp]⟩,
-    ⟨fun f => by simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]⟩⟩
+  exact {
+    left_id := fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp],
+    right_id := fun f => by simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]
+  }
 #align category_theory.semiadditive_of_binary_biproducts.is_unital_right_add CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_rightAdd
 
 theorem distrib (f g h k : X ⟶ Y) : (f +ᵣ g) +ₗ h +ᵣ k = (f +ₗ h) +ᵣ g +ₗ k := by

Mathlib/Data/Finset/Basic.lean

@@ -1452,23 +1452,23 @@ theorem union_comm (s₁ s₂ : Finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
   sup_comm
 #align finset.union_comm Finset.union_comm
 
-instance : IsCommutative (Finset α) (· ∪ ·) :=
+instance : Std.Commutative (α := Finset α) (· ∪ ·) :=
   ⟨union_comm⟩
 
 @[simp]
 theorem union_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
   sup_assoc
 #align finset.union_assoc Finset.union_assoc
 
-instance : IsAssociative (Finset α) (· ∪ ·) :=
+instance : Std.Associative (α := Finset α) (· ∪ ·) :=
   ⟨union_assoc⟩
 
 @[simp]
 theorem union_idempotent (s : Finset α) : s ∪ s = s :=
   sup_idem
 #align finset.union_idempotent Finset.union_idempotent
 
-instance : IsIdempotent (Finset α) (· ∪ ·) :=
+instance : Std.IdempotentOp (α := Finset α) (· ∪ ·) :=
   ⟨union_idempotent⟩
 
 theorem union_subset_left (h : s ∪ t ⊆ u) : s ⊆ u :=

Mathlib/Data/Finset/Fold.lean

@@ -25,7 +25,7 @@ variable {α β γ : Type*}
 
 section Fold
 
-variable (op : β → β → β) [hc : IsCommutative β op] [ha : IsAssociative β op]
+variable (op : β → β → β) [hc : Std.Commutative op] [ha : Std.Associative op]
 
 local notation a " * " b => op a b
 
@@ -92,7 +92,7 @@ theorem fold_const [hd : Decidable (s = ∅)] (c : β) (h : op c (op b c) = op b
       · exact h
 #align finset.fold_const Finset.fold_const
 
-theorem fold_hom {op' : γ → γ → γ} [IsCommutative γ op'] [IsAssociative γ op'] {m : β → γ}
+theorem fold_hom {op' : γ → γ → γ} [Std.Commutative op'] [Std.Associative op'] {m : β → γ}
     (hm : ∀ x y, m (op x y) = op' (m x) (m y)) :
     (s.fold op' (m b) fun x => m (f x)) = m (s.fold op b f) := by
   rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
@@ -117,15 +117,15 @@ theorem fold_union_inter [DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : 
 #align finset.fold_union_inter Finset.fold_union_inter
 
 @[simp]
-theorem fold_insert_idem [DecidableEq α] [hi : IsIdempotent β op] :
+theorem fold_insert_idem [DecidableEq α] [hi : Std.IdempotentOp op] :
     (insert a s).fold op b f = f a * s.fold op b f := by
   by_cases h : a ∈ s
   · rw [← insert_erase h]
     simp [← ha.assoc, hi.idempotent]
   · apply fold_insert h
 #align finset.fold_insert_idem Finset.fold_insert_idem
 
-theorem fold_image_idem [DecidableEq α] {g : γ → α} {s : Finset γ} [hi : IsIdempotent β op] :
+theorem fold_image_idem [DecidableEq α] {g : γ → α} {s : Finset γ} [hi : Std.IdempotentOp op] :
     (image g s).fold op b f = s.fold op b (f ∘ g) := by
   induction' s using Finset.cons_induction with x xs hx ih
   · rw [fold_empty, image_empty, fold_empty]
@@ -155,10 +155,10 @@ theorem fold_ite' {g : α → β} (hb : op b b = b) (p : α → Prop) [Decidable
 relying on typeclass idempotency over the whole type,
 instead of solely on the seed element.
 However, this is easier to use because it does not generate side goals. -/
-theorem fold_ite [IsIdempotent β op] {g : α → β} (p : α → Prop) [DecidablePred p] :
+theorem fold_ite [Std.IdempotentOp op] {g : α → β} (p : α → Prop) [DecidablePred p] :
     Finset.fold op b (fun i => ite (p i) (f i) (g i)) s =
       op (Finset.fold op b f (s.filter p)) (Finset.fold op b g (s.filter fun i => ¬p i)) :=
-  fold_ite' (IsIdempotent.idempotent _) _
+  fold_ite' (Std.IdempotentOp.idempotent _) _
 #align finset.fold_ite Finset.fold_ite
 
 theorem fold_op_rel_iff_and {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ r x y ∧ r x z)

Mathlib/Data/Finset/NoncommProd.lean

@@ -75,7 +75,7 @@ theorem noncommFoldr_eq_foldr (s : Multiset α) (h : LeftCommutative f) (b : β)
 
 section assoc
 
-variable [assoc : IsAssociative α op]
+variable [assoc : Std.Associative op]
 
 /-- Fold of a `s : Multiset α` with an associative `op : α → α → α`, given a proofs that `op`
 is commutative on all elements `x ∈ s`. -/
@@ -100,8 +100,8 @@ theorem noncommFold_cons (s : Multiset α) (a : α) (h h') (x : α) :
   simp
 #align multiset.noncomm_fold_cons Multiset.noncommFold_cons
 
-theorem noncommFold_eq_fold (s : Multiset α) [IsCommutative α op] (a : α) :
-    noncommFold op s (fun x _ y _ _ => IsCommutative.comm x y) a = fold op a s := by
+theorem noncommFold_eq_fold (s : Multiset α) [Std.Commutative op] (a : α) :
+    noncommFold op s (fun x _ y _ _ => Std.Commutative.comm x y) a = fold op a s := by
   induction s using Quotient.inductionOn
   simp
 #align multiset.noncomm_fold_eq_fold Multiset.noncommFold_eq_fold

Mathlib/Data/Fintype/Lattice.lean

@@ -38,7 +38,7 @@ theorem inf_univ_eq_iInf [CompleteLattice β] (f : α → β) : Finset.univ.inf
 @[simp]
 theorem fold_inf_univ [SemilatticeInf α] [OrderBot α] (a : α) :
     -- Porting note: added `haveI`
-    haveI : IsCommutative α (· ⊓ ·) := inferInstance
+    haveI : Std.Commutative (α := α) (· ⊓ ·) := inferInstance
     (Finset.univ.fold (· ⊓ ·) a fun x => x) = ⊥ :=
   eq_bot_iff.2 <|
     ((Finset.fold_op_rel_iff_and <| @le_inf_iff α _).1 le_rfl).2 ⊥ <| Finset.mem_univ _
@@ -47,7 +47,7 @@ theorem fold_inf_univ [SemilatticeInf α] [OrderBot α] (a : α) :
 @[simp]
 theorem fold_sup_univ [SemilatticeSup α] [OrderTop α] (a : α) :
     -- Porting note: added `haveI`
-    haveI : IsCommutative α (· ⊔ ·) := inferInstance
+    haveI : Std.Commutative (α := α) (· ⊔ ·) := inferInstance
     (Finset.univ.fold (· ⊔ ·) a fun x => x) = ⊤ :=
   @fold_inf_univ αᵒᵈ _ _ _ _
 #align finset.fold_sup_univ Finset.fold_sup_univ

Mathlib/Data/List/Basic.lean

@@ -41,14 +41,12 @@ instance uniqueOfIsEmpty [IsEmpty α] : Unique (List α) :=
       | a :: _ => isEmptyElim a }
 #align list.unique_of_is_empty List.uniqueOfIsEmpty
 
-instance : IsLeftId (List α) Append.append [] :=
-  ⟨nil_append⟩
+instance : Std.LawfulIdentity (α := List α) Append.append [] where
+  left_id := nil_append
+  right_id := append_nil
 
-instance : IsRightId (List α) Append.append [] :=
-  ⟨append_nil⟩
-
-instance : IsAssociative (List α) Append.append :=
-  ⟨append_assoc⟩
+instance : Std.Associative (α := List α) Append.append where
+  assoc := append_assoc
 
 #align list.cons_ne_nil List.cons_ne_nil
 #align list.cons_ne_self List.cons_ne_self
@@ -2650,7 +2648,7 @@ end FoldlEqFoldlr'
 
 section
 
-variable {op : α → α → α} [ha : IsAssociative α op] [hc : IsCommutative α op]
+variable {op : α → α → α} [ha : Std.Associative op] [hc : Std.Commutative op]
 
 /-- Notation for `op a b`. -/
 local notation a " ⋆ " b => op a b

Mathlib/Data/List/Perm.lean

@@ -278,7 +278,7 @@ theorem Perm.foldr_eq {f : α → β → β} {l₁ l₂ : List α} (lcomm : Left
 
 section
 
-variable {op : α → α → α} [IA : IsAssociative α op] [IC : IsCommutative α op]
+variable {op : α → α → α} [IA : Std.Associative op] [IC : Std.Commutative op]
 
 -- mathport name: op
 local notation a " * " b => op a b

Mathlib/Data/Multiset/Fold.lean

@@ -22,7 +22,7 @@ variable {α β : Type*}
 
 section Fold
 
-variable (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op]
+variable (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op]
 
 local notation a " * " b => op a b
 
@@ -100,7 +100,7 @@ theorem fold_distrib {f g : β → α} (u₁ u₂ : α) (s : Multiset β) :
       ha.assoc, hc.comm (g a), ha.assoc])
 #align multiset.fold_distrib Multiset.fold_distrib
 
-theorem fold_hom {op' : β → β → β} [IsCommutative β op'] [IsAssociative β op'] {m : α → β}
+theorem fold_hom {op' : β → β → β} [Std.Commutative op'] [Std.Associative op'] {m : α → β}
     (hm : ∀ x y, m (op x y) = op' (m x) (m y)) (b : α) (s : Multiset α) :
     (s.map m).fold op' (m b) = m (s.fold op b) :=
   Multiset.induction_on s (by simp) (by simp (config := { contextual := true }) [hm])
@@ -112,7 +112,7 @@ theorem fold_union_inter [DecidableEq α] (s₁ s₂ : Multiset α) (b₁ b₂ :
 #align multiset.fold_union_inter Multiset.fold_union_inter
 
 @[simp]
-theorem fold_dedup_idem [DecidableEq α] [hi : IsIdempotent α op] (s : Multiset α) (b : α) :
+theorem fold_dedup_idem [DecidableEq α] [hi : Std.IdempotentOp op] (s : Multiset α) (b : α) :
     (dedup s).fold op b = s.fold op b :=
   Multiset.induction_on s (by simp) fun a s IH => by
     by_cases h : a ∈ s <;> simp [IH, h]

Mathlib/Data/Option/Defs.lean

@@ -103,29 +103,27 @@ theorem mem_toList {a : α} {o : Option α} : a ∈ toList o ↔ a ∈ o := by
   cases o <;> simp [toList, eq_comm]
 #align option.mem_to_list Option.mem_toList
 
-instance liftOrGet_isCommutative (f : α → α → α) [IsCommutative α f] :
-    IsCommutative (Option α) (liftOrGet f) :=
-  ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, IsCommutative.comm]⟩
+instance liftOrGet_isCommutative (f : α → α → α) [Std.Commutative f] :
+    Std.Commutative (liftOrGet f) :=
+  ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, Std.Commutative.comm]⟩
 
-instance liftOrGet_isAssociative (f : α → α → α) [IsAssociative α f] :
-    IsAssociative (Option α) (liftOrGet f) :=
-  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [liftOrGet, IsAssociative.assoc]⟩
+instance liftOrGet_isAssociative (f : α → α → α) [Std.Associative f] :
+    Std.Associative (liftOrGet f) :=
+  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [liftOrGet, Std.Associative.assoc]⟩
 
-instance liftOrGet_isIdempotent (f : α → α → α) [IsIdempotent α f] :
-    IsIdempotent (Option α) (liftOrGet f) :=
-  ⟨fun a ↦ by cases a <;> simp [liftOrGet, IsIdempotent.idempotent]⟩
+instance liftOrGet_isIdempotent (f : α → α → α) [Std.IdempotentOp f] :
+    Std.IdempotentOp (liftOrGet f) :=
+  ⟨fun a ↦ by cases a <;> simp [liftOrGet, Std.IdempotentOp.idempotent]⟩
 
-instance liftOrGet_isLeftId (f : α → α → α) : IsLeftId (Option α) (liftOrGet f) none :=
-  ⟨fun a ↦ by cases a <;> simp [liftOrGet]⟩
-
-instance liftOrGet_isRightId (f : α → α → α) : IsRightId (Option α) (liftOrGet f) none :=
-  ⟨fun a ↦ by cases a <;> simp [liftOrGet]⟩
+instance liftOrGet_isId (f : α → α → α) : Std.LawfulIdentity (liftOrGet f) none where
+  left_id a := by cases a <;> simp [liftOrGet]
+  right_id a := by cases a <;> simp [liftOrGet]
 
 #align option.lift_or_get_comm Option.liftOrGet_isCommutative
 #align option.lift_or_get_assoc Option.liftOrGet_isAssociative
 #align option.lift_or_get_idem Option.liftOrGet_isIdempotent
-#align option.lift_or_get_is_left_id Option.liftOrGet_isLeftId
-#align option.lift_or_get_is_right_id Option.liftOrGet_isRightId
+#align option.lift_or_get_is_left_id Option.liftOrGet_isId
+#align option.lift_or_get_is_right_id Option.liftOrGet_isId
 
 /-- Convert `undef` to `none` to make an `LOption` into an `Option`. -/
 def _root_.Lean.LOption.toOption {α} : Lean.LOption α → Option α

Mathlib/Data/Set/Basic.lean

@@ -757,11 +757,11 @@ theorem union_assoc (a b c : Set α) : a ∪ b ∪ c = a ∪ (b ∪ c) :=
   ext fun _ => or_assoc
 #align set.union_assoc Set.union_assoc
 
-instance union_isAssoc : IsAssociative (Set α) (· ∪ ·) :=
+instance union_isAssoc : Std.Associative (α := Set α) (· ∪ ·) :=
   ⟨union_assoc⟩
 #align set.union_is_assoc Set.union_isAssoc
 
-instance union_isComm : IsCommutative (Set α) (· ∪ ·) :=
+instance union_isComm : Std.Commutative (α := Set α) (· ∪ ·) :=
   ⟨union_comm⟩
 #align set.union_is_comm Set.union_isComm
 
@@ -911,11 +911,11 @@ theorem inter_assoc (a b c : Set α) : a ∩ b ∩ c = a ∩ (b ∩ c) :=
   ext fun _ => and_assoc
 #align set.inter_assoc Set.inter_assoc
 
-instance inter_isAssoc : IsAssociative (Set α) (· ∩ ·) :=
+instance inter_isAssoc : Std.Associative (α := Set α) (· ∩ ·) :=
   ⟨inter_assoc⟩
 #align set.inter_is_assoc Set.inter_isAssoc
 
-instance inter_isComm : IsCommutative (Set α) (· ∩ ·) :=
+instance inter_isComm : Std.Commutative (α := Set α) (· ∩ ·) :=
   ⟨inter_comm⟩
 #align set.inter_is_comm Set.inter_isComm