From e8b47c7d8dfc7cd2ce8ddd9d9b4eb7ae98065ec5 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 10 Jan 2024 17:13:57 +1100
Subject: [PATCH 01/15] chore: refactor of Algebra/Group/Defs to reduce imports

---
 Mathlib/Algebra/Abs.lean                      |  2 +-
 Mathlib/Algebra/CharZero/Defs.lean            |  1 +
 .../Algebra/CovariantAndContravariant.lean    |  3 +-
 Mathlib/Algebra/Group/Basic.lean              |  2 +-
 Mathlib/Algebra/Group/Cancel.lean             | 65 ++++++++++++++++++
 Mathlib/Algebra/Group/Classes.lean            | 29 ++++++++
 Mathlib/Algebra/Group/Commute/Defs.lean       |  1 +
 Mathlib/Algebra/Group/Defs.lean               | 68 ++-----------------
 Mathlib/Algebra/Group/Embedding.lean          |  2 +-
 Mathlib/Algebra/Group/Ext.lean                | 12 ++++
 Mathlib/Algebra/Group/Semiconj/Defs.lean      |  1 +
 Mathlib/Algebra/Group/WithOne/Defs.lean       |  1 +
 Mathlib/Algebra/GroupWithZero/Defs.lean       |  1 +
 Mathlib/Algebra/Invertible/Defs.lean          |  1 +
 Mathlib/CategoryTheory/Shift/Basic.lean       |  1 +
 Mathlib/Control/Functor.lean                  |  1 +
 Mathlib/Data/Bracket.lean                     |  2 +-
 Mathlib/Data/DList/Basic.lean                 |  2 +-
 Mathlib/Data/Option/Defs.lean                 |  1 +
 Mathlib/Data/Vector3.lean                     |  1 +
 Mathlib/GroupTheory/EckmannHilton.lean        |  1 +
 Mathlib/Init/Logic.lean                       |  1 +
 Mathlib/Init/Order/Defs.lean                  |  1 +
 Mathlib/Logic/Basic.lean                      |  1 +
 Mathlib/Logic/Nontrivial/Defs.lean            |  1 +
 Mathlib/Tactic/Basic.lean                     | 25 -------
 Mathlib/Tactic/Inhabit.lean                   |  2 +-
 Mathlib/Tactic/Lemma.lean                     | 16 +++++
 Mathlib/Tactic/MkIffOfInductiveProp.lean      |  2 +-
 Mathlib/Tactic/TypeStar.lean                  | 23 +++++++
 30 files changed, 175 insertions(+), 95 deletions(-)
 create mode 100644 Mathlib/Algebra/Group/Cancel.lean
 create mode 100644 Mathlib/Algebra/Group/Classes.lean
 create mode 100644 Mathlib/Tactic/Lemma.lean
 create mode 100644 Mathlib/Tactic/TypeStar.lean

diff --git a/Mathlib/Algebra/Abs.lean b/Mathlib/Algebra/Abs.lean
index 5c8563ced1599..f75b1e2ce9d6a 100644
--- a/Mathlib/Algebra/Abs.lean
+++ b/Mathlib/Algebra/Abs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
 import Mathlib.Mathport.Rename
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 
 #align_import algebra.abs from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 /-!
diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean
index 3653f16065358..03ac87801f1ef 100644
--- a/Mathlib/Algebra/CharZero/Defs.lean
+++ b/Mathlib/Algebra/CharZero/Defs.lean
@@ -7,6 +7,7 @@ import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Tactic.Cases
 import Mathlib.Algebra.NeZero
+import Mathlib.Logic.Function.Basic
 
 #align_import algebra.char_zero.defs from "leanprover-community/mathlib"@"d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d"
 
diff --git a/Mathlib/Algebra/CovariantAndContravariant.lean b/Mathlib/Algebra/CovariantAndContravariant.lean
index dbf7f5923f66d..82b135a279ed2 100644
--- a/Mathlib/Algebra/CovariantAndContravariant.lean
+++ b/Mathlib/Algebra/CovariantAndContravariant.lean
@@ -3,7 +3,8 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Algebra.Group.Defs
+import Mathlib.Algebra.Group.Cancel
+import Mathlib.Algebra.Group.Classes
 import Mathlib.Order.Basic
 import Mathlib.Order.Monotone.Basic
 
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index d0d014980160e..26a32801f6a5a 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Defs
+import Mathlib.Algebra.Group.Cancel
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.SplitIfs
diff --git a/Mathlib/Algebra/Group/Cancel.lean b/Mathlib/Algebra/Group/Cancel.lean
new file mode 100644
index 0000000000000..8868ab393a4cd
--- /dev/null
+++ b/Mathlib/Algebra/Group/Cancel.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
+-/
+import Mathlib.Algebra.Group.Defs
+import Mathlib.Logic.Function.Basic
+
+/-!
+# Facts about injectivity of cancellative multiplication.
+-/
+
+#align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
+
+universe u v w
+
+open Function
+
+variable {G : Type*} [Mul G]
+
+section IsLeftCancelMul
+
+variable [IsLeftCancelMul G] {a b c : G}
+
+@[to_additive]
+theorem mul_right_injective (a : G) : Injective (a * ·) := fun _ _ ↦ mul_left_cancel
+#align mul_right_injective mul_right_injective
+#align add_right_injective add_right_injective
+
+@[to_additive (attr := simp)]
+theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
+  (mul_right_injective a).eq_iff
+#align mul_right_inj mul_right_inj
+#align add_right_inj add_right_inj
+
+@[to_additive]
+theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c :=
+  (mul_right_injective a).ne_iff
+#align mul_ne_mul_right mul_ne_mul_right
+#align add_ne_add_right add_ne_add_right
+
+end IsLeftCancelMul
+
+section IsRightCancelMul
+
+variable [IsRightCancelMul G] {a b c : G}
+
+@[to_additive]
+theorem mul_left_injective (a : G) : Function.Injective (· * a) := fun _ _ ↦ mul_right_cancel
+#align mul_left_injective mul_left_injective
+#align add_left_injective add_left_injective
+
+@[to_additive (attr := simp)]
+theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
+  (mul_left_injective a).eq_iff
+#align mul_left_inj mul_left_inj
+#align add_left_inj add_left_inj
+
+@[to_additive]
+theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
+  (mul_left_injective a).ne_iff
+#align mul_ne_mul_left mul_ne_mul_left
+#align add_ne_add_left add_ne_add_left
+
+end IsRightCancelMul
diff --git a/Mathlib/Algebra/Group/Classes.lean b/Mathlib/Algebra/Group/Classes.lean
new file mode 100644
index 0000000000000..cb91830d3986b
--- /dev/null
+++ b/Mathlib/Algebra/Group/Classes.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
+-/
+import Mathlib.Algebra.Group.Defs
+import Mathlib.Init.Algebra.Classes
+
+/-!
+# Instances for operations in algebraic structures.
+
+As the unbundle algebraic structures typeclasses are of somewhat dubious use at present,
+we separate out the file providing instances from the main `Mathlib.Algebra.Group.Defs` file.
+-/
+
+#align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
+
+variable {G : Type*}
+
+@[to_additive]
+instance Semigroup.to_isAssociative [Semigroup G] : IsAssociative G (· * ·) :=
+  ⟨mul_assoc⟩
+#align semigroup.to_is_associative Semigroup.to_isAssociative
+#align add_semigroup.to_is_associative AddSemigroup.to_isAssociative
+
+@[to_additive]
+instance CommMagma.to_isCommutative [CommMagma G] : IsCommutative 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/Commute/Defs.lean b/Mathlib/Algebra/Group/Commute/Defs.lean
index 0cf1cc337e983..6eec9dda92d2a 100644
--- a/Mathlib/Algebra/Group/Commute/Defs.lean
+++ b/Mathlib/Algebra/Group/Commute/Defs.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Neil Strickland. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Neil Strickland, Yury Kudryashov
 -/
