diff --git a/Mathlib.lean b/Mathlib.lean
index c2f41c0ddeb09..7261b72c19796 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3007,6 +3007,7 @@ import Mathlib.GroupTheory.Perm.ViaEmbedding
 import Mathlib.GroupTheory.PresentedGroup
 import Mathlib.GroupTheory.PushoutI
 import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.GroupTheory.QuotientGroup.Finite
 import Mathlib.GroupTheory.Schreier
 import Mathlib.GroupTheory.SchurZassenhaus
diff --git a/Mathlib/Algebra/Category/Grp/Colimits.lean b/Mathlib/Algebra/Category/Grp/Colimits.lean
index 218f0d859b5ad..ffd0441416766 100644
--- a/Mathlib/Algebra/Category/Grp/Colimits.lean
+++ b/Mathlib/Algebra/Category/Grp/Colimits.lean
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Category.Grp.Preadditive
 import Mathlib.CategoryTheory.Limits.Shapes.Kernels
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
 import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 
 /-!
 # The category of additive commutative groups has all colimits.
diff --git a/Mathlib/Algebra/Category/Grp/EpiMono.lean b/Mathlib/Algebra/Category/Grp/EpiMono.lean
index 472da6d5b3651..08201ebf6c83b 100644
--- a/Mathlib/Algebra/Category/Grp/EpiMono.lean
+++ b/Mathlib/Algebra/Category/Grp/EpiMono.lean
@@ -6,7 +6,8 @@ Authors: Jujian Zhang
 import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.Coset.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 
 /-!
 # Monomorphisms and epimorphisms in `Group`
diff --git a/Mathlib/Algebra/CharZero/Quotient.lean b/Mathlib/Algebra/CharZero/Quotient.lean
index 79b566ed37ce1..5907ad58db1a0 100644
--- a/Mathlib/Algebra/CharZero/Quotient.lean
+++ b/Mathlib/Algebra/CharZero/Quotient.lean
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Field.Basic
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.Algebra.Group.Subgroup.ZPowers
 import Mathlib.Algebra.Order.Group.Unbundled.Int
+import Mathlib.Algebra.Module.Defs
+import Mathlib.GroupTheory.QuotientGroup.Defs
 
 /-!
 # Lemmas about quotients in characteristic zero
diff --git a/Mathlib/Algebra/ModEq.lean b/Mathlib/Algebra/ModEq.lean
index 2744ba932b93f..854300ae9ac33 100644
--- a/Mathlib/Algebra/ModEq.lean
+++ b/Mathlib/Algebra/ModEq.lean
@@ -3,11 +3,12 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Data.Int.ModEq
 import Mathlib.Algebra.Field.Basic
+import Mathlib.Algebra.Group.Subgroup.ZPowers
 import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.Ring.Int
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.Data.Int.ModEq
+import Mathlib.GroupTheory.QuotientGroup.Defs
 
 /-!
 # Equality modulo an element
diff --git a/Mathlib/Algebra/Pointwise/Stabilizer.lean b/Mathlib/Algebra/Pointwise/Stabilizer.lean
index e7a7ecfdf6292..0596f27478672 100644
--- a/Mathlib/Algebra/Pointwise/Stabilizer.lean
+++ b/Mathlib/Algebra/Pointwise/Stabilizer.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 
 /-!
 # Stabilizer of a set under a pointwise action
diff --git a/Mathlib/GroupTheory/Abelianization.lean b/Mathlib/GroupTheory/Abelianization.lean
index 935768695e704..0d35f5937e6b3 100644
--- a/Mathlib/GroupTheory/Abelianization.lean
+++ b/Mathlib/GroupTheory/Abelianization.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Michael Howes
 -/
 import Mathlib.Data.Finite.Card
-import Mathlib.GroupTheory.Finiteness
-import Mathlib.GroupTheory.Commutator.Basic
 import Mathlib.Data.Finite.Prod
+import Mathlib.GroupTheory.Commutator.Basic
+import Mathlib.GroupTheory.Coset.Basic
+import Mathlib.GroupTheory.Finiteness
 
 /-!
 # The abelianization of a group
