From 500d6dd12a217e9854108710b5cba707589f40c3 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 25 Jan 2024 17:02:56 +0100 Subject: [PATCH 1/5] Merge remote-tracking branch 'origin/lean-pr-testing-3195' into nightly-testing (cherry picked from commit add685a24611d9420d6be7e32e189ec1274d89c8) --- Mathlib/Algebra/GCDMonoid/Basic.lean | 16 +++---- Mathlib/Algebra/Group/Basic.lean | 4 +- Mathlib/Algebra/Group/WithOne/Defs.lean | 4 +- Mathlib/Algebra/Lie/Abelian.lean | 4 +- Mathlib/Algebra/Ring/BooleanRing.lean | 2 +- Mathlib/Algebra/Ring/Idempotents.lean | 4 +- .../Preadditive/OfBiproducts.lean | 12 ++++-- Mathlib/Data/Finset/Basic.lean | 6 +-- Mathlib/Data/Finset/Fold.lean | 12 +++--- Mathlib/Data/Finset/NoncommProd.lean | 6 +-- Mathlib/Data/Fintype/Lattice.lean | 4 +- Mathlib/Data/List/Basic.lean | 14 +++---- Mathlib/Data/List/Perm.lean | 2 +- Mathlib/Data/Multiset/Fold.lean | 6 +-- Mathlib/Data/Option/Defs.lean | 26 +++++------- Mathlib/Data/Set/Basic.lean | 8 ++-- Mathlib/GroupTheory/EckmannHilton.lean | 9 ++-- Mathlib/GroupTheory/Subgroup/Basic.lean | 4 +- Mathlib/Init/Algebra/Classes.lean | 42 +++++++------------ Mathlib/Logic/Basic.lean | 2 +- Mathlib/Logic/Equiv/Basic.lean | 4 +- Mathlib/Logic/Function/Conjugate.lean | 24 +++++------ Mathlib/Order/Lattice.lean | 15 +++---- Mathlib/Order/MinMax.lean | 14 +++---- Mathlib/Order/SymmDiff.lean | 8 ++-- Mathlib/Topology/Homotopy/HomotopyGroup.lean | 6 ++- 26 files changed, 121 insertions(+), 137 deletions(-) diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean index 996392c72d6ff..ff9e2719275f0 100644 --- a/Mathlib/Algebra/GCDMonoid/Basic.lean +++ b/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 := diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index 9cc7b2c117dbc..e332467d8897c 100644 --- a/Mathlib/Algebra/Group/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean index dcf263a377592..c58394120f7dc 100644 --- a/Mathlib/Algebra/Group/WithOne/Defs.lean +++ b/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 diff --git a/Mathlib/Algebra/Lie/Abelian.lean b/Mathlib/Algebra/Lie/Abelian.lean index ea25f01255453..e2e79f321b382 100644 --- a/Mathlib/Algebra/Lie/Abelian.lean +++ b/Mathlib/Algebra/Lie/Abelian.lean @@ -89,8 +89,8 @@ 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 diff --git a/Mathlib/Algebra/Ring/BooleanRing.lean b/Mathlib/Algebra/Ring/BooleanRing.lean index ae75c55d39791..29979e6a392f4 100644 --- a/Mathlib/Algebra/Ring/BooleanRing.lean +++ b/Mathlib/Algebra/Ring/BooleanRing.lean @@ -54,7 +54,7 @@ section BooleanRing variable [BooleanRing α] (a b : α) -instance : IsIdempotent α (· * ·) := +instance : Std.IdempotentOp (α := α) (· * ·) := ⟨BooleanRing.mul_self⟩ @[simp] diff --git a/Mathlib/Algebra/Ring/Idempotents.lean b/Mathlib/Algebra/Ring/Idempotents.lean index 9fb919d04b7c8..44637a34f3d87 100644 --- a/Mathlib/Algebra/Ring/Idempotents.lean +++ b/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 := diff --git a/Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean b/Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean index e380fac53ef8d..b5c39f050ce79 100644 --- a/Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean +++ b/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 diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index 2cbed15f7771b..a87a3c5364c0d 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/Mathlib/Data/Finset/Basic.lean @@ -1452,7 +1452,7 @@ 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] @@ -1460,7 +1460,7 @@ theorem union_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∪ s₂ ∪ s₃ = s₁ sup_assoc #align finset.union_assoc Finset.union_assoc -instance : IsAssociative (Finset α) (· ∪ ·) := +instance : Std.Associative (α := Finset α) (· ∪ ·) := ⟨union_assoc⟩ @[simp] @@ -1468,7 +1468,7 @@ 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 := diff --git a/Mathlib/Data/Finset/Fold.lean b/Mathlib/Data/Finset/Fold.lean index 9c3e35b64a012..5575648267c7c 100644 --- a/Mathlib/Data/Finset/Fold.lean +++ b/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,7 +117,7 @@ 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] @@ -125,7 +125,7 @@ theorem fold_insert_idem [DecidableEq α] [hi : IsIdempotent β op] : · 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) diff --git a/Mathlib/Data/Finset/NoncommProd.lean b/Mathlib/Data/Finset/NoncommProd.lean index ab0133e010833..e2828bba31027 100644 --- a/Mathlib/Data/Finset/NoncommProd.lean +++ b/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 diff --git a/Mathlib/Data/Fintype/Lattice.lean b/Mathlib/Data/Fintype/Lattice.lean index a328954aa08bd..c2a59cfb38508 100644 --- a/Mathlib/Data/Fintype/Lattice.lean +++ b/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 diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 58fa0bead9274..6c73c6e23df47 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/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 diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index 0493db1487451..401d93084b594 100644 --- a/Mathlib/Data/List/Perm.lean +++ 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 diff --git a/Mathlib/Data/Multiset/Fold.lean b/Mathlib/Data/Multiset/Fold.lean index 99141dfea5d8b..6b2c19e781084 100644 --- a/Mathlib/Data/Multiset/Fold.lean +++ 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] diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean index 8ad18723f50b3..a2998ef365761 100644 --- a/Mathlib/Data/Option/Defs.lean +++ b/Mathlib/Data/Option/Defs.lean @@ -103,29 +103,25 @@ 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_isId (f : α → α → α) : Std.LawfulIdentity (liftOrGet f) none where + left_id a := by cases a <;> simp [liftOrGet] + right_id a := by cases a <;> simp [liftOrGet] -instance liftOrGet_isRightId (f : α → α → α) : IsRightId (Option α) (liftOrGet f) none := - ⟨fun 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 LawfulIdentity.toLeftIdentity +--#align option.lift_or_get_is_right_id LawfulIdentity.toLeftIdentity /-- Convert `undef` to `none` to make an `LOption` into an `Option`. -/ def _root_.Lean.LOption.toOption {α} : Lean.LOption α → Option α diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index de779712c72f4..a38bb4e8a7750 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/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 diff --git a/Mathlib/GroupTheory/EckmannHilton.lean b/Mathlib/GroupTheory/EckmannHilton.lean index a986d6bd2b231..1d65f01cfb79c 100644 --- a/Mathlib/GroupTheory/EckmannHilton.lean +++ b/Mathlib/GroupTheory/EckmannHilton.lean @@ -35,12 +35,13 @@ local notation a " <" m:51 "> " b => m a b /-- `IsUnital m e` expresses that `e : X` is a left and right unit for the binary operation `m : X → X → X`. -/ -structure IsUnital (m : X → X → X) (e : X) extends IsLeftId _ m e, IsRightId _ m e : Prop +structure IsUnital (m : X → X → X) (e : X) extends Std.LawfulIdentity m e : Prop #align eckmann_hilton.is_unital EckmannHilton.IsUnital @[to_additive EckmannHilton.AddZeroClass.IsUnital] theorem MulOneClass.isUnital [_G : MulOneClass X] : IsUnital (· * ·) (1 : X) := - IsUnital.mk ⟨MulOneClass.one_mul⟩ ⟨MulOneClass.mul_one⟩ + IsUnital.mk { left_id := MulOneClass.one_mul, + right_id := MulOneClass.mul_one } #align eckmann_hilton.mul_one_class.is_unital EckmannHilton.MulOneClass.isUnital #align eckmann_hilton.add_zero_class.is_unital EckmannHilton.AddZeroClass.IsUnital @@ -75,7 +76,7 @@ theorem mul : m₁ = m₂ := by then these operations are commutative. In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`. -/ -theorem mul_comm : IsCommutative _ m₂ := +theorem mul_comm : Std.Commutative m₂ := ⟨fun a b => by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib e₂ a b e₂⟩ #align eckmann_hilton.mul_comm EckmannHilton.mul_comm @@ -83,7 +84,7 @@ theorem mul_comm : IsCommutative _ m₂ := then these operations are associative. In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`. -/ -theorem mul_assoc : IsAssociative _ m₂ := +theorem mul_assoc : Std.Associative m₂ := ⟨fun a b c => by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c⟩ #align eckmann_hilton.mul_assoc EckmannHilton.mul_assoc diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index 2181cd5907cd4..3c57459235d4e 100644 --- a/Mathlib/GroupTheory/Subgroup/Basic.lean +++ b/Mathlib/GroupTheory/Subgroup/Basic.lean @@ -2405,7 +2405,7 @@ end Centralizer /-- Commutativity of a subgroup -/ structure IsCommutative : Prop where /-- `*` is commutative on `H` -/ - is_comm : IsCommutative H (· * ·) + is_comm : Std.Commutative (α := H) (· * ·) #align subgroup.is_commutative Subgroup.IsCommutative attribute [class] IsCommutative @@ -2413,7 +2413,7 @@ attribute [class] IsCommutative /-- Commutativity of an additive subgroup -/ structure _root_.AddSubgroup.IsCommutative (H : AddSubgroup A) : Prop where /-- `+` is commutative on `H` -/ - is_comm : _root_.IsCommutative H (· + ·) + is_comm : Std.Commutative (α := H) (· + ·) #align add_subgroup.is_commutative AddSubgroup.IsCommutative attribute [to_additive] Subgroup.IsCommutative diff --git a/Mathlib/Init/Algebra/Classes.lean b/Mathlib/Init/Algebra/Classes.lean index 93be685a599df..a3a8882bfac3e 100644 --- a/Mathlib/Init/Algebra/Classes.lean +++ b/Mathlib/Init/Algebra/Classes.lean @@ -72,38 +72,27 @@ class IsSymmOp (α : Type u) (β : Type v) (op : α → α → β) : Prop where #align is_symm_op IsSymmOp /-- A commutative binary operation. -/ -class IsCommutative (α : Type u) (op : α → α → α) : Prop where - comm : ∀ a b, op a b = op b a +@[deprecated IsCommutative] +abbrev IsCommutative (α : Type u) (op : α → α → α) := Std.Commutative op #align is_commutative IsCommutative -instance {op} [IsCommutative α op] : Lean.IsCommutative op where - comm := IsCommutative.comm - instance (priority := 100) isSymmOp_of_isCommutative (α : Type u) (op : α → α → α) - [IsCommutative α op] : IsSymmOp α α op where symm_op := IsCommutative.comm + [Std.Commutative op] : IsSymmOp α α op where symm_op := Std.Commutative.comm #align is_symm_op_of_is_commutative isSymmOp_of_isCommutative /-- An associative binary operation. -/ -class IsAssociative (α : Type u) (op : α → α → α) : Prop where - assoc : ∀ a b c, op (op a b) c = op a (op b c) -#align is_associative IsAssociative - -instance {op} [IsAssociative α op] : Lean.IsAssociative op where - assoc := IsAssociative.assoc +@[deprecated IsAssociative] +abbrev IsAssociative (α : Type u) (op : α → α → α) := Std.Associative op /-- A binary operation with a left identity. -/ -class IsLeftId (α : Type u) (op : α → α → α) (o : outParam α) : Prop where - left_id : ∀ a, op o a = a -#align is_left_id IsLeftId +@[deprecated IsLeftId] +abbrev IsLeftId (α : Type u) (op : α → α → α) (o : outParam α) := Std.LawfulLeftIdentity op o +#align is_left_id Std.LawfulLeftIdentity /-- A binary operation with a right identity. -/ -class IsRightId (α : Type u) (op : α → α → α) (o : outParam α) : Prop where - right_id : ∀ a, op a o = a -#align is_right_id IsRightId - -instance {op} [IsLeftId α op o] [IsRightId α op o] : Lean.IsNeutral op o where - left_neutral := IsLeftId.left_id - right_neutral := IsRightId.right_id +@[deprecated IsRightId] +abbrev IsRightId (α : Type u) (op : α → α → α) (o : outParam α) := Std.LawfulRightIdentity op o +#align is_right_id Std.LawfulRightIdentity -- class IsLeftNull (α : Type u) (op : α → α → α) (o : outParam α) : Prop where -- left_null : ∀ a, op o a = o @@ -121,12 +110,9 @@ class IsRightCancel (α : Type u) (op : α → α → α) : Prop where right_cancel : ∀ a b c, op a b = op c b → a = c #align is_right_cancel IsRightCancel -class IsIdempotent (α : Type u) (op : α → α → α) : Prop where - idempotent : ∀ a, op a a = a -#align is_idempotent IsIdempotent - -instance {op} [IsIdempotent α op] : Lean.IsIdempotent op where - idempotent := IsIdempotent.idempotent +@[deprecated IsIdempotent] +abbrev IsIdempotent (α : Type u) (op : α → α → α) := Std.IdempotentOp op +#align is_idempotent Std.IdempotentOp -- class IsLeftDistrib (α : Type u) (op₁ : α → α → α) (op₂ : outParam <| α → α → α) : Prop where -- left_distrib : ∀ a b c, op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c) diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index 4b35de4a91df6..4558cbb510278 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -302,7 +302,7 @@ lemma Iff.ne_right {α β : Sort*} {a b : α} {c d : β} : (a ≠ b ↔ c = d) theorem xor_comm (a b) : Xor' a b = Xor' b a := by simp [Xor', and_comm, or_comm] #align xor_comm xor_comm -instance : IsCommutative Prop Xor' := ⟨xor_comm⟩ +instance : Std.Commutative Xor' := ⟨xor_comm⟩ @[simp] theorem xor_self (a : Prop) : Xor' a a = False := by simp [Xor'] #align xor_self xor_self diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean index bbc0360364928..1ec05f76b0664 100644 --- a/Mathlib/Logic/Equiv/Basic.lean +++ b/Mathlib/Logic/Equiv/Basic.lean @@ -1958,10 +1958,10 @@ theorem semiconj_conj (f : α₁ → α₁) : Semiconj e f (e.conj f) := fun x = theorem semiconj₂_conj : Semiconj₂ e f (e.arrowCongr e.conj f) := fun x y => by simp [arrowCongr] #align equiv.semiconj₂_conj Equiv.semiconj₂_conj -instance [IsAssociative α₁ f] : IsAssociative β₁ (e.arrowCongr (e.arrowCongr e) f) := +instance [Std.Associative f] : Std.Associative (e.arrowCongr (e.arrowCongr e) f) := (e.semiconj₂_conj f).isAssociative_right e.surjective -instance [IsIdempotent α₁ f] : IsIdempotent β₁ (e.arrowCongr (e.arrowCongr e) f) := +instance [Std.IdempotentOp f] : Std.IdempotentOp (e.arrowCongr (e.arrowCongr e) f) := (e.semiconj₂_conj f).isIdempotent_right e.surjective instance [IsLeftCancel α₁ f] : IsLeftCancel β₁ (e.arrowCongr (e.arrowCongr e) f) := diff --git a/Mathlib/Logic/Function/Conjugate.lean b/Mathlib/Logic/Function/Conjugate.lean index d7f6e31f0fe43..0f974e7321a83 100644 --- a/Mathlib/Logic/Function/Conjugate.lean +++ b/Mathlib/Logic/Function/Conjugate.lean @@ -191,24 +191,24 @@ theorem comp {f' : β → γ} {gc : γ → γ → γ} (hf' : Semiconj₂ f' gb g Semiconj₂ (f' ∘ f) ga gc := fun x y ↦ by simp only [hf'.eq, hf.eq, comp_apply] #align function.semiconj₂.comp Function.Semiconj₂.comp -theorem isAssociative_right [IsAssociative α ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) : - IsAssociative β gb := - ⟨h_surj.forall₃.2 fun x₁ x₂ x₃ ↦ by simp only [← h.eq, @IsAssociative.assoc _ ga]⟩ +theorem isAssociative_right [Std.Associative ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) : + Std.Associative gb := + ⟨h_surj.forall₃.2 fun x₁ x₂ x₃ ↦ by simp only [← h.eq, Std.Associative.assoc (op := ga)]⟩ #align function.semiconj₂.is_associative_right Function.Semiconj₂.isAssociative_right -theorem isAssociative_left [IsAssociative β gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : - IsAssociative α ga := - ⟨fun x₁ x₂ x₃ ↦ h_inj <| by simp only [h.eq, @IsAssociative.assoc _ gb]⟩ +theorem isAssociative_left [Std.Associative gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : + Std.Associative ga := + ⟨fun x₁ x₂ x₃ ↦ h_inj <| by simp only [h.eq, Std.Associative.assoc (op := gb)]⟩ #align function.semiconj₂.is_associative_left Function.Semiconj₂.isAssociative_left -theorem isIdempotent_right [IsIdempotent α ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) : - IsIdempotent β gb := - ⟨h_surj.forall.2 fun x ↦ by simp only [← h.eq, @IsIdempotent.idempotent _ ga]⟩ +theorem isIdempotent_right [Std.IdempotentOp ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) : + Std.IdempotentOp gb := + ⟨h_surj.forall.2 fun x ↦ by simp only [← h.eq, Std.IdempotentOp.idempotent (op := ga)]⟩ #align function.semiconj₂.is_idempotent_right Function.Semiconj₂.isIdempotent_right -theorem isIdempotent_left [IsIdempotent β gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : - IsIdempotent α ga := - ⟨fun x ↦ h_inj <| by rw [h.eq, @IsIdempotent.idempotent _ gb]⟩ +theorem isIdempotent_left [Std.IdempotentOp gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : + Std.IdempotentOp ga := + ⟨fun x ↦ h_inj <| by rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]⟩ #align function.semiconj₂.is_idempotent_left Function.Semiconj₂.isIdempotent_left end Semiconj₂ diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean index 89dc78ea9ae86..ee7be6f3549ca 100644 --- a/Mathlib/Order/Lattice.lean +++ b/Mathlib/Order/Lattice.lean @@ -231,21 +231,18 @@ theorem sup_le_sup_right (h₁ : a ≤ b) (c) : a ⊔ c ≤ b ⊔ c := theorem sup_idem : a ⊔ a = a := by simp #align sup_idem sup_idem -instance : IsIdempotent α (· ⊔ ·) := - ⟨@sup_idem _ _⟩ +instance : Std.IdempotentOp (α := α) (· ⊔ ·) := ⟨@sup_idem _ _⟩ theorem sup_comm : a ⊔ b = b ⊔ a := by apply le_antisymm <;> simp #align sup_comm sup_comm -instance : IsCommutative α (· ⊔ ·) := - ⟨@sup_comm _ _⟩ +instance : Std.Commutative (α := α) (· ⊔ ·) := ⟨@sup_comm _ _⟩ theorem sup_assoc : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := eq_of_forall_ge_iff fun x => by simp only [sup_le_iff]; rw [and_assoc] #align sup_assoc sup_assoc -instance : IsAssociative α (· ⊔ ·) := - ⟨@sup_assoc _ _⟩ +instance : Std.Associative (α := α) (· ⊔ ·) := ⟨@sup_assoc _ _⟩ theorem sup_left_right_swap (a b c : α) : a ⊔ b ⊔ c = c ⊔ b ⊔ a := by rw [sup_comm, @sup_comm _ _ a, sup_assoc] @@ -481,21 +478,21 @@ theorem inf_idem : a ⊓ a = a := @sup_idem αᵒᵈ _ _ #align inf_idem inf_idem -instance : IsIdempotent α (· ⊓ ·) := +instance : Std.IdempotentOp (α := α) (· ⊓ ·) := ⟨@inf_idem _ _⟩ theorem inf_comm : a ⊓ b = b ⊓ a := @sup_comm αᵒᵈ _ _ _ #align inf_comm inf_comm -instance : IsCommutative α (· ⊓ ·) := +instance : Std.Commutative (α := α) (· ⊓ ·) := ⟨@inf_comm _ _⟩ theorem inf_assoc : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := @sup_assoc αᵒᵈ _ a b c #align inf_assoc inf_assoc -instance : IsAssociative α (· ⊓ ·) := +instance : Std.Associative (α := α) (· ⊓ ·) := ⟨@inf_assoc _ _⟩ theorem inf_left_right_swap (a b c : α) : a ⊓ b ⊓ c = c ⊓ b ⊓ a := diff --git a/Mathlib/Order/MinMax.lean b/Mathlib/Order/MinMax.lean index 2970f3dd0d6bc..561b201852e9c 100644 --- a/Mathlib/Order/MinMax.lean +++ b/Mathlib/Order/MinMax.lean @@ -206,13 +206,13 @@ theorem max_lt_max_right_iff : max a b < max a c ↔ b < c ∧ a < c := #align max_lt_max_right_iff max_lt_max_right_iff /-- An instance asserting that `max a a = a` -/ -instance max_idem : IsIdempotent α max where +instance max_idem : Std.IdempotentOp (α := α) max where idempotent := by simp #align max_idem max_idem -- short-circuit type class inference /-- An instance asserting that `min a a = a` -/ -instance min_idem : IsIdempotent α min where +instance min_idem : Std.IdempotentOp (α := α) min where idempotent := by simp #align min_idem min_idem @@ -299,10 +299,10 @@ theorem max_associative : Associative (max : α → α → α) := max_assoc #align max_associative max_associative -instance : IsCommutative α max where +instance : Std.Commutative (α := α) max where comm := max_comm -instance : IsAssociative α max where +instance : Std.Associative (α := α) max where assoc := max_assoc theorem max_left_commutative : LeftCommutative (max : α → α → α) := @@ -313,14 +313,14 @@ theorem min_commutative : Commutative (min : α → α → α) := min_comm #align min_commutative min_commutative -theorem min_associative : Associative (min : α → α → α) := +theorem min_associative : Associative (α := α) min := min_assoc #align min_associative min_associative -instance : IsCommutative α min where +instance : Std.Commutative (α := α) min where comm := min_comm -instance : IsAssociative α min where +instance : Std.Associative (α := α) min where assoc := min_assoc theorem min_left_commutative : LeftCommutative (min : α → α → α) := diff --git a/Mathlib/Order/SymmDiff.lean b/Mathlib/Order/SymmDiff.lean index 28a16946cf572..ef8abdd945cee 100644 --- a/Mathlib/Order/SymmDiff.lean +++ b/Mathlib/Order/SymmDiff.lean @@ -113,7 +113,7 @@ theorem ofDual_bihimp (a b : αᵒᵈ) : ofDual (a ⇔ b) = ofDual a ∆ ofDual theorem symmDiff_comm : a ∆ b = b ∆ a := by simp only [symmDiff, sup_comm] #align symm_diff_comm symmDiff_comm -instance symmDiff_isCommutative : IsCommutative α (· ∆ ·) := +instance symmDiff_isCommutative : Std.Commutative (α := α) (· ∆ ·) := ⟨symmDiff_comm⟩ #align symm_diff_is_comm symmDiff_isCommutative @@ -234,7 +234,7 @@ theorem ofDual_symmDiff (a b : αᵒᵈ) : ofDual (a ∆ b) = ofDual a ⇔ ofDua theorem bihimp_comm : a ⇔ b = b ⇔ a := by simp only [(· ⇔ ·), inf_comm] #align bihimp_comm bihimp_comm -instance bihimp_isCommutative : IsCommutative α (· ⇔ ·) := +instance bihimp_isCommutative : Std.Commutative (α := α) (· ⇔ ·) := ⟨bihimp_comm⟩ #align bihimp_is_comm bihimp_isCommutative @@ -474,7 +474,7 @@ theorem symmDiff_assoc : a ∆ b ∆ c = a ∆ (b ∆ c) := by rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right] #align symm_diff_assoc symmDiff_assoc -instance symmDiff_isAssociative : IsAssociative α (· ∆ ·) := +instance symmDiff_isAssociative : Std.Associative (α := α) (· ∆ ·) := ⟨symmDiff_assoc⟩ #align symm_diff_is_assoc symmDiff_isAssociative @@ -623,7 +623,7 @@ theorem bihimp_assoc : a ⇔ b ⇔ c = a ⇔ (b ⇔ c) := @symmDiff_assoc αᵒᵈ _ _ _ _ #align bihimp_assoc bihimp_assoc -instance bihimp_isAssociative : IsAssociative α (· ⇔ ·) := +instance bihimp_isAssociative : Std.Associative (α := α) (· ⇔ ·) := ⟨bihimp_assoc⟩ #align bihimp_is_assoc bihimp_isAssociative diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean index 3bf9198692c36..90926e106ce7c 100644 --- a/Mathlib/Topology/Homotopy/HomotopyGroup.lean +++ b/Mathlib/Topology/Homotopy/HomotopyGroup.lean @@ -515,8 +515,10 @@ def auxGroup (i : N) : Group (HomotopyGroup N X x) := #align homotopy_group.aux_group HomotopyGroup.auxGroup theorem isUnital_auxGroup (i : N) : - EckmannHilton.IsUnital (auxGroup i).mul (⟦const⟧ : HomotopyGroup N X x) := - ⟨⟨(auxGroup i).one_mul⟩, ⟨(auxGroup i).mul_one⟩⟩ + EckmannHilton.IsUnital (auxGroup i).mul (⟦const⟧ : HomotopyGroup N X x) := { + left_id := (auxGroup i).one_mul, + right_id := (auxGroup i).mul_one + } #align homotopy_group.is_unital_aux_group HomotopyGroup.isUnital_auxGroup theorem auxGroup_indep (i j : N) : (auxGroup i : Group (HomotopyGroup N X x)) = auxGroup j := by From 8ae7792a9cc4b0577c0b5545996fb75cc6a6b97b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 25 Jan 2024 17:33:28 +0100 Subject: [PATCH 2/5] Linebreaks (cherry picked from commit 006e42c46a5f2831d8e8e106a5b20c1cec40cf0c) --- Mathlib/Algebra/Lie/Abelian.lean | 3 ++- Mathlib/Data/Option/Defs.lean | 9 ++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Lie/Abelian.lean b/Mathlib/Algebra/Lie/Abelian.lean index e2e79f321b382..fda2508e872cf 100644 --- a/Mathlib/Algebra/Lie/Abelian.lean +++ b/Mathlib/Algebra/Lie/Abelian.lean @@ -90,7 +90,8 @@ theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : T theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] : 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₁ : 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 diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean index a2998ef365761..beadee9c6d259 100644 --- a/Mathlib/Data/Option/Defs.lean +++ b/Mathlib/Data/Option/Defs.lean @@ -103,13 +103,16 @@ 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 : α → α → α) [Std.Commutative f] : Std.Commutative (liftOrGet f) := +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 : α → α → α) [Std.Associative f] : Std.Associative (liftOrGet f) := +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 : α → α → α) [Std.IdempotentOp f] : Std.IdempotentOp (liftOrGet f) := +instance liftOrGet_isIdempotent (f : α → α → α) [Std.IdempotentOp f] : + Std.IdempotentOp (liftOrGet f) := ⟨fun a ↦ by cases a <;> simp [liftOrGet, Std.IdempotentOp.idempotent]⟩ instance liftOrGet_isId (f : α → α → α) : Std.LawfulIdentity (liftOrGet f) none where From 559bcffc03283af0429d608796ea177b9bb897e9 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 25 Jan 2024 17:49:09 +0100 Subject: [PATCH 3/5] Actually bump toolchain --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b39e2129f7686..8b9b7b255342d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-01-23 +leanprover/lean4:nightly-2024-01-25 From 69aa2b9f1c759ac2dc2f3c345dc4c40a00511d3b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 24 Jan 2024 19:25:15 +1100 Subject: [PATCH 4/5] merge lean-pr-testing-3060 (cherry picked from commit c100a1348c77ce500ed93bd31aca9f7b69dd7030) --- Mathlib/Tactic/TFAE.lean | 9 ++++++--- lean-toolchain | 2 +- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/TFAE.lean b/Mathlib/Tactic/TFAE.lean index 80cfbc9e87059..4594db66cf4d4 100644 --- a/Mathlib/Tactic/TFAE.lean +++ b/Mathlib/Tactic/TFAE.lean @@ -128,7 +128,8 @@ partial def proveChain (i : ℕ) (is : List ℕ) (P : Q(Prop)) (l : Q(List Prop) match l with | ~q([]) => return q(Chain.nil) | ~q($P' :: $l') => - let i' :: is' := is | unreachable! + -- `id` is a workaround for https://github.com/leanprover-community/quote4/issues/30 + let i' :: is' := id is | unreachable! have cl' : Q(Chain (· → ·) $P' $l') := ← proveChain i' is' q($P') q($l') let p ← proveImpl hyps atoms i i' P P' return q(Chain.cons $p $cl') @@ -139,7 +140,8 @@ partial def proveGetLastDImpl (i i' : ℕ) (is : List ℕ) (P P' : Q(Prop)) (l : match l with | ~q([]) => proveImpl hyps atoms i' i P' P | ~q($P'' :: $l') => - let i'' :: is' := is | unreachable! + -- `id` is a workaround for https://github.com/leanprover-community/quote4/issues/30 + let i'' :: is' := id is | unreachable! proveGetLastDImpl i i'' is' P P'' l' /-- Attempt to prove a statement of the form `TFAE [P₁, P₂, ...]`. -/ @@ -148,7 +150,8 @@ def proveTFAE (is : List ℕ) (l : Q(List Prop)) : MetaM Q(TFAE $l) := do | ~q([]) => return q(tfae_nil) | ~q([$P]) => return q(tfae_singleton $P) | ~q($P :: $P' :: $l') => - let i :: i' :: is' := is | unreachable! + -- `id` is a workaround for https://github.com/leanprover-community/quote4/issues/30 + let i :: i' :: is' := id is | unreachable! let c ← proveChain hyps atoms i (i'::is') P q($P' :: $l') let il ← proveGetLastDImpl hyps atoms i i' is' P P' l' return q(tfae_of_cycle $c $il) diff --git a/lean-toolchain b/lean-toolchain index b39e2129f7686..ec40378583fcc 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-01-23 +leanprover/lean4:nightly-2024-01-24 From 480765199b63094a32a567781f53919adf5f250d Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 30 Jan 2024 01:50:52 +1100 Subject: [PATCH 5/5] modify align; it's not exact, but hopefully helpful --- Mathlib/Data/Option/Defs.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean index beadee9c6d259..cf96c6dc38d95 100644 --- a/Mathlib/Data/Option/Defs.lean +++ b/Mathlib/Data/Option/Defs.lean @@ -119,12 +119,11 @@ instance liftOrGet_isId (f : α → α → α) : Std.LawfulIdentity (liftOrGet f 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 LawfulIdentity.toLeftIdentity ---#align option.lift_or_get_is_right_id LawfulIdentity.toLeftIdentity +#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 α