+import Mathlib.Init.Algebra.Classes
 import Mathlib.Algebra.Group.Semiconj.Defs
 
 #align_import algebra.group.commute from "leanprover-community/mathlib"@"05101c3df9d9cfe9430edc205860c79b6d660102"
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index 5871222cc782d..acf27030f2c2b 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -5,8 +5,9 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 import Mathlib.Init.ZeroOne
 import Mathlib.Init.Data.Int.Basic
-import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Basic
+-- import Mathlib.Logic.Function.Basic
+import Mathlib.Tactic.Lemma
+import Mathlib.Tactic.TypeStar
 
 #align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
@@ -220,27 +221,10 @@ theorem mul_left_cancel : a * b = a * c → b = c :=
 
 @[to_additive]
 theorem mul_left_cancel_iff : a * b = a * c ↔ b = c :=
-  ⟨mul_left_cancel, congr_arg _⟩
+  ⟨mul_left_cancel, congrArg _⟩
 #align mul_left_cancel_iff mul_left_cancel_iff
 #align add_left_cancel_iff add_left_cancel_iff
 
-@[to_additive]
-theorem mul_right_injective (a : G) : Injective (a * ·) := fun _ _ ↦ mul_left_cancel
-#align mul_right_injective mul_right_injective
-#align add_right_injective add_right_injective
-
-@[to_additive (attr := simp)]
-theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
-  (mul_right_injective a).eq_iff
-#align mul_right_inj mul_right_inj
-#align add_right_inj add_right_inj
-
-@[to_additive]
-theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c :=
-  (mul_right_injective a).ne_iff
-#align mul_ne_mul_right mul_ne_mul_right
-#align add_ne_add_right add_ne_add_right
-
 end IsLeftCancelMul
 
 section IsRightCancelMul
@@ -255,27 +239,10 @@ theorem mul_right_cancel : a * b = c * b → a = c :=
 
 @[to_additive]
 theorem mul_right_cancel_iff : b * a = c * a ↔ b = c :=
-  ⟨mul_right_cancel, congr_arg (· * a)⟩
+  ⟨mul_right_cancel, congrArg (· * a)⟩
 #align mul_right_cancel_iff mul_right_cancel_iff
 #align add_right_cancel_iff add_right_cancel_iff
 
-@[to_additive]
-theorem mul_left_injective (a : G) : Function.Injective (· * a) := fun _ _ ↦ mul_right_cancel
-#align mul_left_injective mul_left_injective
-#align add_left_injective add_left_injective
-
-@[to_additive (attr := simp)]
-theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
-  (mul_left_injective a).eq_iff
-#align mul_left_inj mul_left_inj
-#align add_left_inj add_left_inj
-
-@[to_additive]
-theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
-  (mul_left_injective a).ne_iff
-#align mul_ne_mul_left mul_ne_mul_left
-#align add_ne_add_left add_ne_add_left
-
 end IsRightCancelMul
 
 end Mul
@@ -310,12 +277,6 @@ theorem mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) :=
 #align mul_assoc mul_assoc
 #align add_assoc add_assoc
 
-@[to_additive]
-instance Semigroup.to_isAssociative : IsAssociative G (· * ·) :=
-  ⟨mul_assoc⟩
-#align semigroup.to_is_associative Semigroup.to_isAssociative
-#align add_semigroup.to_is_associative AddSemigroup.to_isAssociative
-
 end Semigroup
 
 /-- A commutative addition is a type with an addition which commutes-/
@@ -358,11 +319,6 @@ theorem mul_comm : ∀ a b : G, a * b = b * a := CommMagma.mul_comm
 #align mul_comm mul_comm
 #align add_comm add_comm
 