diff --git a/Mathlib/GroupTheory/Coxeter/Basic.lean b/Mathlib/GroupTheory/Coxeter/Basic.lean
index 26d4fff4bda3c..0d9a5d61d777b 100644
--- a/Mathlib/GroupTheory/Coxeter/Basic.lean
+++ b/Mathlib/GroupTheory/Coxeter/Basic.lean
@@ -3,12 +3,13 @@ Copyright (c) 2024 Newell Jensen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Newell Jensen, Mitchell Lee
 -/
+import Mathlib.Algebra.Group.Subgroup.Pointwise
 import Mathlib.Algebra.Ring.Int
-import Mathlib.GroupTheory.PresentedGroup
 import Mathlib.GroupTheory.Coxeter.Matrix
+import Mathlib.GroupTheory.PresentedGroup
+import Mathlib.Tactic.NormNum.DivMod
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Use
-import Mathlib.Tactic.NormNum.DivMod
 
 /-!
 # Coxeter groups and Coxeter systems
diff --git a/Mathlib/GroupTheory/Divisible.lean b/Mathlib/GroupTheory/Divisible.lean
index e34a6a788ad69..99ead5b297aa7 100644
--- a/Mathlib/GroupTheory/Divisible.lean
+++ b/Mathlib/GroupTheory/Divisible.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 import Mathlib.Algebra.Group.ULift
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Pointwise
+import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.Tactic.NormNum.Eq
 
 /-!
diff --git a/Mathlib/GroupTheory/Finiteness.lean b/Mathlib/GroupTheory/Finiteness.lean
index 6d7da785053a0..88f64c318c38f 100644
--- a/Mathlib/GroupTheory/Finiteness.lean
+++ b/Mathlib/GroupTheory/Finiteness.lean
@@ -3,8 +3,9 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
+import Mathlib.Algebra.Group.Subgroup.Pointwise
 import Mathlib.Data.Set.Pointwise.Finite
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean
index 66ce7103de92b..38d3dbe061cf8 100644
--- a/Mathlib/GroupTheory/Index.lean
+++ b/Mathlib/GroupTheory/Index.lean
@@ -9,6 +9,7 @@ import Mathlib.Data.Set.Card
 import Mathlib.GroupTheory.Coset.Card
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.GroupAction.Quotient
+import Mathlib.GroupTheory.QuotientGroup.Basic
 
 /-!
 # Index of a Subgroup
diff --git a/Mathlib/GroupTheory/PresentedGroup.lean b/Mathlib/GroupTheory/PresentedGroup.lean
index 35916a0da95d5..f1bf24a4e9739 100644
--- a/Mathlib/GroupTheory/PresentedGroup.lean
+++ b/Mathlib/GroupTheory/PresentedGroup.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Howes, Newell Jensen
 -/
 import Mathlib.GroupTheory.FreeGroup.Basic
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 
 /-!
 # Defining a group given by generators and relations
diff --git a/Mathlib/GroupTheory/QuotientGroup/Basic.lean b/Mathlib/GroupTheory/QuotientGroup/Basic.lean
index 207475f814a34..4495ebe68b078 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Basic.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Basic.lean
@@ -8,6 +8,7 @@ Authors: Kevin Buzzard, Patrick Massot
 import Mathlib.Algebra.Group.Subgroup.Pointwise
 import Mathlib.GroupTheory.Congruence.Hom
 import Mathlib.GroupTheory.Coset.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 
 /-!
 # Quotients of groups by normal subgroups
@@ -15,14 +16,6 @@ import Mathlib.GroupTheory.Coset.Basic
 This files develops the basic theory of quotients of groups by normal subgroups. In particular it
 proves Noether's first and second isomorphism theorems.
 
-## Main definitions
-
-* `mk'`: the canonical group homomorphism `G →* G/N` given a normal subgroup `N` of `G`.
-* `lift φ`: the group homomorphism `G/N →* H` given a group homomorphism `φ : G →* H` such that
-  `N ⊆ ker φ`.
-* `map f`: the group homomorphism `G/N →* H/M` given a group homomorphism `f : G →* H` such that
-  `N ⊆ f⁻¹(M)`.
-
 ## Main statements
 
 * `QuotientGroup.quotientKerEquivRange`: Noether's first isomorphism theorem, an explicit
@@ -47,44 +40,6 @@ namespace QuotientGroup
 variable {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H]
   {M : Type x} [Monoid M]
 
