diff --git a/Mathlib.lean b/Mathlib.lean
index adb39fb612df4..46a45eb22ce91 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3356,6 +3356,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
@@ -3457,6 +3458,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
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..942eacb855158 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.Defs
+import Mathlib.Algebra.Group.Basic
 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..9cc7b2c117dbc 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -4,6 +4,7 @@ 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
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.SplitIfs
@@ -25,14 +26,66 @@ 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
+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
@@ -43,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
@@ -51,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/Commute/Defs.lean b/Mathlib/Algebra/Group/Commute/Defs.lean
index a32be5c111e4f..bd1e121ee007a 100644
--- a/Mathlib/Algebra/Group/Commute/Defs.lean
+++ b/Mathlib/Algebra/Group/Commute/Defs.lean
@@ -5,6 +5,7 @@ Authors: Neil Strickland, Yury Kudryashov
 -/
 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/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index 5484a4f9bcd49..4729a8c29b78f 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -3,11 +3,13 @@ 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.Basic
 import Mathlib.Init.ZeroOne
+import Mathlib.Tactic.Lemma
+import Mathlib.Tactic.TypeStar
+import Mathlib.Tactic.Simps.Basic
+import Mathlib.Tactic.ToAdditive
+import Mathlib.Util.AssertExists
 
 #align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
@@ -221,27 +223,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
@@ -256,27 +241,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
@@ -311,12 +279,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-/
@@ -359,11 +321,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`."]
@@ -993,7 +950,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
@@ -1231,12 +1188,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
@@ -1248,12 +1199,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]
@@ -1318,3 +1263,6 @@ initialize_simps_projections Group
 initialize_simps_projections AddGroup
 initialize_simps_projections CommGroup
 initialize_simps_projections AddCommGroup
+
+assert_not_exists Function.Injective
+assert_not_exists IsCommutative
diff --git a/Mathlib/Algebra/Group/Embedding.lean b/Mathlib/Algebra/Group/Embedding.lean
index 201064e794f6f..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.Defs
+import Mathlib.Algebra.Group.Basic
 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..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)]
@@ -152,6 +154,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]
+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
+
 @[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 +173,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]
+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
+
 @[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..bcd2698ed13bd 100644
--- a/Mathlib/Algebra/Group/Semiconj/Defs.lean
+++ b/Mathlib/Algebra/Group/Semiconj/Defs.lean
@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 Some proofs and docs came from `algebra/commute` (c) Neil Strickland
 -/
 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/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean
index 41cc2435e9b3d..dcf263a377592 100644
--- a/Mathlib/Algebra/Group/WithOne/Defs.lean
+++ b/Mathlib/Algebra/Group/WithOne/Defs.lean
@@ -3,8 +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.Ring.Defs
+import Mathlib.Order.WithBot
 
 #align_import algebra.group.with_one.defs from "leanprover-community/mathlib"@"995b47e555f1b6297c7cf16855f1023e355219fb"
 
@@ -187,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
@@ -392,3 +400,9 @@ instance semiring [Semiring α] : Semiring (WithZero α) :=
     WithZero.monoidWithZero, WithZero.instDistrib with }
 
 end WithZero
+
+-- 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
+assert_not_exists pow_ite
diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
index ce855a2e4e948..ab87a0d095187 100644
--- a/Mathlib/Algebra/GroupWithZero/Defs.lean
+++ b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.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/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..62863ff34b0b9 100644
--- a/Mathlib/CategoryTheory/Shift/Basic.lean
+++ b/Mathlib/CategoryTheory/Shift/Basic.lean
@@ -3,6 +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.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
 import Mathlib.CategoryTheory.Monoidal.End
 import Mathlib.CategoryTheory.Monoidal.Discrete
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/GroupTheory/EckmannHilton.lean b/Mathlib/GroupTheory/EckmannHilton.lean
index d9cd17e0f947f..a986d6bd2b231 100644
--- a/Mathlib/GroupTheory/EckmannHilton.lean
+++ b/Mathlib/GroupTheory/EckmannHilton.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau, Robert Y. Lewis
 -/
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Init.Algebra.Classes
 
 #align_import group_theory.eckmann_hilton from "leanprover-community/mathlib"@"41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3"
 
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/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.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
diff --git a/Mathlib/Tactic/Basic.lean b/Mathlib/Tactic/Basic.lean
index 5a1a3f5a3ff74..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
 
@@ -21,31 +23,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..d5187b04f16f1
--- /dev/null
+++ b/Mathlib/Tactic/Lemma.lean
@@ -0,0 +1,25 @@
+/-
+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 -/
+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..50dc1a4f01c46
--- /dev/null
+++ b/Mathlib/Tactic/TypeStar.lean
@@ -0,0 +1,29 @@
+/-
+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
+
+/-!
+# 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
+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))
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 : ∀ {α}, α