-@[to_additive]
-instance CommMagma.to_isCommutative : IsCommutative G (· * ·) := ⟨mul_comm⟩
-#align comm_semigroup.to_is_commutative CommMagma.to_isCommutative
-#align add_comm_semigroup.to_is_commutative AddCommMagma.to_isCommutative
-
 /-- Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsLeftCancelMul G`. -/
 @[to_additive AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd "Any `AddCommMagma G` that satisfies
 `IsRightCancelAdd G` also satisfies `IsLeftCancelAdd G`."]
@@ -992,7 +948,7 @@ theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
   | 0 => (zpow_zero _).trans (pow_zero _).symm
   | n + 1 => calc
     a ^ (↑(n + 1) : ℤ) = a * a ^ (n : ℤ) := DivInvMonoid.zpow_succ' _ _
-    _ = a * a ^ n := congr_arg (a * ·) (zpow_ofNat a n)
+    _ = a * a ^ n := congrArg (a * ·) (zpow_ofNat a n)
     _ = a ^ (n + 1) := (pow_succ _ _).symm
 #align zpow_coe_nat zpow_ofNat
 #align zpow_of_nat zpow_ofNat
@@ -1230,12 +1186,6 @@ instance (priority := 100) Group.toCancelMonoid : CancelMonoid G :=
 
 end Group
 
-@[to_additive]
-theorem Group.toDivInvMonoid_injective {G : Type*} :
-    Function.Injective (@Group.toDivInvMonoid G) := by rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
-#align group.to_div_inv_monoid_injective Group.toDivInvMonoid_injective
-#align add_group.to_sub_neg_add_monoid_injective AddGroup.toSubNegAddMonoid_injective
-
 /-- An additive commutative group is an additive group with commutative `(+)`. -/
 class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
 #align add_comm_group AddCommGroup
@@ -1247,12 +1197,6 @@ class CommGroup (G : Type u) extends Group G, CommMonoid G
 
 attribute [to_additive existing] CommGroup.toCommMonoid
 
-@[to_additive]
-theorem CommGroup.toGroup_injective {G : Type u} : Function.Injective (@CommGroup.toGroup G) := by
-  rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
-#align comm_group.to_group_injective CommGroup.toGroup_injective
-#align add_comm_group.to_add_group_injective AddCommGroup.toAddGroup_injective
-
 section CommGroup
 
 variable [CommGroup G]
diff --git a/Mathlib/Algebra/Group/Embedding.lean b/Mathlib/Algebra/Group/Embedding.lean
index 201064e794f6f..a1376a6c117d1 100644
--- a/Mathlib/Algebra/Group/Embedding.lean
+++ b/Mathlib/Algebra/Group/Embedding.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Algebra.Group.Defs
+import Mathlib.Algebra.Group.Cancel
 import Mathlib.Logic.Embedding.Basic
 
 #align_import algebra.hom.embedding from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean
index 73e8643a4473c..55ac1f1b5ced3 100644
--- a/Mathlib/Algebra/Group/Ext.lean
+++ b/Mathlib/Algebra/Group/Ext.lean
@@ -152,6 +152,12 @@ theorem DivInvMonoid.ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄
 #align div_inv_monoid.ext DivInvMonoid.ext
 #align sub_neg_monoid.ext SubNegMonoid.ext
 
+@[to_additive]
+theorem Group.toDivInvMonoid_injective {G : Type*} :
+    Function.Injective (@Group.toDivInvMonoid G) := by rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
+#align group.to_div_inv_monoid_injective Group.toDivInvMonoid_injective
+#align add_group.to_sub_neg_add_monoid_injective AddGroup.toSubNegAddMonoid_injective
+
 @[to_additive (attr := ext)]
 theorem Group.ext {G : Type*} ⦃g₁ g₂ : Group G⦄ (h_mul : g₁.mul = g₂.mul) : g₁ = g₂ := by
   have h₁ : g₁.one = g₂.one := congr_arg (·.one) (Monoid.ext h_mul)
@@ -165,6 +171,12 @@ theorem Group.ext {G : Type*} ⦃g₁ g₂ : Group G⦄ (h_mul : g₁.mul = g₂
 #align group.ext Group.ext
 #align add_group.ext AddGroup.ext
 
+@[to_additive]
+theorem CommGroup.toGroup_injective {G : Type u} : Function.Injective (@CommGroup.toGroup G) := by
+  rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
+#align comm_group.to_group_injective CommGroup.toGroup_injective
+#align add_comm_group.to_add_group_injective AddCommGroup.toAddGroup_injective
+
 @[to_additive (attr := ext)]
 theorem CommGroup.ext {G : Type*} ⦃g₁ g₂ : CommGroup G⦄ (h_mul : g₁.mul = g₂.mul) : g₁ = g₂ :=
   CommGroup.toGroup_injective <| Group.ext h_mul
diff --git a/Mathlib/Algebra/Group/Semiconj/Defs.lean b/Mathlib/Algebra/Group/Semiconj/Defs.lean
index f1e617cc8fdbe..5926e54c5d6fa 100644
--- a/Mathlib/Algebra/Group/Semiconj/Defs.lean
+++ b/Mathlib/Algebra/Group/Semiconj/Defs.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 
 Some proofs and docs came from `algebra/commute` (c) Neil Strickland
 -/
+import Mathlib.Init.Logic
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Tactic.Cases
 
diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean
index 41cc2435e9b3d..4c79ab6ef0480 100644
--- a/Mathlib/Algebra/Group/WithOne/Defs.lean
+++ b/Mathlib/Algebra/Group/WithOne/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
 -/
 import Mathlib.Order.WithBot
+import Mathlib.Algebra.Group.Classes
 import Mathlib.Algebra.Ring.Defs
 
 #align_import algebra.group.with_one.defs from "leanprover-community/mathlib"@"995b47e555f1b6297c7cf16855f1023e355219fb"
diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
index ce855a2e4e948..0a3f8d4f23f36 100644
--- a/Mathlib/Algebra/GroupWithZero/Defs.lean
+++ b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Logic.Nontrivial.Defs
+import Mathlib.Logic.Function.Basic
 
 #align_import algebra.group_with_zero.defs from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"
 
diff --git a/Mathlib/Algebra/Invertible/Defs.lean b/Mathlib/Algebra/Invertible/Defs.lean
index e2c27988ece5e..e2620a07e4e08 100644
--- a/Mathlib/Algebra/Invertible/Defs.lean
+++ b/Mathlib/Algebra/Invertible/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Logic.Basic
 
 #align_import algebra.invertible from "leanprover-community/mathlib"@"722b3b152ddd5e0cf21c0a29787c76596cb6b422"
 
diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean
index d09a2d1a1cea1..70878977e751b 100644
--- a/Mathlib/CategoryTheory/Shift/Basic.lean
+++ b/Mathlib/CategoryTheory/Shift/Basic.lean
@@ -6,6 +6,7 @@ Authors: Scott Morrison, Johan Commelin, Andrew Yang
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
 import Mathlib.CategoryTheory.Monoidal.End
 import Mathlib.CategoryTheory.Monoidal.Discrete
+import Mathlib.Algebra.Group.Cancel
 
 #align_import category_theory.shift.basic from "leanprover-community/mathlib"@"6876fa15e3158ff3e4a4e2af1fb6e1945c6e8803"
 
diff --git a/Mathlib/Control/Functor.lean b/Mathlib/Control/Functor.lean
index df9c171e3c2a7..b93a4c910b199 100644
--- a/Mathlib/Control/Functor.lean
+++ b/Mathlib/Control/Functor.lean
@@ -6,6 +6,7 @@ Authors: Simon Hudon
 import Mathlib.Control.Basic
 import Mathlib.Init.Set
 import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 import Std.Tactic.Lint
 
 #align_import control.functor from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
diff --git a/Mathlib/Data/Bracket.lean b/Mathlib/Data/Bracket.lean
index db726be4ed98b..4d3fee3f79801 100644
--- a/Mathlib/Data/Bracket.lean
+++ b/Mathlib/Data/Bracket.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Lutz, Oliver Nash
 -/
 import Mathlib.Mathport.Rename
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 
 #align_import data.bracket from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 
diff --git a/Mathlib/Data/DList/Basic.lean b/Mathlib/Data/DList/Basic.lean
index 0ab79b30fb993..b300ca5bfd300 100644
--- a/Mathlib/Data/DList/Basic.lean
+++ b/Mathlib/Data/DList/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
 import Mathlib.Data.DList.Defs
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 
 #align_import data.dlist.basic from "leanprover-community/mathlib"@"d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d"
 
diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean
index 7d315c0c52ce9..8ad18723f50b3 100644
--- a/Mathlib/Data/Option/Defs.lean
+++ b/Mathlib/Data/Option/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Init.Algebra.Classes
+import Mathlib.Tactic.TypeStar
 
 #align_import data.option.defs from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 
diff --git a/Mathlib/Data/Vector3.lean b/Mathlib/Data/Vector3.lean
index c7b1c0fbb2f1f..c57e3fc8f2c16 100644
--- a/Mathlib/Data/Vector3.lean
+++ b/Mathlib/Data/Vector3.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathlib.Data.Fin.Fin2
 import Mathlib.Init.Align
 import Mathlib.Mathport.Notation
+import Mathlib.Tactic.TypeStar
 
 #align_import data.vector3 from "leanprover-community/mathlib"@"3d7987cda72abc473c7cdbbb075170e9ac620042"
 
diff --git a/Mathlib/GroupTheory/EckmannHilton.lean b/Mathlib/GroupTheory/EckmannHilton.lean
index d9cd17e0f947f..913d850b6fffb 100644
--- a/Mathlib/GroupTheory/EckmannHilton.lean
+++ b/Mathlib/GroupTheory/EckmannHilton.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau, Robert Y. Lewis
 -/
+import Mathlib.Init.Algebra.Classes
 import Mathlib.Algebra.Group.Defs
 
 #align_import group_theory.eckmann_hilton from "leanprover-community/mathlib"@"41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3"
diff --git a/Mathlib/Init/Logic.lean b/Mathlib/Init/Logic.lean
index aebf2e759b59f..648ac5ba2cea4 100644
--- a/Mathlib/Init/Logic.lean
+++ b/Mathlib/Init/Logic.lean
@@ -9,6 +9,7 @@ import Std.Tactic.Relation.Rfl
 import Std.Logic
 import Std.WF
 import Mathlib.Tactic.Basic
+import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Mathport.Attributes
 import Mathlib.Mathport.Rename
diff --git a/Mathlib/Init/Order/Defs.lean b/Mathlib/Init/Order/Defs.lean
index c0f97b9393654..719b8ff63b533 100644
--- a/Mathlib/Init/Order/Defs.lean
+++ b/Mathlib/Init/Order/Defs.lean
@@ -7,6 +7,7 @@ import Mathlib.Mathport.Rename
 import Mathlib.Init.Algebra.Classes
 import Mathlib.Init.Data.Ordering.Basic
 import Mathlib.Tactic.SplitIfs
+import Mathlib.Tactic.TypeStar
 
 #align_import init.algebra.order from "leanprover-community/lean"@"c2bcdbcbe741ed37c361a30d38e179182b989f76"
 
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index 7636444aa89e1..9fe26474f7942 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Init.Logic
 import Mathlib.Init.Function
 import Mathlib.Init.Algebra.Classes
 import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 import Std.Util.LibraryNote
 import Std.Tactic.Lint.Basic
 
diff --git a/Mathlib/Logic/Nontrivial/Defs.lean b/Mathlib/Logic/Nontrivial/Defs.lean
index f9cebabe09c90..9e09be39f19a3 100644
--- a/Mathlib/Logic/Nontrivial/Defs.lean
+++ b/Mathlib/Logic/Nontrivial/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Init.Function
+import Mathlib.Tactic.TypeStar
 
 #align_import logic.nontrivial from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
diff --git a/Mathlib/Tactic/Basic.lean b/Mathlib/Tactic/Basic.lean
index 5a1a3f5a3ff74..2c572ea57d944 100644
--- a/Mathlib/Tactic/Basic.lean
+++ b/Mathlib/Tactic/Basic.lean
@@ -21,31 +21,6 @@ syntax (name := «variables») "variables" (ppSpace bracketedBinder)* : command
     elabVariable (← `(variable%$pos $binders*))
   | _ => throwUnsupportedSyntax
 