-/-- The congruence relation generated by a normal subgroup. -/
-@[to_additive "The additive congruence relation generated by a normal additive subgroup."]
-protected def con : Con G where
-  toSetoid := leftRel N
-  mul' := fun {a b c d} hab hcd => by
-    rw [leftRel_eq] at hab hcd ⊢
-    dsimp only
-    calc
-      c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
-      _ = (a * c)⁻¹ * (b * d) := by
-        simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-
-@[to_additive]
-instance Quotient.group : Group (G ⧸ N) :=
-  (QuotientGroup.con N).group
-
-/-- The group homomorphism from `G` to `G/N`. -/
-@[to_additive "The additive group homomorphism from `G` to `G/N`."]
-def mk' : G →* G ⧸ N :=
-  MonoidHom.mk' QuotientGroup.mk fun _ _ => rfl
-
-@[to_additive (attr := simp)]
-theorem coe_mk' : (mk' N : G → G ⧸ N) = mk :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk'_apply (x : G) : mk' N x = x :=
-  rfl
-
-@[to_additive]
-theorem mk'_surjective : Surjective <| mk' N :=
-  @mk_surjective _ _ N
-
-@[to_additive]
-theorem mk'_eq_mk' {x y : G} : mk' N x = mk' N y ↔ ∃ z ∈ N, x * z = y :=
-  QuotientGroup.eq.trans <| by
-    simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]
-
 open scoped Pointwise in
 @[to_additive]
 theorem sound (U : Set (G ⧸ N)) (g : N.op) :
@@ -94,230 +49,20 @@ theorem sound (U : Set (G ⧸ N)) (g : N.op) :
   congr! 1
   exact Quotient.sound ⟨g⁻¹, rfl⟩
 
-/-- Two `MonoidHom`s from a quotient group are equal if their compositions with
-`QuotientGroup.mk'` are equal.
-
-See note [partially-applied ext lemmas]. -/
-@[to_additive (attr := ext 1100) "Two `AddMonoidHom`s from an additive quotient group are equal if
- their compositions with `AddQuotientGroup.mk'` are equal.
-
- See note [partially-applied ext lemmas]. "]
-theorem monoidHom_ext ⦃f g : G ⧸ N →* M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
-  MonoidHom.ext fun x => QuotientGroup.induction_on x <| (DFunLike.congr_fun h : _)
-
-@[to_additive (attr := simp)]
-theorem eq_one_iff {N : Subgroup G} [N.Normal] (x : G) : (x : G ⧸ N) = 1 ↔ x ∈ N := by
-  refine QuotientGroup.eq.trans ?_
-  rw [mul_one, Subgroup.inv_mem_iff]
-
-@[to_additive]
-theorem ker_le_range_iff {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) :
-    g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1 :=
-  ⟨fun h => MonoidHom.ext fun ⟨_, hx⟩ => (eq_one_iff _).mpr <| h hx,
-    fun h x hx => (eq_one_iff _).mp <| by exact DFunLike.congr_fun h ⟨x, hx⟩⟩
-
-@[to_additive (attr := simp)]
-theorem ker_mk' : MonoidHom.ker (QuotientGroup.mk' N : G →* G ⧸ N) = N :=
-  Subgroup.ext eq_one_iff
--- Porting note: I think this is misnamed without the prime
-
-@[to_additive]
-theorem eq_iff_div_mem {N : Subgroup G} [nN : N.Normal] {x y : G} :
-    (x : G ⧸ N) = y ↔ x / y ∈ N := by
-  refine eq_comm.trans (QuotientGroup.eq.trans ?_)
-  rw [nN.mem_comm_iff, div_eq_mul_inv]
-
 -- for commutative groups we don't need normality assumption
 