-/-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems -/
-syntax (name := lemma) declModifiers
-  group("lemma " declId ppIndent(declSig) declVal Parser.Command.terminationSuffix) : command
-
-/-- Implementation of the `lemma` command, by macro expansion to `theorem`. -/
-@[macro «lemma»] def expandLemma : Macro := fun stx =>
-  -- FIXME: this should be a macro match, but terminationSuffix is not easy to bind correctly.
-  -- This implementation ensures that any future changes to `theorem` are reflected in `lemma`
-  let stx := stx.modifyArg 1 fun stx =>
-    let stx := stx.modifyArg 0 (mkAtomFrom · "theorem" (canonical := true))
-    stx.setKind ``Parser.Command.theorem
-  pure <| stx.setKind ``Parser.Command.declaration
-
-/-- The syntax `variable (X Y ... Z : Sort*)` creates a new distinct implicit universe variable
-for each variable in the sequence. -/
-elab "Sort*" : term => do
-  let u ← Lean.Meta.mkFreshLevelMVar
-  Elab.Term.levelMVarToParam (.sort u)
-
-/-- The syntax `variable (X Y ... Z : Type*)` creates a new distinct implicit universe variable
-`> 0` for each variable in the sequence. -/
-elab "Type*" : term => do
-  let u ← Lean.Meta.mkFreshLevelMVar
-  Elab.Term.levelMVarToParam (.sort (.succ u))
-
 /-- Given two arrays of `FVarId`s, one from an old local context and the other from a new local
 context, pushes `FVarAliasInfo`s into the info tree for corresponding pairs of `FVarId`s.
 Recall that variables linked this way should be considered to be semantically identical.
diff --git a/Mathlib/Tactic/Inhabit.lean b/Mathlib/Tactic/Inhabit.lean
index b4a2a6fd08b5a..daa5b484d6c1e 100644
--- a/Mathlib/Tactic/Inhabit.lean
+++ b/Mathlib/Tactic/Inhabit.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joshua Clune
 -/
 import Lean
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 
 /-!
 Defines the `inhabit α` tactic, which tries to construct an `Inhabited α` instance,
diff --git a/Mathlib/Tactic/Lemma.lean b/Mathlib/Tactic/Lemma.lean
new file mode 100644
index 0000000000000..d4ee68e01f659
--- /dev/null
+++ b/Mathlib/Tactic/Lemma.lean
@@ -0,0 +1,16 @@
+import Lean.Parser.Command
+
+open Lean
+
+/-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems -/
+syntax (name := lemma) declModifiers
+  group("lemma " declId ppIndent(declSig) declVal Parser.Command.terminationSuffix) : command
+
+/-- Implementation of the `lemma` command, by macro expansion to `theorem`. -/
+@[macro «lemma»] def expandLemma : Macro := fun stx =>
+  -- FIXME: this should be a macro match, but terminationSuffix is not easy to bind correctly.
+  -- This implementation ensures that any future changes to `theorem` are reflected in `lemma`
+  let stx := stx.modifyArg 1 fun stx =>
+    let stx := stx.modifyArg 0 (mkAtomFrom · "theorem" (canonical := true))
+    stx.setKind ``Parser.Command.theorem
+  pure <| stx.setKind ``Parser.Command.declaration
diff --git a/Mathlib/Tactic/MkIffOfInductiveProp.lean b/Mathlib/Tactic/MkIffOfInductiveProp.lean
index 6efae87acb7bc..94caf2862cb03 100644
--- a/Mathlib/Tactic/MkIffOfInductiveProp.lean
+++ b/Mathlib/Tactic/MkIffOfInductiveProp.lean
@@ -7,7 +7,7 @@ import Lean
 import Std.Tactic.LeftRight
 import Mathlib.Lean.Meta
 import Mathlib.Lean.Name
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 
 /-!
 # mk_iff_of_inductive_prop
diff --git a/Mathlib/Tactic/TypeStar.lean b/Mathlib/Tactic/TypeStar.lean
new file mode 100644
index 0000000000000..433fc680a2649
--- /dev/null
+++ b/Mathlib/Tactic/TypeStar.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2023 Matthew Ballard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matthew Ballard
+-/
+import Lean
+import Std
+import Mathlib.Tactic.PPWithUniv
+import Mathlib.Tactic.ExtendDoc
+
+open Lean
+
+/-- The syntax `variable (X Y ... Z : Sort*)` creates a new distinct implicit universe variable
+for each variable in the sequence. -/
+elab "Sort*" : term => do
+  let u ← Lean.Meta.mkFreshLevelMVar
+  Elab.Term.levelMVarToParam (.sort u)
+
+/-- The syntax `variable (X Y ... Z : Type*)` creates a new distinct implicit universe variable
+`> 0` for each variable in the sequence. -/
+elab "Type*" : term => do
+  let u ← Lean.Meta.mkFreshLevelMVar
+  Elab.Term.levelMVarToParam (.sort (.succ u))

From 364c7ad5ada3a656c202e00f3e3904c7d68254a5 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 10 Jan 2024 17:18:24 +1100
Subject: [PATCH 02/15] cleanup

---
 Mathlib/Algebra/Group/Defs.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index acf27030f2c2b..1eab2dce6cea4 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -3,9 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
-import Mathlib.Init.ZeroOne
 import Mathlib.Init.Data.Int.Basic
--- import Mathlib.Logic.Function.Basic
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.TypeStar
 

From 3708d35fcfd6ee2da1d01b982c87424193b1af2e Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 10 Jan 2024 18:04:04 +1100
Subject: [PATCH 03/15] add module doc

---
 Mathlib/Tactic/Lemma.lean    | 9 +++++++++
 Mathlib/Tactic/TypeStar.lean | 6 ++++++
 2 files changed, 15 insertions(+)

diff --git a/Mathlib/Tactic/Lemma.lean b/Mathlib/Tactic/Lemma.lean
index d4ee68e01f659..d5187b04f16f1 100644
--- a/Mathlib/Tactic/Lemma.lean
+++ b/Mathlib/Tactic/Lemma.lean
@@ -1,5 +1,14 @@
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Kyle Miller
+-/
 import Lean.Parser.Command
 
+/-!
+# Support for `lemma` as a synonym for `theorem`.
+-/
+
 open Lean
 
 /-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems -/
diff --git a/Mathlib/Tactic/TypeStar.lean b/Mathlib/Tactic/TypeStar.lean
index 433fc680a2649..50dc1a4f01c46 100644
--- a/Mathlib/Tactic/TypeStar.lean
+++ b/Mathlib/Tactic/TypeStar.lean
@@ -8,6 +8,12 @@ import Std
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.ExtendDoc
 
+/-!
+# Support for `Sort*` and `Type*`.
+
+These elaborate as `Sort u` and `Type u` with a fresh implicit universe variable `u`.
+-/
+
 open Lean
 
 /-- The syntax `variable (X Y ... Z : Sort*)` creates a new distinct implicit universe variable

From a42bf4a6f30c0f3c930735b5dcde1467dd5b2e74 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 10 Jan 2024 18:07:21 +1100
Subject: [PATCH 04/15] .

---
 Mathlib.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 4cb013b926fbc..00e761ccb5e01 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -168,6 +168,8 @@ import Mathlib.Algebra.GradedMonoid
 import Mathlib.Algebra.GradedMulAction
 import Mathlib.Algebra.Group.Aut
 import Mathlib.Algebra.Group.Basic
+import Mathlib.Algebra.Group.Cancel
+import Mathlib.Algebra.Group.Classes
 import Mathlib.Algebra.Group.Commutator
 import Mathlib.Algebra.Group.Commute.Basic
 import Mathlib.Algebra.Group.Commute.Defs
@@ -3346,6 +3348,7 @@ import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
+import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.LiftLets
@@ -3447,6 +3450,7 @@ import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
 import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
+import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.UnsetOption
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.Variable

From 57f470deea9af1178e7183f8f22c46bcaf7a1865 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 10 Jan 2024 18:09:40 +1100
Subject: [PATCH 05/15] import all

---
 Mathlib/Tactic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 19af921d915fd..9e17126b806c1 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -68,6 +68,7 @@ import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
+import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.LiftLets
@@ -169,6 +170,7 @@ import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
 import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
+import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.UnsetOption
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.Variable

From ee102fe8970f48dc2f8b5e883b268fc1e49e16e7 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 10 Jan 2024 20:26:37 +1100
Subject: [PATCH 06/15] fix test

---
 test/ImplicitUniverses.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/ImplicitUniverses.lean b/test/ImplicitUniverses.lean
index b7a8b604613a0..01782ba761cfe 100644
--- a/test/ImplicitUniverses.lean
+++ b/test/ImplicitUniverses.lean
@@ -1,4 +1,4 @@
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.SuccessIfFailWithMsg
 
 private axiom test_sorry : ∀ {α}, α

From beb8163e3846ebb78e917777f38a207e0340e1c5 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Thu, 11 Jan 2024 12:02:14 +1100
Subject: [PATCH 07/15] Apply suggestions from code review

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
---
 Mathlib/Algebra/Group/Classes.lean       | 2 +-
 Mathlib/Algebra/Group/Semiconj/Defs.lean | 2 +-
 Mathlib/Algebra/GroupWithZero/Defs.lean  | 2 +-
 Mathlib/CategoryTheory/Shift/Basic.lean  | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Algebra/Group/Classes.lean b/Mathlib/Algebra/Group/Classes.lean
index cb91830d3986b..ebf61a84eb898 100644
--- a/Mathlib/Algebra/Group/Classes.lean
+++ b/Mathlib/Algebra/Group/Classes.lean
@@ -9,7 +9,7 @@ import Mathlib.Init.Algebra.Classes
 /-!
 # Instances for operations in algebraic structures.
 
-As the unbundle algebraic structures typeclasses are of somewhat dubious use at present,
+As the unbundled algebraic structures typeclasses are of somewhat dubious use at present,
 we separate out the file providing instances from the main `Mathlib.Algebra.Group.Defs` file.
 -/
 
diff --git a/Mathlib/Algebra/Group/Semiconj/Defs.lean b/Mathlib/Algebra/Group/Semiconj/Defs.lean
index 5926e54c5d6fa..bcd2698ed13bd 100644
--- a/Mathlib/Algebra/Group/Semiconj/Defs.lean
+++ b/Mathlib/Algebra/Group/Semiconj/Defs.lean
@@ -5,8 +5,8 @@ Authors: Yury Kudryashov
 
 Some proofs and docs came from `algebra/commute` (c) Neil Strickland
 -/
-import Mathlib.Init.Logic
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Init.Logic
 import Mathlib.Tactic.Cases
 
 #align_import algebra.group.semiconj from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
index 0a3f8d4f23f36..ab87a0d095187 100644
--- a/Mathlib/Algebra/GroupWithZero/Defs.lean
+++ b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.Defs
-import Mathlib.Logic.Nontrivial.Defs
 import Mathlib.Logic.Function.Basic
+import Mathlib.Logic.Nontrivial.Defs
 
 #align_import algebra.group_with_zero.defs from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"
 
diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean
index 70878977e751b..bfe9e26fb23d8 100644
--- a/Mathlib/CategoryTheory/Shift/Basic.lean
+++ b/Mathlib/CategoryTheory/Shift/Basic.lean
@@ -3,10 +3,10 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johan Commelin, Andrew Yang
 -/
+import Mathlib.Algebra.Group.Cancel
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
 import Mathlib.CategoryTheory.Monoidal.End
 import Mathlib.CategoryTheory.Monoidal.Discrete
-import Mathlib.Algebra.Group.Cancel
 
 #align_import category_theory.shift.basic from "leanprover-community/mathlib"@"6876fa15e3158ff3e4a4e2af1fb6e1945c6e8803"
 

From fc94448be1ec6f17557213d7c6a924bb4669b78c Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 11 Jan 2024 12:06:00 +1100
Subject: [PATCH 08/15] import Tactic.TypeStar and Tactic.Lemma in Tactic.Basic

---
 Mathlib/Algebra/Group/Defs.lean | 2 ++
 Mathlib/Control/Functor.lean    | 1 -
 Mathlib/Data/Option/Defs.lean   | 1 -
 Mathlib/Data/Vector3.lean       | 1 -
 Mathlib/Init/Logic.lean         | 1 -
 Mathlib/Tactic/Basic.lean       | 2 ++
 6 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index 1eab2dce6cea4..eea75a562b8ff 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -1259,3 +1259,5 @@ initialize_simps_projections Group
 initialize_simps_projections AddGroup
 initialize_simps_projections CommGroup
 initialize_simps_projections AddCommGroup
+
+assert_not_exists Function.Injective
diff --git a/Mathlib/Control/Functor.lean b/Mathlib/Control/Functor.lean
index b93a4c910b199..df9c171e3c2a7 100644
--- a/Mathlib/Control/Functor.lean
+++ b/Mathlib/Control/Functor.lean
@@ -6,7 +6,6 @@ Authors: Simon Hudon
 import Mathlib.Control.Basic
 import Mathlib.Init.Set
 import Mathlib.Tactic.Basic
-import Mathlib.Tactic.TypeStar
 import Std.Tactic.Lint
 
 #align_import control.functor from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean
index 8ad18723f50b3..7d315c0c52ce9 100644
--- a/Mathlib/Data/Option/Defs.lean
+++ b/Mathlib/Data/Option/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Init.Algebra.Classes
-import Mathlib.Tactic.TypeStar
 
 #align_import data.option.defs from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 