-@[to_additive]
-instance Quotient.commGroup {G : Type*} [CommGroup G] (N : Subgroup G) : CommGroup (G ⧸ N) :=
-  { toGroup := have := N.normal_of_comm; QuotientGroup.Quotient.group N
-    mul_comm := fun a b => Quotient.inductionOn₂' a b fun a b => congr_arg mk (mul_comm a b) }
-
 local notation " Q " => G ⧸ N
 
-@[to_additive (attr := simp)]
-theorem mk_one : ((1 : G) : Q) = 1 :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_mul (a b : G) : ((a * b : G) : Q) = a * b :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_inv (a : G) : ((a⁻¹ : G) : Q) = (a : Q)⁻¹ :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_div (a b : G) : ((a / b : G) : Q) = a / b :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = (a : Q) ^ n :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = (a : Q) ^ n :=
-  rfl
-
 @[to_additive (attr := simp)]
 theorem mk_prod {G ι : Type*} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} :
     ((Finset.prod s f : G) : G ⧸ N) = Finset.prod s (fun i => (f i : G ⧸ N)) :=
   map_prod (QuotientGroup.mk' N) _ _
 
-@[to_additive (attr := simp)] lemma map_mk'_self : N.map (mk' N) = ⊥ := by aesop
-
 @[to_additive QuotientAddGroup.strictMono_comap_prod_map]
 theorem strictMono_comap_prod_map :
     StrictMono fun H : Subgroup G ↦ (H.comap N.subtype, H.map (mk' N)) :=
   strictMono_comap_prod_image N
 
-/-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
-group homomorphism `G/N →* M`. -/
-@[to_additive "An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
- to a group homomorphism `G/N →* M`."]
-def lift (φ : G →* M) (HN : N ≤ φ.ker) : Q →* M :=
-  (QuotientGroup.con N).lift φ fun x y h => by
-    simp only [QuotientGroup.con, leftRel_apply, Con.rel_mk] at h
-    rw [Con.ker_rel]
-    calc
-      φ x = φ (y * (x⁻¹ * y)⁻¹) := by rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
-      _ = φ y := by rw [φ.map_mul, HN (N.inv_mem h), mul_one]
-
-@[to_additive (attr := simp)]
-theorem lift_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q) = φ g :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk g : Q) = φ g :=
-  rfl
--- TODO: replace `mk` with `mk'`)
-
-@[to_additive (attr := simp)]
-theorem lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) :
-    lift N φ HN (Quot.mk _ g : Q) = φ g :=
-  rfl
-
-/-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/
-@[to_additive
-      "An `AddGroup` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if `N ⊆ f⁻¹(M)`."]
-def map (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) : G ⧸ N →* H ⧸ M := by
-  refine QuotientGroup.lift N ((mk' M).comp f) ?_
-  intro x hx
-  refine QuotientGroup.eq.2 ?_
-  rw [mul_one, Subgroup.inv_mem_iff]
-  exact h hx
-
-@[to_additive (attr := simp)]
-theorem map_mk (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
-    map N M f h ↑x = ↑(f x) :=
-  rfl
-
-@[to_additive]
-theorem map_mk' (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
-    map N M f h (mk' _ x) = ↑(f x) :=
-  rfl
-
-@[to_additive]
-theorem map_id_apply (h : N ≤ Subgroup.comap (MonoidHom.id _) N := (Subgroup.comap_id N).le) (x) :
-    map N N (MonoidHom.id _) h x = x :=
-  induction_on x fun _x => rfl
-
-@[to_additive (attr := simp)]
-theorem map_id (h : N ≤ Subgroup.comap (MonoidHom.id _) N := (Subgroup.comap_id N).le) :
-    map N N (MonoidHom.id _) h = MonoidHom.id _ :=
-  MonoidHom.ext (map_id_apply N h)
-
-@[to_additive (attr := simp)]
-theorem map_map {I : Type*} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal]
-    (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O)
-    (hgf : N ≤ Subgroup.comap (g.comp f) O :=
-      hf.trans ((Subgroup.comap_mono hg).trans_eq (Subgroup.comap_comap _ _ _)))
-    (x : G ⧸ N) : map M O g hg (map N M f hf x) = map N O (g.comp f) hgf x := by
-  refine induction_on x fun x => ?_
-  simp only [map_mk, MonoidHom.comp_apply]
-
-@[to_additive (attr := simp)]
-theorem map_comp_map {I : Type*} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal]
-    (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O)
-    (hgf : N ≤ Subgroup.comap (g.comp f) O :=
-      hf.trans ((Subgroup.comap_mono hg).trans_eq (Subgroup.comap_comap _ _ _))) :
-    (map M O g hg).comp (map N M f hf) = map N O (g.comp f) hgf :=
-  MonoidHom.ext (map_map N M O f g hf hg hgf)
-
-section Pointwise
-open Set
-
-@[to_additive (attr := simp)] lemma image_coe : ((↑) : G → Q) '' N = 1 :=
-  congr_arg ((↑) : Subgroup Q → Set Q) <| map_mk'_self N
-
-@[to_additive]
-lemma preimage_image_coe (s : Set G) : ((↑) : G → Q) ⁻¹' ((↑) '' s) = N * s := by
-  ext a
-  constructor
-  · rintro ⟨b, hb, h⟩
-    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
-    simp only [h, QuotientGroup.mk_div, div_self']
-  · rintro ⟨a, ha, b, hb, rfl⟩
-    refine ⟨b, hb, ?_⟩
-    simpa only [QuotientGroup.mk_mul, self_eq_mul_left, QuotientGroup.eq_one_iff]
-
-@[to_additive]
-lemma image_coe_inj {s t : Set G} : ((↑) : G → Q) '' s = ((↑) : G → Q) '' t ↔ ↑N * s = N * t := by
-  simp_rw [← preimage_image_coe]
-  exact QuotientGroup.mk_surjective.preimage_injective.eq_iff.symm
-
-end Pointwise
-
-section congr
-
-variable (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H']
-
-/-- `QuotientGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
-given that `e` maps `G` to `H`. -/
-@[to_additive "`QuotientAddGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
- given that `e` maps `G` to `H`."]
-def congr (e : G ≃* H) (he : G'.map e = H') : G ⧸ G' ≃* H ⧸ H' :=
-  { map G' H' e (he ▸ G'.le_comap_map (e : G →* H)) with
-    toFun := map G' H' e (he ▸ G'.le_comap_map (e : G →* H))
-    invFun := map H' G' e.symm (he ▸ (G'.map_equiv_eq_comap_symm e).le)
-    left_inv := fun x => by
-      rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H))
-        (he ▸ (G'.map_equiv_eq_comap_symm e).le)]
-      simp only [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
-        MulEquiv.coe_monoidHom_refl, map_id_apply]
-    right_inv := fun x => by
-      rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le)
-        (he ▸ G'.le_comap_map (e : G →* H)) ]
-      simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
-        MulEquiv.coe_monoidHom_refl, map_id_apply] }
-
-@[simp]
-theorem congr_mk (e : G ≃* H) (he : G'.map ↑e = H') (x) : congr G' H' e he (mk x) = e x :=
-  rfl
-
-theorem congr_mk' (e : G ≃* H) (he : G'.map ↑e = H') (x) :
-    congr G' H' e he (mk' G' x) = mk' H' (e x) :=
-  rfl
-
-@[simp]
-theorem congr_apply (e : G ≃* H) (he : G'.map ↑e = H') (x : G) :
-    congr G' H' e he x = mk' H' (e x) :=
-  rfl
-
-@[simp]
-theorem congr_refl (he : G'.map (MulEquiv.refl G : G →* G) = G' := Subgroup.map_id G') :
-    congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G') := by
-  ext ⟨x⟩
-  rfl
-
-@[simp]
-theorem congr_symm (e : G ≃* H) (he : G'.map ↑e = H') :
-    (congr G' H' e he).symm = congr H' G' e.symm ((Subgroup.map_symm_eq_iff_map_eq _).mpr he) :=
-  rfl
-
-end congr
-
 variable (φ : G →* H)
 
 open MonoidHom
diff --git a/Mathlib/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
new file mode 100644
index 0000000000000..0eeaeb9aa5c12
--- /dev/null
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -0,0 +1,291 @@
+/-
+Copyright (c) 2018 Kevin Buzzard, Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard, Patrick Massot
+-/
+-- This file is to a certain extent based on `quotient_module.lean` by Johannes Hölzl.
+
+import Mathlib.GroupTheory.Congruence.Hom
+import Mathlib.GroupTheory.Coset.Defs
+
+/-!
+# Quotients of groups by normal subgroups
+
+This file defines the group structure on the quotient by a normal subgroup.
+
+## Main definitions
+
+* `QuotientGroup.Quotient.Group`: the group structure on `G/N` given a normal subgroup `N` of `G`.
+* `mk'`: the canonical group homomorphism `G →* G/N` given a normal subgroup `N` of `G`.
+* `lift φ`: the group homomorphism `G/N →* H` given a group homomorphism `φ : G →* H` such that
+  `N ⊆ ker φ`.
+* `map f`: the group homomorphism `G/N →* H/M` given a group homomorphism `f : G →* H` such that
+  `N ⊆ f⁻¹(M)`.
+
+## Tags
+
+quotient groups
+-/
+
+open Function
+open scoped Pointwise
+
+universe u v w x
+namespace QuotientGroup
+
+variable {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H]
+  {M : Type x} [Monoid M]
+
+/-- The congruence relation generated by a normal subgroup. -/
+@[to_additive "The additive congruence relation generated by a normal additive subgroup."]
+protected def con : Con G where
+  toSetoid := leftRel N
+  mul' := fun {a b c d} hab hcd => by
+    rw [leftRel_eq] at hab hcd ⊢
+    dsimp only
+    calc
+      c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
+      _ = (a * c)⁻¹ * (b * d) := by
+        simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
+
+@[to_additive]
+instance Quotient.group : Group (G ⧸ N) :=
+  (QuotientGroup.con N).group
+
+/-- The group homomorphism from `G` to `G/N`. -/
+@[to_additive "The additive group homomorphism from `G` to `G/N`."]
+def mk' : G →* G ⧸ N :=
+  MonoidHom.mk' QuotientGroup.mk fun _ _ => rfl
+
+@[to_additive (attr := simp)]
+theorem coe_mk' : (mk' N : G → G ⧸ N) = mk :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk'_apply (x : G) : mk' N x = x :=
+  rfl
+
+@[to_additive]
+theorem mk'_surjective : Surjective <| mk' N :=
+  @mk_surjective _ _ N
+
+@[to_additive]
+theorem mk'_eq_mk' {x y : G} : mk' N x = mk' N y ↔ ∃ z ∈ N, x * z = y :=
+  QuotientGroup.eq.trans <| by
+    simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]
+
+/-- Two `MonoidHom`s from a quotient group are equal if their compositions with
+`QuotientGroup.mk'` are equal.
+
+See note [partially-applied ext lemmas]. -/
+@[to_additive (attr := ext 1100) "Two `AddMonoidHom`s from an additive quotient group are equal if
+ their compositions with `AddQuotientGroup.mk'` are equal.
+
+ See note [partially-applied ext lemmas]. "]
+theorem monoidHom_ext ⦃f g : G ⧸ N →* M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
+  MonoidHom.ext fun x => QuotientGroup.induction_on x <| (DFunLike.congr_fun h : _)
+
+@[to_additive (attr := simp)]
+theorem eq_one_iff {N : Subgroup G} [N.Normal] (x : G) : (x : G ⧸ N) = 1 ↔ x ∈ N := by
+  refine QuotientGroup.eq.trans ?_
+  rw [mul_one, Subgroup.inv_mem_iff]
+
+@[to_additive]
+theorem ker_le_range_iff {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) :
+    g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1 :=
+  ⟨fun h => MonoidHom.ext fun ⟨_, hx⟩ => (eq_one_iff _).mpr <| h hx,
+    fun h x hx => (eq_one_iff _).mp <| by exact DFunLike.congr_fun h ⟨x, hx⟩⟩
+
+@[to_additive (attr := simp)]
+theorem ker_mk' : MonoidHom.ker (QuotientGroup.mk' N : G →* G ⧸ N) = N :=
+  Subgroup.ext eq_one_iff
+-- Porting note: I think this is misnamed without the prime
+
+@[to_additive]
+theorem eq_iff_div_mem {N : Subgroup G} [nN : N.Normal] {x y : G} :
+    (x : G ⧸ N) = y ↔ x / y ∈ N := by
+  refine eq_comm.trans (QuotientGroup.eq.trans ?_)
+  rw [nN.mem_comm_iff, div_eq_mul_inv]
+
+-- for commutative groups we don't need normality assumption
+
+@[to_additive]
+instance Quotient.commGroup {G : Type*} [CommGroup G] (N : Subgroup G) : CommGroup (G ⧸ N) :=
+  { toGroup := have := N.normal_of_comm; QuotientGroup.Quotient.group N
+    mul_comm := fun a b => Quotient.inductionOn₂' a b fun a b => congr_arg mk (mul_comm a b) }
+
+local notation " Q " => G ⧸ N
+
+@[to_additive (attr := simp)]
+theorem mk_one : ((1 : G) : Q) = 1 :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_mul (a b : G) : ((a * b : G) : Q) = a * b :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_inv (a : G) : ((a⁻¹ : G) : Q) = (a : Q)⁻¹ :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_div (a b : G) : ((a / b : G) : Q) = a / b :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = (a : Q) ^ n :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = (a : Q) ^ n :=
+  rfl
+
+@[to_additive (attr := simp)] lemma map_mk'_self : N.map (mk' N) = ⊥ := by aesop
+
+/-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
+group homomorphism `G/N →* M`. -/
+@[to_additive "An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
+ to a group homomorphism `G/N →* M`."]
+def lift (φ : G →* M) (HN : N ≤ φ.ker) : Q →* M :=
+  (QuotientGroup.con N).lift φ fun x y h => by
+    simp only [QuotientGroup.con, leftRel_apply, Con.rel_mk] at h
+    rw [Con.ker_rel]
+    calc
+      φ x = φ (y * (x⁻¹ * y)⁻¹) := by rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
+      _ = φ y := by rw [φ.map_mul, HN (N.inv_mem h), mul_one]
+
+@[to_additive (attr := simp)]
+theorem lift_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q) = φ g :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk g : Q) = φ g :=
+  rfl
+-- TODO: replace `mk` with `mk'`)
+
+@[to_additive (attr := simp)]
+theorem lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) :
+    lift N φ HN (Quot.mk _ g : Q) = φ g :=
+  rfl
+
+/-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/
+@[to_additive
+      "An `AddGroup` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if `N ⊆ f⁻¹(M)`."]
+def map (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) : G ⧸ N →* H ⧸ M := by
+  refine QuotientGroup.lift N ((mk' M).comp f) ?_
+  intro x hx
+  refine QuotientGroup.eq.2 ?_
+  rw [mul_one, Subgroup.inv_mem_iff]
+  exact h hx
+
+@[to_additive (attr := simp)]
+theorem map_mk (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+    map N M f h ↑x = ↑(f x) :=
+  rfl
+
+@[to_additive]
+theorem map_mk' (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+    map N M f h (mk' _ x) = ↑(f x) :=
+  rfl
+
+@[to_additive]
+theorem map_id_apply (h : N ≤ Subgroup.comap (MonoidHom.id _) N := (Subgroup.comap_id N).le) (x) :
+    map N N (MonoidHom.id _) h x = x :=
+  induction_on x fun _x => rfl
+
+@[to_additive (attr := simp)]
+theorem map_id (h : N ≤ Subgroup.comap (MonoidHom.id _) N := (Subgroup.comap_id N).le) :
+    map N N (MonoidHom.id _) h = MonoidHom.id _ :=
+  MonoidHom.ext (map_id_apply N h)
+
+@[to_additive (attr := simp)]
+theorem map_map {I : Type*} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal]
+    (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O)
+    (hgf : N ≤ Subgroup.comap (g.comp f) O :=
+      hf.trans ((Subgroup.comap_mono hg).trans_eq (Subgroup.comap_comap _ _ _)))
+    (x : G ⧸ N) : map M O g hg (map N M f hf x) = map N O (g.comp f) hgf x := by
+  refine induction_on x fun x => ?_
+  simp only [map_mk, MonoidHom.comp_apply]
+
+@[to_additive (attr := simp)]
+theorem map_comp_map {I : Type*} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal]
+    (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O)
+    (hgf : N ≤ Subgroup.comap (g.comp f) O :=
+      hf.trans ((Subgroup.comap_mono hg).trans_eq (Subgroup.comap_comap _ _ _))) :
+    (map M O g hg).comp (map N M f hf) = map N O (g.comp f) hgf :=
+  MonoidHom.ext (map_map N M O f g hf hg hgf)
+
+section Pointwise
+open Set
+
+@[to_additive (attr := simp)] lemma image_coe : ((↑) : G → Q) '' N = 1 :=
+  congr_arg ((↑) : Subgroup Q → Set Q) <| map_mk'_self N
+
+@[to_additive]
+lemma preimage_image_coe (s : Set G) : ((↑) : G → Q) ⁻¹' ((↑) '' s) = N * s := by
+  ext a
+  constructor
+  · rintro ⟨b, hb, h⟩
+    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
+    simp only [h, QuotientGroup.mk_div, div_self']
+  · rintro ⟨a, ha, b, hb, rfl⟩
+    refine ⟨b, hb, ?_⟩
+    simpa only [QuotientGroup.mk_mul, self_eq_mul_left, QuotientGroup.eq_one_iff]
+
+@[to_additive]
+lemma image_coe_inj {s t : Set G} : ((↑) : G → Q) '' s = ((↑) : G → Q) '' t ↔ ↑N * s = N * t := by
+  simp_rw [← preimage_image_coe]
+  exact QuotientGroup.mk_surjective.preimage_injective.eq_iff.symm
+
+end Pointwise
+
+section congr
+
+variable (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H']
+
+/-- `QuotientGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
+given that `e` maps `G` to `H`. -/
+@[to_additive "`QuotientAddGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
+ given that `e` maps `G` to `H`."]
+def congr (e : G ≃* H) (he : G'.map e = H') : G ⧸ G' ≃* H ⧸ H' :=
+  { map G' H' e (he ▸ G'.le_comap_map (e : G →* H)) with
+    toFun := map G' H' e (he ▸ G'.le_comap_map (e : G →* H))
+    invFun := map H' G' e.symm (he ▸ (G'.map_equiv_eq_comap_symm e).le)
+    left_inv := fun x => by
+      rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H))
+        (he ▸ (G'.map_equiv_eq_comap_symm e).le)]
+      simp only [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
+        MulEquiv.coe_monoidHom_refl, map_id_apply]
+    right_inv := fun x => by
+      rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le)
+        (he ▸ G'.le_comap_map (e : G →* H)) ]
+      simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
+        MulEquiv.coe_monoidHom_refl, map_id_apply] }
+
+@[simp]
+theorem congr_mk (e : G ≃* H) (he : G'.map ↑e = H') (x) : congr G' H' e he (mk x) = e x :=
+  rfl
+
+theorem congr_mk' (e : G ≃* H) (he : G'.map ↑e = H') (x) :
+    congr G' H' e he (mk' G' x) = mk' H' (e x) :=
+  rfl
+
+@[simp]
+theorem congr_apply (e : G ≃* H) (he : G'.map ↑e = H') (x : G) :
+    congr G' H' e he x = mk' H' (e x) :=
+  rfl
+
+@[simp]
+theorem congr_refl (he : G'.map (MulEquiv.refl G : G →* G) = G' := Subgroup.map_id G') :
+    congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G') := by
+  ext ⟨x⟩
+  rfl
+
+@[simp]
+theorem congr_symm (e : G ≃* H) (he : G'.map ↑e = H') :
+    (congr G' H' e he).symm = congr H' G' e.symm ((Subgroup.map_symm_eq_iff_map_eq _).mpr he) :=
+  rfl
+
+end congr
+
+end QuotientGroup
diff --git a/Mathlib/RepresentationTheory/Action/Concrete.lean b/Mathlib/RepresentationTheory/Action/Concrete.lean
index 61d62003c4f3d..16750cee24335 100644
--- a/Mathlib/RepresentationTheory/Action/Concrete.lean
+++ b/Mathlib/RepresentationTheory/Action/Concrete.lean
@@ -6,7 +6,7 @@ Authors: Kim Morrison
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.CategoryTheory.FintypeCat
 import Mathlib.GroupTheory.GroupAction.Quotient
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.RepresentationTheory.Action.Basic
 
 /-!
diff --git a/Mathlib/Topology/Algebra/Group/Quotient.lean b/Mathlib/Topology/Algebra/Group/Quotient.lean
index ced9990e38fb3..d4e000715092d 100644
--- a/Mathlib/Topology/Algebra/Group/Quotient.lean
+++ b/Mathlib/Topology/Algebra/Group/Quotient.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov
 -/
 import Mathlib.GroupTheory.GroupAction.Quotient
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.Topology.Algebra.Group.Basic
 import Mathlib.Topology.Maps.OpenQuotient