diff --git a/Mathlib/Data/Vector3.lean b/Mathlib/Data/Vector3.lean
index c57e3fc8f2c16..c7b1c0fbb2f1f 100644
--- a/Mathlib/Data/Vector3.lean
+++ b/Mathlib/Data/Vector3.lean
@@ -6,7 +6,6 @@ Authors: Mario Carneiro
 import Mathlib.Data.Fin.Fin2
 import Mathlib.Init.Align
 import Mathlib.Mathport.Notation
-import Mathlib.Tactic.TypeStar
 
 #align_import data.vector3 from "leanprover-community/mathlib"@"3d7987cda72abc473c7cdbbb075170e9ac620042"
 
diff --git a/Mathlib/Init/Logic.lean b/Mathlib/Init/Logic.lean
index 648ac5ba2cea4..aebf2e759b59f 100644
--- a/Mathlib/Init/Logic.lean
+++ b/Mathlib/Init/Logic.lean
@@ -9,7 +9,6 @@ import Std.Tactic.Relation.Rfl
 import Std.Logic
 import Std.WF
 import Mathlib.Tactic.Basic
-import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Mathport.Attributes
 import Mathlib.Mathport.Rename
diff --git a/Mathlib/Tactic/Basic.lean b/Mathlib/Tactic/Basic.lean
index 2c572ea57d944..5773d41dcf83b 100644
--- a/Mathlib/Tactic/Basic.lean
+++ b/Mathlib/Tactic/Basic.lean
@@ -7,6 +7,8 @@ import Lean
 import Std
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.ExtendDoc
+import Mathlib.Tactic.Lemma
+import Mathlib.Tactic.TypeStar
 
 set_option autoImplicit true
 

From ecddcee954ba4ce3d9e28e1aef2ba79543f2c4c9 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 11 Jan 2024 12:07:42 +1100
Subject: [PATCH 09/15] import assert_not_exists

---
 Mathlib/Algebra/Group/Defs.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index eea75a562b8ff..df269ecea06ec 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.TypeStar
+import Mathlib.Util.AssertExists
 
 #align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
@@ -1261,3 +1262,4 @@ initialize_simps_projections CommGroup
 initialize_simps_projections AddCommGroup
 
 assert_not_exists Function.Injective
+assert_not_exists IsCommutative

From 3fd2844a3bba45482ad0a932325c0fee554b1245 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 11 Jan 2024 12:09:51 +1100
Subject: [PATCH 10/15] cleanup

---
 Mathlib/Logic/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index 9fe26474f7942..7636444aa89e1 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -7,7 +7,6 @@ import Mathlib.Init.Logic
 import Mathlib.Init.Function
 import Mathlib.Init.Algebra.Classes
 import Mathlib.Tactic.Basic
-import Mathlib.Tactic.TypeStar
 import Std.Util.LibraryNote
 import Std.Tactic.Lint.Basic
 

From 04524bc1cf2d57ec9d8d83b1e6881b470c1fc8e6 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 11 Jan 2024 12:56:49 +1100
Subject: [PATCH 11/15] =?UTF-8?q?move=20lemmas=20into=20Group/Basic=20per?=
 =?UTF-8?q?=20Ya=C3=ABl's=20request?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib.lean                                  |  1 -
 .../Algebra/CovariantAndContravariant.lean    |  2 +-
 Mathlib/Algebra/Group/Basic.lean              | 49 +++++++++++++-
 Mathlib/Algebra/Group/Cancel.lean             | 65 -------------------
 Mathlib/Algebra/Group/Embedding.lean          |  2 +-
 Mathlib/CategoryTheory/Shift/Basic.lean       |  2 +-
 6 files changed, 51 insertions(+), 70 deletions(-)
 delete mode 100644 Mathlib/Algebra/Group/Cancel.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 00e761ccb5e01..f4444d39fb9b0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -168,7 +168,6 @@ import Mathlib.Algebra.GradedMonoid
 import Mathlib.Algebra.GradedMulAction
 import Mathlib.Algebra.Group.Aut
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Group.Cancel
 import Mathlib.Algebra.Group.Classes
 import Mathlib.Algebra.Group.Commutator
 import Mathlib.Algebra.Group.Commute.Basic
diff --git a/Mathlib/Algebra/CovariantAndContravariant.lean b/Mathlib/Algebra/CovariantAndContravariant.lean
index 82b135a279ed2..bd5804fa88772 100644
--- a/Mathlib/Algebra/CovariantAndContravariant.lean
+++ b/Mathlib/Algebra/CovariantAndContravariant.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Algebra.Group.Cancel
+import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Classes
 import Mathlib.Order.Basic
 import Mathlib.Order.Monotone.Basic
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index 26a32801f6a5a..f4e563fa1ab48 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -3,7 +3,8 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Cancel
+import Mathlib.Algebra.Group.Defs
+import Mathlib.Logic.Function.Basic
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.SplitIfs
@@ -25,6 +26,52 @@ universe u
 
 variable {α β G : Type*}
 
+section IsLeftCancelMul
+
+variable [Mul G] [IsLeftCancelMul G]
+
+@[to_additive]
+theorem mul_right_injective (a : G) : Injective (a * ·) := fun _ _ ↦ mul_left_cancel
+#align mul_right_injective mul_right_injective
+#align add_right_injective add_right_injective
+
+@[to_additive (attr := simp)]
+theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
+  (mul_right_injective a).eq_iff
+#align mul_right_inj mul_right_inj
+#align add_right_inj add_right_inj
+
+@[to_additive]
+theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c :=
+  (mul_right_injective a).ne_iff
+#align mul_ne_mul_right mul_ne_mul_right
+#align add_ne_add_right add_ne_add_right
+
+end IsLeftCancelMul
+
+section IsRightCancelMul
+
+variable [Mul G] [IsRightCancelMul G]
+
+@[to_additive]
+theorem mul_left_injective (a : G) : Function.Injective (· * a) := fun _ _ ↦ mul_right_cancel
+#align mul_left_injective mul_left_injective
+#align add_left_injective add_left_injective
+
+@[to_additive (attr := simp)]
+theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
+  (mul_left_injective a).eq_iff
+#align mul_left_inj mul_left_inj
+#align add_left_inj add_left_inj
+
+@[to_additive]
+theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
+  (mul_left_injective a).ne_iff
+#align mul_ne_mul_left mul_ne_mul_left
+#align add_ne_add_left add_ne_add_left
+
+end IsRightCancelMul
+
 section Semigroup
 
 /-- Composing two multiplications on the left by `y` then `x`
diff --git a/Mathlib/Algebra/Group/Cancel.lean b/Mathlib/Algebra/Group/Cancel.lean
deleted file mode 100644
index 8868ab393a4cd..0000000000000
--- a/Mathlib/Algebra/Group/Cancel.lean
+++ /dev/null
@@ -1,65 +0,0 @@
-/-
-Copyright (c) 2014 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
--/
-import Mathlib.Algebra.Group.Defs
-import Mathlib.Logic.Function.Basic
-
-/-!
-# Facts about injectivity of cancellative multiplication.
--/
-
-#align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
-
-universe u v w
-
-open Function
-
-variable {G : Type*} [Mul G]
-
-section IsLeftCancelMul
-
-variable [IsLeftCancelMul G] {a b c : G}
-
-@[to_additive]
-theorem mul_right_injective (a : G) : Injective (a * ·) := fun _ _ ↦ mul_left_cancel
-#align mul_right_injective mul_right_injective
-#align add_right_injective add_right_injective
-
-@[to_additive (attr := simp)]
-theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
-  (mul_right_injective a).eq_iff
-#align mul_right_inj mul_right_inj
-#align add_right_inj add_right_inj
-
-@[to_additive]
-theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c :=
-  (mul_right_injective a).ne_iff
-#align mul_ne_mul_right mul_ne_mul_right
-#align add_ne_add_right add_ne_add_right
-
-end IsLeftCancelMul
-
-section IsRightCancelMul
-
-variable [IsRightCancelMul G] {a b c : G}
-
-@[to_additive]
-theorem mul_left_injective (a : G) : Function.Injective (· * a) := fun _ _ ↦ mul_right_cancel
-#align mul_left_injective mul_left_injective
-#align add_left_injective add_left_injective
-
-@[to_additive (attr := simp)]
-theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
-  (mul_left_injective a).eq_iff
-#align mul_left_inj mul_left_inj
-#align add_left_inj add_left_inj
-
-@[to_additive]
-theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
-  (mul_left_injective a).ne_iff
-#align mul_ne_mul_left mul_ne_mul_left
-#align add_ne_add_left add_ne_add_left
-
-end IsRightCancelMul
diff --git a/Mathlib/Algebra/Group/Embedding.lean b/Mathlib/Algebra/Group/Embedding.lean
index a1376a6c117d1..640621ad8f42c 100644
--- a/Mathlib/Algebra/Group/Embedding.lean
+++ b/Mathlib/Algebra/Group/Embedding.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Algebra.Group.Cancel
+import Mathlib.Algebra.Group.Basic
 import Mathlib.Logic.Embedding.Basic
 
 #align_import algebra.hom.embedding from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean
index bfe9e26fb23d8..62863ff34b0b9 100644
--- a/Mathlib/CategoryTheory/Shift/Basic.lean
+++ b/Mathlib/CategoryTheory/Shift/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johan Commelin, Andrew Yang
 -/
-import Mathlib.Algebra.Group.Cancel
+import Mathlib.Algebra.Group.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
 import Mathlib.CategoryTheory.Monoidal.End
 import Mathlib.CategoryTheory.Monoidal.Discrete

From 78753aa3a7852ed1d2425e5a1765cabb888922e8 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 15 Jan 2024 13:18:43 +1100
Subject: [PATCH 12/15] add assert_not_exists

---
 Mathlib/Algebra/Group/WithOne/Defs.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean
index 4c79ab6ef0480..0a9f28ebaec2a 100644
--- a/Mathlib/Algebra/Group/WithOne/Defs.lean
+++ b/Mathlib/Algebra/Group/WithOne/Defs.lean
@@ -393,3 +393,9 @@ instance semiring [Semiring α] : Semiring (WithZero α) :=
     WithZero.monoidWithZero, WithZero.instDistrib with }
 
 end WithZero
+
+-- Check that we haven't need to import all the basic lemmas about groups,
+-- by asserting a random sample don't exist here:
+assert_not_exists inv_involutive
+assert_not_exists div_right_inj
+assert_not_exists pow_ite

From e7b2f74ccd66f5ff99802ae9cf72ec2bd928e600 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 17 Jan 2024 11:00:56 +0000
Subject: [PATCH 13/15] delete `Algebra.Group.Classes`

---
 Mathlib.lean                            |  1 -
 Mathlib/Algebra/Group/Basic.lean        | 15 ++++++++++--
 Mathlib/Algebra/Group/Classes.lean      | 29 -----------------------
 Mathlib/Algebra/Group/WithOne/Defs.lean | 31 +++++++++++++++----------
 4 files changed, 32 insertions(+), 44 deletions(-)
 delete mode 100644 Mathlib/Algebra/Group/Classes.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 7e05a54d5080e..46a45eb22ce91 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -167,7 +167,6 @@ import Mathlib.Algebra.GradedMonoid
 import Mathlib.Algebra.GradedMulAction
 import Mathlib.Algebra.Group.Aut
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Group.Classes
 import Mathlib.Algebra.Group.Commutator
 import Mathlib.Algebra.Group.Commute.Basic
 import Mathlib.Algebra.Group.Commute.Defs
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index f4e563fa1ab48..9cc7b2c117dbc 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -73,13 +73,19 @@ theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
 end IsRightCancelMul
 
 section Semigroup
+variable [Semigroup α]
+
+@[to_additive]
+instance Semigroup.to_isAssociative : IsAssociative α (· * ·) := ⟨mul_assoc⟩
+#align semigroup.to_is_associative Semigroup.to_isAssociative
+#align add_semigroup.to_is_associative AddSemigroup.to_isAssociative
 
 /-- Composing two multiplications on the left by `y` then `x`
 is equal to a multiplication on the left by `x * y`.
 -/
 @[to_additive (attr := simp) "Composing two additions on the left by `y` then `x`
 is equal to an addition on the left by `x + y`."]
-theorem comp_mul_left [Semigroup α] (x y : α) : (x * ·) ∘ (y * ·) = (x * y * ·) := by
+theorem comp_mul_left (x y : α) : (x * ·) ∘ (y * ·) = (x * y * ·) := by
   ext z
   simp [mul_assoc]
 #align comp_mul_left comp_mul_left
@@ -90,7 +96,7 @@ is equal to a multiplication on the right by `y * x`.
 -/
 @[to_additive (attr := simp) "Composing two additions on the right by `y` and `x`
 is equal to an addition on the right by `y + x`."]
-theorem comp_mul_right [Semigroup α] (x y : α) : (· * x) ∘ (· * y) = (· * (y * x)) := by
+theorem comp_mul_right (x y : α) : (· * x) ∘ (· * y) = (· * (y * x)) := by
   ext z
   simp [mul_assoc]
 #align comp_mul_right comp_mul_right
@@ -98,6 +104,11 @@ theorem comp_mul_right [Semigroup α] (x y : α) : (· * x) ∘ (· * y) = (· *
 
 end Semigroup
 
+@[to_additive]
+instance CommMagma.to_isCommutative [CommMagma G] : IsCommutative G (· * ·) := ⟨mul_comm⟩
+#align comm_semigroup.to_is_commutative CommMagma.to_isCommutative
+#align add_comm_semigroup.to_is_commutative AddCommMagma.to_isCommutative
+
 section MulOneClass
 
 variable {M : Type u} [MulOneClass M]
diff --git a/Mathlib/Algebra/Group/Classes.lean b/Mathlib/Algebra/Group/Classes.lean
deleted file mode 100644
index ebf61a84eb898..0000000000000
--- a/Mathlib/Algebra/Group/Classes.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2014 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
--/
-import Mathlib.Algebra.Group.Defs
-import Mathlib.Init.Algebra.Classes
-
-/-!
-# Instances for operations in algebraic structures.
-
-As the unbundled algebraic structures typeclasses are of somewhat dubious use at present,
-we separate out the file providing instances from the main `Mathlib.Algebra.Group.Defs` file.
--/
-
-#align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
-
-variable {G : Type*}
-
-@[to_additive]
-instance Semigroup.to_isAssociative [Semigroup G] : IsAssociative G (· * ·) :=
-  ⟨mul_assoc⟩
-#align semigroup.to_is_associative Semigroup.to_isAssociative
-#align add_semigroup.to_is_associative AddSemigroup.to_isAssociative
-
-@[to_additive]
-instance CommMagma.to_isCommutative [CommMagma G] : IsCommutative 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 0a9f28ebaec2a..2859f13d80692 100644
--- a/Mathlib/Algebra/Group/WithOne/Defs.lean
+++ b/Mathlib/Algebra/Group/WithOne/Defs.lean
@@ -3,9 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
 -/
-import Mathlib.Order.WithBot
-import Mathlib.Algebra.Group.Classes
 import Mathlib.Algebra.Ring.Defs
+import Mathlib.Order.WithBot
 
 #align_import algebra.group.with_one.defs from "leanprover-community/mathlib"@"995b47e555f1b6297c7cf16855f1023e355219fb"
 
@@ -188,20 +187,28 @@ instance mulOneClass [Mul α] : MulOneClass (WithOne α) where
   one_mul := (Option.liftOrGet_isLeftId _).1
   mul_one := (Option.liftOrGet_isRightId _).1
 
-@[to_additive]
-instance monoid [Semigroup α] : Monoid (WithOne α) :=
-  { WithOne.mulOneClass with mul_assoc := (Option.liftOrGet_isAssociative _).1 }
-
-@[to_additive]
-instance commMonoid [CommSemigroup α] : CommMonoid (WithOne α) :=
-  { WithOne.monoid with mul_comm := (Option.liftOrGet_isCommutative _).1 }
-
 @[to_additive (attr := simp, norm_cast)]
-theorem coe_mul [Mul α] (a b : α) : ((a * b : α) : WithOne α) = a * b :=
-  rfl
+lemma coe_mul [Mul α] (a b : α) : (↑(a * b) : WithOne α) = a * b := rfl
 #align with_one.coe_mul WithOne.coe_mul
 #align with_zero.coe_add WithZero.coe_add
 
+@[to_additive]
+instance monoid [Semigroup α] : Monoid (WithOne α) where
+  __ := mulOneClass
+  mul_assoc a b c := match a, b, c with
+    | 1, b, c => by simp
+    | (a : α), 1, c => by simp
+    | (a : α), (b : α), 1 => by simp
+    | (a : α), (b : α), (c : α) => by simp_rw [← coe_mul, mul_assoc]
+
+@[to_additive]
+instance commMonoid [CommSemigroup α] : CommMonoid (WithOne α) where
+  mul_comm := fun a b => match a, b with
+    | (a : α), (b : α) => congr_arg some (mul_comm a b)
+    | (_ : α), 1 => rfl
+    | 1, (_ : α) => rfl
+    | 1, 1 => rfl
+
 @[to_additive (attr := simp, norm_cast)]
 theorem coe_inv [Inv α] (a : α) : ((a⁻¹ : α) : WithOne α) = (a : WithOne α)⁻¹ :=
   rfl

From 1d455440f0d09a7db356f878df09119bddf8f031 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 17 Jan 2024 11:01:53 +0000
Subject: [PATCH 14/15] delete unnecessary import

---
 Mathlib/Algebra/CovariantAndContravariant.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Algebra/CovariantAndContravariant.lean b/Mathlib/Algebra/CovariantAndContravariant.lean
index bd5804fa88772..942eacb855158 100644
--- a/Mathlib/Algebra/CovariantAndContravariant.lean
+++ b/Mathlib/Algebra/CovariantAndContravariant.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Group.Classes
 import Mathlib.Order.Basic
 import Mathlib.Order.Monotone.Basic
 

From 0905b81458fd2572fcb53b342e12092c5b297239 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 17 Jan 2024 11:06:38 +0000
Subject: [PATCH 15/15] final cleanup

---
 Mathlib/Algebra/Group/Commute/Defs.lean | 2 +-
 Mathlib/Algebra/Group/Ext.lean          | 8 +++++---
 Mathlib/Algebra/Group/WithOne/Defs.lean | 2 +-
 Mathlib/GroupTheory/EckmannHilton.lean  | 2 +-
 4 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/Group/Commute/Defs.lean b/Mathlib/Algebra/Group/Commute/Defs.lean
index 84388bb7b6e71..bd1e121ee007a 100644
--- a/Mathlib/Algebra/Group/Commute/Defs.lean
+++ b/Mathlib/Algebra/Group/Commute/Defs.lean
@@ -3,9 +3,9 @@ Copyright (c) 2019 Neil Strickland. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Neil Strickland, Yury Kudryashov
 -/
-import Mathlib.Init.Algebra.Classes
 import Mathlib.Algebra.Group.Semiconj.Defs
 import Mathlib.Data.Nat.Defs
+import Mathlib.Init.Algebra.Classes
 
 #align_import algebra.group.commute from "leanprover-community/mathlib"@"05101c3df9d9cfe9430edc205860c79b6d660102"
 
diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean
index 55ac1f1b5ced3..5941bfbe9346b 100644
--- a/Mathlib/Algebra/Group/Ext.lean
+++ b/Mathlib/Algebra/Group/Ext.lean
@@ -27,6 +27,8 @@ former uses `HMul.hMul` which is the canonical spelling.
 monoid, group, extensionality
 -/
 
+open Function
+
 universe u
 
 @[to_additive (attr := ext)]
@@ -153,8 +155,8 @@ theorem DivInvMonoid.ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄
 #align sub_neg_monoid.ext SubNegMonoid.ext
 
 @[to_additive]
-theorem Group.toDivInvMonoid_injective {G : Type*} :
-    Function.Injective (@Group.toDivInvMonoid G) := by rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
+lemma Group.toDivInvMonoid_injective {G : Type*} : Injective (@Group.toDivInvMonoid G) := by
+  rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
 #align group.to_div_inv_monoid_injective Group.toDivInvMonoid_injective
 #align add_group.to_sub_neg_add_monoid_injective AddGroup.toSubNegAddMonoid_injective
 
@@ -172,7 +174,7 @@ theorem Group.ext {G : Type*} ⦃g₁ g₂ : Group G⦄ (h_mul : g₁.mul = g₂
 #align add_group.ext AddGroup.ext
 
 @[to_additive]
-theorem CommGroup.toGroup_injective {G : Type u} : Function.Injective (@CommGroup.toGroup G) := by
+lemma CommGroup.toGroup_injective {G : Type*} : Injective (@CommGroup.toGroup G) := by
   rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
 #align comm_group.to_group_injective CommGroup.toGroup_injective
 #align add_comm_group.to_add_group_injective AddCommGroup.toAddGroup_injective
diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean
index 2859f13d80692..dcf263a377592 100644
--- a/Mathlib/Algebra/Group/WithOne/Defs.lean
+++ b/Mathlib/Algebra/Group/WithOne/Defs.lean
@@ -401,7 +401,7 @@ instance semiring [Semiring α] : Semiring (WithZero α) :=
 
 end WithZero
 
--- Check that we haven't need to import all the basic lemmas about groups,
+-- Check that we haven't needed to import all the basic lemmas about groups,
 -- by asserting a random sample don't exist here:
 assert_not_exists inv_involutive
 assert_not_exists div_right_inj
diff --git a/Mathlib/GroupTheory/EckmannHilton.lean b/Mathlib/GroupTheory/EckmannHilton.lean
index 913d850b6fffb..a986d6bd2b231 100644
--- a/Mathlib/GroupTheory/EckmannHilton.lean
+++ b/Mathlib/GroupTheory/EckmannHilton.lean
@@ -3,8 +3,8 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau, Robert Y. Lewis
 -/
-import Mathlib.Init.Algebra.Classes
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Init.Algebra.Classes
 
 #align_import group_theory.eckmann_hilton from "leanprover-community/mathlib"@"41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3"