From 9d93764a7a0b1b8e060dc2ec248796e957949d44 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 20 Nov 2022 14:48:34 -0600
Subject: [PATCH 01/12] feat(ring_theory/integral_domain): generalize
 `card_fiber_eq_of_mem_range`

* Generalize `card_fiber_eq_of_mem_range` to homomorphisms from a
  group to a monoid.
* Rename it to `monoid_hom.card_fiber_eq_of_mem_range`, use
  `to_additive`.
---
 src/ring_theory/integral_domain.lean | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
index c9e84fe09ac29..e10c7c4391f0b 100644
--- a/src/ring_theory/integral_domain.lean
+++ b/src/ring_theory/integral_domain.lean
@@ -133,20 +133,19 @@ end
 
 variables [fintype G]
 
-lemma card_fiber_eq_of_mem_range {H : Type*} [group H] [decidable_eq H]
-  (f : G →* H) {x y : H} (hx : x ∈ set.range f) (hy : y ∈ set.range f) :
+@[to_additive] lemma monoid_hom.card_fiber_eq_of_mem_range {M} [monoid M] [decidable_eq M]
+  (f : G →* M) {x y : M} (hx : x ∈ set.range f) (hy : y ∈ set.range f) :
   (univ.filter $ λ g, f g = x).card = (univ.filter $ λ g, f g = y).card :=
 begin
-  rcases hx with ⟨x, rfl⟩,
-  rcases hy with ⟨y, rfl⟩,
-  refine card_congr (λ g _, g * x⁻¹ * y) _ _ (λ g hg, ⟨g * y⁻¹ * x, _⟩),
-  { simp only [mem_filter, one_mul, monoid_hom.map_mul, mem_univ, mul_right_inv,
-      eq_self_iff_true, monoid_hom.map_mul_inv, and_self, forall_true_iff] {contextual := tt} },
-  { simp only [mul_left_inj, imp_self, forall_2_true_iff], },
-  { simp only [true_and, mem_filter, mem_univ] at hg,
-    simp only [hg, mem_filter, one_mul, monoid_hom.map_mul, mem_univ, mul_right_inv,
-      eq_self_iff_true, exists_prop_of_true, monoid_hom.map_mul_inv, and_self,
-      mul_inv_cancel_right, inv_mul_cancel_right], }
+  rcases ⟨hx, hy⟩ with ⟨⟨x, rfl⟩, y, rfl⟩,
+  obtain ⟨f, rfl⟩ : ∃ f' : G →* Mˣ, f = (units.coe_hom M).comp f',
+    from ⟨f.to_hom_units, fun_like.ext' rfl⟩,
+  rcases mul_left_surjective x y with ⟨y, rfl⟩,
+  simp only [monoid_hom.comp_apply, units.coe_hom_apply, units.eq_iff],
+  conv_lhs { rw [← map_univ_equiv (equiv.mul_right y⁻¹), filter_map, card_map] },
+  congr' 2 with g,
+  simp only [mul_inv_eq_iff_eq_mul, (∘), equiv.to_embedding_apply, equiv.coe_mul_right, map_inv,
+    map_mul]
 end
 
 /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.
@@ -181,7 +180,7 @@ begin
   ... = 0 : smul_zero _,
   { -- remaining goal 1
     show (univ.filter (λ (g : G), f.to_hom_units g = u)).card = c,
-    apply card_fiber_eq_of_mem_range f.to_hom_units,
+    apply f.to_hom_units.card_fiber_eq_of_mem_range,
     { simpa only [mem_image, mem_univ, exists_prop_of_true, set.mem_range] using hu, },
     { exact ⟨1, f.to_hom_units.map_one⟩ } },
   -- remaining goal 2

From 87778dbf2faee647255fba30be70916b947fcbe5 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 20 Nov 2022 14:59:00 -0600
Subject: [PATCH 02/12] Golf

---
 src/algebra/hom/units.lean           | 6 ++++--
 src/ring_theory/integral_domain.lean | 7 ++-----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/algebra/hom/units.lean b/src/algebra/hom/units.lean
index bd660360a96d1..9e5a0f813322b 100644
--- a/src/algebra/hom/units.lean
+++ b/src/algebra/hom/units.lean
@@ -142,8 +142,10 @@ units.lift_right f
   (λ g, ⟨f g, f g⁻¹, map_mul_eq_one f (mul_inv_self _), map_mul_eq_one f (inv_mul_self _)⟩)
   (λ g, rfl)
 
-@[simp] lemma coe_to_hom_units {G M : Type*} [group G] [monoid M] (f : G →* M) (g : G):
-  (f.to_hom_units g : M) = f g := rfl
+@[simp, to_additive]
+lemma coe_to_hom_units {G M : Type*} [group G] [monoid M] (f : G →* M) (g : G) :
+  (f.to_hom_units g : M) = f g :=
+rfl
 
 end monoid_hom
 
diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
index e10c7c4391f0b..3892a12aef14c 100644
--- a/src/ring_theory/integral_domain.lean
+++ b/src/ring_theory/integral_domain.lean
@@ -138,14 +138,11 @@ variables [fintype G]
   (univ.filter $ λ g, f g = x).card = (univ.filter $ λ g, f g = y).card :=
 begin
   rcases ⟨hx, hy⟩ with ⟨⟨x, rfl⟩, y, rfl⟩,
-  obtain ⟨f, rfl⟩ : ∃ f' : G →* Mˣ, f = (units.coe_hom M).comp f',
-    from ⟨f.to_hom_units, fun_like.ext' rfl⟩,
   rcases mul_left_surjective x y with ⟨y, rfl⟩,
-  simp only [monoid_hom.comp_apply, units.coe_hom_apply, units.eq_iff],
   conv_lhs { rw [← map_univ_equiv (equiv.mul_right y⁻¹), filter_map, card_map] },
   congr' 2 with g,
-  simp only [mul_inv_eq_iff_eq_mul, (∘), equiv.to_embedding_apply, equiv.coe_mul_right, map_inv,
-    map_mul]
+  simp only [(∘), equiv.to_embedding_apply, equiv.coe_mul_right, map_mul],
+  rw [← f.coe_to_hom_units y⁻¹, map_inv, units.mul_inv_eq_iff_eq_mul, f.coe_to_hom_units]
 end
 
 /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.

From 83c3644b26a2047532df788997d3e133eef96513 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 22 Nov 2022 17:59:38 -0600
Subject: [PATCH 03/12] Snapshot

---
 src/algebra/group/units.lean               |  6 ++
 src/group_theory/subgroup/basic.lean       | 54 ++++++++++++-----
 src/group_theory/submonoid/membership.lean | 23 +++-----
 src/ring_theory/integral_domain.lean       | 69 ++++++++--------------
 4 files changed, 77 insertions(+), 75 deletions(-)

diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
index 9715e7eaaabdd..908948072c914 100644
--- a/src/algebra/group/units.lean
+++ b/src/algebra/group/units.lean
@@ -475,6 +475,12 @@ h.mul_left_inj.1
 @[to_additive] protected lemma mul_left_injective (h : is_unit b) : injective (* b) :=
 λ _ _, h.mul_right_cancel
 
+@[to_additive] protected lemma mul_right_eq_self (h : is_unit a) : a * b = a ↔ b = 1 :=
+iff.trans (by rw [mul_one]) h.mul_right_inj
+
+@[to_additive] protected lemma mul_left_eq_self (h : is_unit b) : a * b = b ↔ a = 1 :=
+iff.trans (by rw [one_mul]) h.mul_left_inj
+
 end monoid
 
 variables [division_monoid M] {a : M}
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 811854bd17ea8..3b59815b996ed 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -2142,6 +2142,41 @@ lemma ker_prod_map {G' : Type*} {N' : Type*} [group G'] [group N'] (f : G →* N
   (prod_map f g).ker = f.ker.prod g.ker :=
 by rw [←comap_bot, ←comap_bot, ←comap_bot, ←prod_map_comap_prod, bot_prod_bot]
 
+variables [monoid N]
+
+@[simp, to_additive] lemma preimage_mul_left_ker (f : G →* N) (x : G) :
+  ((*) x) ⁻¹' f.ker = f ⁻¹' {f x⁻¹} :=
+begin
+  ext y,
+  rcases mul_left_surjective x⁻¹ y with ⟨y, rfl⟩,
+  simp only [set.mem_preimage, set_like.mem_coe, set.mem_singleton_iff, mem_ker,
+    mul_inv_cancel_left, map_mul, ((group.is_unit _).map f).mul_right_eq_self]
+end
+
+@[simp, to_additive] lemma preimage_mul_right_ker (f : G →* N) (x : G) :
+  (λ y, y * x) ⁻¹' f.ker = f ⁻¹' {f x⁻¹} :=
+begin
+  ext y,
+  rcases mul_right_surjective x⁻¹ y with ⟨y, rfl⟩,
+  simp only [set.mem_preimage, set_like.mem_coe, set.mem_singleton_iff, mem_ker,
+    inv_mul_cancel_right, map_mul, ((group.is_unit _).map f).mul_left_eq_self]
+end
+
+@[simp, to_additive] lemma image_mul_left_ker (f : G →* N) (x : G) :
+  ((*) x) '' f.ker = f ⁻¹' {f x} :=
+by rw [← equiv.coe_mul_left, equiv.image_eq_preimage, equiv.mul_left_symm_apply,
+  preimage_mul_left_ker, inv_inv]
+
+@[simp, to_additive] lemma image_mul_right_ker (f : G →* N) (x : G) :
+  (λ y, y * x) '' f.ker = f ⁻¹' {f x} :=
+by rw [← equiv.coe_mul_right, equiv.image_eq_preimage, equiv.mul_right_symm_apply,
+  preimage_mul_right_ker, inv_inv]
+
+@[simp, to_additive] lemma card_preimage_singleton (f : G →* N) (x : G)
+  [fintype f.ker] [fintype (f ⁻¹' {f x})] : fintype.card (f ⁻¹' {f x}) = fintype.card f.ker :=
+fintype.card_congr $ (equiv.set_congr $ f.image_mul_left_ker x).symm.trans $
+  ((equiv.mul_left x).image _).symm
+
 end ker
 
 /-- The subgroup of elements `x : G` such that `f x = g x` -/
@@ -2213,14 +2248,7 @@ namespace subgroup
 variables {N : Type*} [group N] (H : subgroup G)
 
 @[to_additive] lemma map_eq_bot_iff {f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker :=
-begin
-  rw eq_bot_iff,
-  split,
-  { exact λ h x hx, h ⟨x, hx, rfl⟩ },
-  { intros h x hx,
-    obtain ⟨y, hy, rfl⟩ := hx,
-    exact h hy },
-end
+(gc_map_comap f).l_eq_bot
 
 @[to_additive]
 lemma map_eq_bot_iff_of_injective {f : G →* N} (hf : function.injective f) : H.map f = ⊥ ↔ H = ⊥ :=
@@ -2257,10 +2285,8 @@ lemma le_comap_map (H : subgroup G) : H ≤ comap f (map f H) :=
 @[to_additive]
 lemma map_comap_eq (H : subgroup N) :
   map f (comap f H) = f.range ⊓ H :=
-set_like.ext' begin
-  convert set.image_preimage_eq_inter_range,
-  simp [set.inter_comm],
-end
+set_like.ext' $ by rw [coe_map, coe_comap, set.image_preimage_eq_inter_range, coe_inf, coe_range,
+  set.inter_comm]
 
 @[to_additive]
 lemma comap_map_eq (H : subgroup G) : comap f (map f H) = H ⊔ f.ker :=
@@ -2806,9 +2832,7 @@ instance : is_modular_lattice (subgroup C) :=
   rw [mem_inf, mem_sup] at ha,
   rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩,
   rw mem_sup,
-  refine ⟨b, hb, c, mem_inf.2 ⟨hc, _⟩, rfl⟩,
-  rw ← inv_mul_cancel_left b c,
-  apply z.mul_mem (z.inv_mem (xz hb)) haz,
+  exact ⟨b, hb, c, mem_inf.2 ⟨hc, (mul_mem_cancel_left (xz hb)).1 haz⟩, rfl⟩
 end⟩
 
 end subgroup
diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean
index 5fcbd19046167..61336ecb40075 100644
--- a/src/group_theory/submonoid/membership.lean
+++ b/src/group_theory/submonoid/membership.lean
@@ -351,6 +351,8 @@ by { ext, exact mem_closure_singleton.symm }
 lemma powers_subset {n : M} {P : submonoid M} (h : n ∈ P) : powers n ≤ P :=
 λ x hx, match x, hx with _, ⟨i, rfl⟩ := pow_mem h i end
 
+@[simp] lemma powers_one : powers (1 : M) = ⊥ := bot_unique $ powers_subset (one_mem _)
+
 /-- Exponentiation map from natural numbers to powers. -/
 @[simps] def pow (n : M) (m : ℕ) : powers n :=
 (powers_hom M n).mrange_restrict (multiplicative.of_add m)
@@ -472,21 +474,12 @@ def multiples (x : A) : add_submonoid A :=
 add_submonoid.copy (multiples_hom A x).mrange (set.range (λ i, i • x : ℕ → A)) $
 set.ext (λ n, exists_congr $ λ i, by simp; refl)
 
-@[simp] lemma mem_multiples (x : A) : x ∈ multiples x := ⟨1, one_nsmul _⟩
-
-lemma mem_multiples_iff (x z : A) : x ∈ multiples z ↔ ∃ n : ℕ, n • z = x := iff.rfl
-
-lemma multiples_eq_closure (x : A) : multiples x = closure {x} :=
-by { ext, exact mem_closure_singleton.symm }
-
-lemma multiples_subset {x : A} {P : add_submonoid A} (h : x ∈ P) : multiples x ≤ P :=
-λ x hx, match x, hx with _, ⟨i, rfl⟩ := nsmul_mem h i end
-
-attribute [to_additive add_submonoid.multiples] submonoid.powers
-attribute [to_additive add_submonoid.mem_multiples] submonoid.mem_powers
-attribute [to_additive add_submonoid.mem_multiples_iff] submonoid.mem_powers_iff
-attribute [to_additive add_submonoid.multiples_eq_closure] submonoid.powers_eq_closure
-attribute [to_additive add_submonoid.multiples_subset] submonoid.powers_subset
+attribute [to_additive multiples] submonoid.powers
+attribute [to_additive mem_multiples] submonoid.mem_powers
+attribute [to_additive mem_multiples_iff] submonoid.mem_powers_iff
+attribute [to_additive multiples_eq_closure] submonoid.powers_eq_closure
+attribute [to_additive multiples_subset] submonoid.powers_subset
+attribute [to_additive multiples_zero] submonoid.powers_one
 
 end add_submonoid
 
diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
index 3892a12aef14c..244f95ddb959e 100644
--- a/src/ring_theory/integral_domain.lean
+++ b/src/ring_theory/integral_domain.lean
@@ -116,65 +116,44 @@ To support `ℤˣ` and other infinite monoids with finite groups of units, this
 instance [finite Rˣ] : is_cyclic Rˣ :=
 is_cyclic_of_subgroup_is_domain (units.coe_hom R) $ units.ext
 
-section
-
-variables (S : subgroup Rˣ) [finite S]
-
 /-- A finite subgroup of the units of an integral domain is cyclic. -/
-instance subgroup_units_cyclic : is_cyclic S :=
-begin
-  refine is_cyclic_of_subgroup_is_domain ⟨(coe : S → R), _, _⟩
-    (units.ext.comp subtype.val_injective),
-  { simp },
-  { intros, simp },
-end
-
-end
+instance subgroup_units_cyclic (S : subgroup Rˣ) [finite S] : is_cyclic S :=
+is_cyclic_of_subgroup_is_domain ((units.coe_hom R).comp S.subtype)
+  (units.ext.comp subtype.coe_injective)
 
 variables [fintype G]
 
-@[to_additive] lemma monoid_hom.card_fiber_eq_of_mem_range {M} [monoid M] [decidable_eq M]
-  (f : G →* M) {x y : M} (hx : x ∈ set.range f) (hy : y ∈ set.range f) :
-  (univ.filter $ λ g, f g = x).card = (univ.filter $ λ g, f g = y).card :=
-begin
-  rcases ⟨hx, hy⟩ with ⟨⟨x, rfl⟩, y, rfl⟩,
-  rcases mul_left_surjective x y with ⟨y, rfl⟩,
-  conv_lhs { rw [← map_univ_equiv (equiv.mul_right y⁻¹), filter_map, card_map] },
-  congr' 2 with g,
-  simp only [(∘), equiv.to_embedding_apply, equiv.coe_mul_right, map_mul],
-  rw [← f.coe_to_hom_units y⁻¹, map_inv, units.mul_inv_eq_iff_eq_mul, f.coe_to_hom_units]
-end
-
 /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.
 -/
 lemma sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 :=
 begin
   classical,
-  obtain ⟨x, hx⟩ : ∃ x : monoid_hom.range f.to_hom_units,
-    ∀ y : monoid_hom.range f.to_hom_units, y ∈ submonoid.powers x,
+  obtain ⟨f, rfl⟩ : ∃ f' : G →* Rˣ, (units.coe_hom R).comp f' = f,
+    from ⟨f.to_hom_units, fun_like.ext' rfl⟩,
+  obtain ⟨x, hx⟩ : ∃ x : f.range, ∀ y : f.range, y ∈ submonoid.powers x,
     from is_cyclic.exists_monoid_generator,
   have hx1 : x ≠ 1,
   { rintro rfl,
     apply hf,
     ext g,
-    rw [monoid_hom.one_apply],
-    cases hx ⟨f.to_hom_units g, g, rfl⟩ with n hn,
-    rwa [subtype.ext_iff, units.ext_iff, subtype.coe_mk, monoid_hom.coe_to_hom_units,
-      one_pow, eq_comm] at hn, },
-  replace hx1 : (x : R) - 1 ≠ 0,
-    from λ h, hx1 (subtype.eq (units.ext (sub_eq_zero.1 h))),
-  let c := (univ.filter (λ g, f.to_hom_units g = 1)).card,
-  calc ∑ g : G, f g
-      = ∑ g : G, f.to_hom_units g : rfl
-  ... = ∑ u : Rˣ in univ.image f.to_hom_units,
-    (univ.filter (λ g, f.to_hom_units g = u)).card • u : sum_comp (coe : Rˣ → R) f.to_hom_units
-  ... = ∑ u : Rˣ in univ.image f.to_hom_units, c • u :
-    sum_congr rfl (λ u hu, congr_arg2 _ _ rfl) -- remaining goal 1, proven below
-  ... = ∑ b : monoid_hom.range f.to_hom_units, c • ↑b : finset.sum_subtype _
-      (by simp ) _
-  ... = c • ∑ b : monoid_hom.range f.to_hom_units, (b : R) : smul_sum.symm
-  ... = c • 0 : congr_arg2 _ rfl _            -- remaining goal 2, proven below
-  ... = 0 : smul_zero _,
+    specialize hx ⟨f g, g, rfl⟩,
+    rw [submonoid.powers_one, submonoid.mem_bot, ← subtype.coe_inj, subtype.coe_mk] at hx,
+    rw [monoid_hom.comp_apply, monoid_hom.one_apply, hx, coe_one, map_one] },
+  replace hx1 : (x : R) - 1 ≠ 0, from sub_ne_zero.2 (λ h, hx1 $ subtype.ext $ units.ext h),
+  set c := fintype.card f.ker,
+  calc ∑ g : G, (f g : R) = ∑ u : Rˣ in univ.image f, c • u : eq.symm $ sum_image' _ $
+    λ g hg, _ -- remaining goal 1, proven below
+  ... = _ : _,
+    
+  -- calc ∑ g : G, f g = ∑ u : Rˣ in univ.image f,
+  --   (univ.filter (λ g, f.to_hom_units g = u)).card • u : sum_comp (coe : Rˣ → R) f.to_hom_units
+  -- ... = ∑ u : Rˣ in univ.image f, c • u :
+  --   sum_congr rfl (λ u hu, congr_arg2 _ _ rfl) -- remaining goal 1, proven below
+  -- ... = ∑ b : f.range, c • ↑b : finset.sum_subtype _
+  --     (by simp ) _
+  -- ... = c • ∑ b : monoid_hom.range f.to_hom_units, (b : R) : smul_sum.symm
+  -- ... = c • 0 : congr_arg2 _ rfl _            -- remaining goal 2, proven below
+  -- ... = 0 : smul_zero _,
   { -- remaining goal 1
     show (univ.filter (λ (g : G), f.to_hom_units g = u)).card = c,
     apply f.to_hom_units.card_fiber_eq_of_mem_range,

From 7c88f0b04270dbc189d31f63dc73270cb75d526d Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 23 Nov 2022 13:06:12 -0600
Subject: [PATCH 04/12] Snapshot

---
 src/data/quot.lean                   |  17 +-
 src/data/set/basic.lean              |  29 ++-
 src/group_theory/coset.lean          |   8 +-
 src/group_theory/quotient_group.lean | 258 +++++++++++++--------------
 src/group_theory/subgroup/basic.lean |  59 +++---
 src/ring_theory/integral_domain.lean |   3 +
 6 files changed, 205 insertions(+), 169 deletions(-)

diff --git a/src/data/quot.lean b/src/data/quot.lean
index b082163abe85a..0b17e5e3db445 100644
--- a/src/data/quot.lean
+++ b/src/data/quot.lean
@@ -21,6 +21,8 @@ quotient
 
 variables {α : Sort*} {β : Sort*}
 
+open function
+
 namespace setoid
 
 lemma ext {α : Sort*} :
@@ -72,13 +74,17 @@ lemma factor_mk_eq {α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y 
 variables {γ : Sort*} {r : α → α → Prop} {s : β → β → Prop}
 
 /-- **Alias** of `quot.lift_beta`. -/
-lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
-  quot.lift f h (quot.mk r a) = f a := quot.lift_beta f h a
+@[simp] lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
+  quot.lift f h (quot.mk r a) = f a := rfl
 
 @[simp]
 lemma lift_on_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
   quot.lift_on (quot.mk r a) f h = f a := rfl
 
+@[simp] lemma surjective_lift {f : α → γ} (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
+  surjective (lift f h) ↔ surjective f :=
+⟨λ hf, hf.comp quot.exists_rep, λ hf y, let ⟨x, hx⟩ := hf y in ⟨quot.mk _ x, hx⟩⟩
+
 /-- Descends a function `f : α → β → γ` to quotients of `α` and `β`. -/
 attribute [reducible, elab_as_eliminator]
 protected def lift₂
@@ -272,8 +278,7 @@ rfl
   quotient.lift_on₂ (quotient.mk x) (quotient.mk y) f h = f x y := rfl
 
 /-- `quot.mk r` is a surjective function. -/
-lemma surjective_quot_mk (r : α → α → Prop) : function.surjective (quot.mk r) :=
-quot.exists_rep
+lemma surjective_quot_mk (r : α → α → Prop) : surjective (quot.mk r) := quot.exists_rep
 
 /-- `quotient.mk` is a surjective function. -/
 lemma surjective_quotient_mk (α : Sort*) [s : setoid α] :
@@ -482,6 +487,10 @@ protected def lift_on' (q : quotient s₁) (f : α → φ)
 protected lemma lift_on'_mk' (f : α → φ) (h) (x : α) :
   quotient.lift_on' (@quotient.mk' _ s₁ x) f h = f x := rfl
 
+@[simp] lemma surjective_lift_on' {f : α → φ} (h : ∀ a b, @setoid.r α s₁ a b → f a = f b) :
+  surjective (λ x, quotient.lift_on' x f h) ↔ surjective f :=
+quot.surjective_lift _
+
 /-- A version of `quotient.lift_on₂` taking `{s₁ : setoid α} {s₂ : setoid β}` as implicit arguments
 instead of instance arguments. -/
 @[elab_as_eliminator, reducible]
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 65eab1507f17d..9d09eebaf500e 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -2284,13 +2284,36 @@ by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_d
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
 (surjective_quot_mk r).range_eq
 
-instance can_lift (c) (p) [can_lift α β c p] :
-  can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
-{ prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
+@[simp] theorem range_quot_lift {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) :
+  range (quot.lift f hf) = range f :=
+ext $ λ y, (surjective_quot_mk _).exists
+
+@[simp] theorem range_quot_lift_on {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) :
+  range (λ x, quot.lift_on x f hf) = range f :=
+range_quot_lift _
 
 @[simp] theorem range_quotient_mk [setoid α] : range (λx : α, ⟦x⟧) = univ :=
 range_quot_mk _
 
+@[simp] theorem range_quotient_lift [s : setoid ι] (hf) :
+  range (quotient.lift f hf : quotient s → α) = range f :=
+range_quot_lift _
+
+@[simp] theorem range_quotient_mk' {s : setoid α} : range (quotient.mk' : α → quotient s) = univ :=
+range_quot_mk _
+
+@[simp] theorem range_quotient_lift_on' {s : setoid ι} (hf) :
+  range (λ x : quotient s, quotient.lift_on' x f hf) = range f :=
+range_quot_lift _
+
+@[simp] theorem range_quotient_lift_on [s : setoid ι] (hf) :
+  range (λ x : quotient s, quotient.lift_on x f hf) = range f :=
+range_quot_lift _
+
+instance can_lift (c) (p) [can_lift α β c p] :
+  can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
+{ prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
+
 lemma range_const_subset {c : α} : range (λ x : ι, c) ⊆ {c} :=
 range_subset_iff.2 $ λ x, rfl
 
diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean
index e89d65f50d697..211089fd5cd2d 100644
--- a/src/group_theory/coset.lean
+++ b/src/group_theory/coset.lean
@@ -328,10 +328,14 @@ quotient.mk' a
 lemma mk_surjective : function.surjective $ @mk _ _ s := quotient.surjective_quotient_mk'
 
 @[elab_as_eliminator, to_additive]
-lemma induction_on {C : α ⧸ s → Prop} (x : α ⧸ s)
-  (H : ∀ z, C (quotient_group.mk z)) : C x :=
+lemma induction_on {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ z, C (mk z)) : C x :=
 quotient.induction_on' x H
 
+@[elab_as_eliminator, to_additive]
+lemma induction_on₂ {β} [group β] {t : subgroup β} {C : α ⧸ s → β ⧸ t → Prop}
+  (x : α ⧸ s) (y : β ⧸ t) (H : ∀ a b, C (mk a) (mk b)) : C x y :=
+quotient.induction_on₂' x y H
+
 @[to_additive]
 instance : has_coe_t α (α ⧸ s) := ⟨mk⟩ -- note [use has_coe_t]
 
diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
index 774945da9661f..029642567f24a 100644
--- a/src/group_theory/quotient_group.lean
+++ b/src/group_theory/quotient_group.lean
@@ -38,11 +38,12 @@ proves Noether's first and second isomorphism theorems.
 isomorphism theorems, quotient groups
 -/
 
-universes u v
+universes u v w
 
 namespace quotient_group
 
 variables {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H]
+  {M : Type w} [monoid M]
 include nN
 
 /-- The congruence relation generated by a normal subgroup. -/
@@ -56,12 +57,10 @@ protected def con : con G :=
     ... ∈ N : N.mul_mem (nN.conj_mem _ hab _) hcd
   end }
 
-@[to_additive quotient_add_group.add_group]
-instance quotient.group : group (G ⧸ N) :=
-(quotient_group.con N).group
+@[to_additive] instance quotient.group : group (G ⧸ N) := (quotient_group.con N).group
 
 /-- The group homomorphism from `G` to `G/N`. -/
-@[to_additive quotient_add_group.mk' "The additive group homomorphism from `G` to `G/N`."]
+@[to_additive "The additive group homomorphism from `G` to `G/N`."]
 def mk' : G →* G ⧸ N := monoid_hom.mk' (quotient_group.mk) (λ _ _, rfl)
 
 @[simp, to_additive]
@@ -89,20 +88,17 @@ See note [partially-applied ext lemmas]. "-/]
 lemma monoid_hom_ext ⦃f g : G ⧸ N →* H⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
 monoid_hom.ext $ λ x, quotient_group.induction_on x $ (monoid_hom.congr_fun h : _)
 
-@[simp, to_additive quotient_add_group.eq_zero_iff]
+@[simp, to_additive]
 lemma eq_one_iff {N : subgroup G} [nN : N.normal] (x : G) : (x : G ⧸ N) = 1 ↔ x ∈ N :=
 begin
   refine quotient_group.eq.trans _,
   rw [mul_one, subgroup.inv_mem_iff],
 end
 
-@[simp, to_additive quotient_add_group.ker_mk]
-lemma ker_mk :
-  monoid_hom.ker (quotient_group.mk' N : G →* G ⧸ N) = N :=
+@[simp, to_additive] lemma ker_mk : (quotient_group.mk' N : G →* G ⧸ N).ker = N :=
 subgroup.ext eq_one_iff
 
-@[to_additive quotient_add_group.eq_iff_sub_mem]
-lemma eq_iff_div_mem {N : subgroup G} [nN : N.normal] {x y : G} :
+@[to_additive] lemma eq_iff_div_mem {N : subgroup G} [nN : N.normal] {x y : G} :
   (x : G ⧸ N) = y ↔ x / y ∈ N :=
 begin
   refine eq_comm.trans (quotient_group.eq.trans _),
@@ -112,8 +108,7 @@ end
 -- for commutative groups we don't need normality assumption
 omit nN
 
-@[to_additive quotient_add_group.add_comm_group]
-instance {G : Type*} [comm_group G] (N : subgroup G) : comm_group (G ⧸ N) :=
+@[to_additive] instance {G : Type*} [comm_group G] (N : subgroup G) : comm_group (G ⧸ N) :=
 { mul_comm := λ a b, quotient.induction_on₂' a b
     (λ a b, congr_arg mk (mul_comm a b)),
   .. @quotient_group.quotient.group _ _ N N.normal_of_comm }
@@ -122,77 +117,82 @@ include nN
 
 local notation ` Q ` := G ⧸ N
 
-@[simp, to_additive quotient_add_group.coe_zero]
-lemma coe_one : ((1 : G) : Q) = 1 := rfl
+@[simp, to_additive] lemma coe_one : ((1 : G) : Q) = 1 := rfl
+@[simp, to_additive] lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl
+@[simp, to_additive] lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl
+@[simp, to_additive] lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := rfl
+@[simp, to_additive] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := rfl
+@[simp, to_additive] lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := rfl
+
+/-- A homomorphism `φ : G →* M` from a group to a monoid with `N ⊆ monoid_hom.ker φ` descends
+(i.e. `lift`s) to a homomorphism `G ⧸ N →* M`. -/
+@[to_additive "An addtive monoid homomorphism `φ : G →+ M` from an additive group to an additive
+monoid with `N ⊆ add_monoid_hom.ker φ` descends (i.e. `lift`s) to an additive monoid homomorphism
+`G ⧸ N →+ H`."]
+def lift (φ : G →* M) (HN : N ≤ φ.ker) : Q →* M :=
+(quotient_group.con N).lift φ $ λ x y h, (φ.eq_iff.2 (HN $ left_rel_apply.1 h)).symm
+
+@[simp, to_additive]
+lemma lift_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q) = φ g := rfl
 
-@[simp, to_additive quotient_add_group.coe_add]
-lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl
+@[simp, to_additive]
+lemma lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk g : Q) = φ g := rfl
 
-@[simp, to_additive quotient_add_group.coe_neg]
-lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl
+@[simp, to_additive] lemma lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) :
+  lift N φ HN (quot.mk _ g : Q) = φ g :=
+rfl
 
-@[simp, to_additive quotient_add_group.coe_sub]
-lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := rfl
+@[simp, to_additive]
+lemma lift_comp_mk {φ : G →* M} (HN : N ≤ φ.ker) : (lift N φ HN).comp (mk' N) = φ :=
+monoid_hom.ext $ λ x, rfl
 
-@[simp, to_additive quotient_add_group.coe_nsmul]
-lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := rfl
+@[simp, to_additive]
+lemma comap_mk'_ker_lift {φ : G →* M} (HN : N ≤ φ.ker) :
+  (lift N φ HN).ker.comap (mk' N) = φ.ker :=
+rfl
 
-@[simp, to_additive quotient_add_group.coe_zsmul]
-lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := rfl
+@[to_additive] lemma ker_lift_eq {φ : G →* M} (HN : N ≤ φ.ker) :
+  (lift N φ HN).ker = φ.ker.map (mk' N) :=
+subgroup.comap_injective (mk'_surjective N) $
+  by rw [comap_mk'_ker_lift, subgroup.comap_map_eq, ker_mk, sup_of_le_left HN]
 
-/-- A group homomorphism `φ : G →* H` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
-group homomorphism `G/N →* H`. -/
-@[to_additive quotient_add_group.lift "An `add_group` homomorphism `φ : G →+ H` with `N ⊆ ker(φ)`
-descends (i.e. `lift`s) to a group homomorphism `G/N →* H`."]
-def lift (φ : G →* H) (HN : ∀x∈N, φ x = 1) : Q →* H :=
-(quotient_group.con N).lift φ $ λ x y h, begin
-  simp only [quotient_group.con, left_rel_apply, con.rel_mk] at h,
-  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]
-  end
+@[simp, to_additive] lemma lift_injective_iff {φ : G →* M} (HN : N ≤ φ.ker) :
+  function.injective (lift N φ HN) ↔ N = φ.ker :=
+by simp only [← monoid_hom.ker_eq_bot_iff, ker_lift_eq, subgroup.map_eq_bot_iff, ker_mk,
+  HN.le_iff_eq, eq_comm]
 
-@[simp, to_additive quotient_add_group.lift_mk]
-lemma lift_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) :
-  lift N φ HN (g : Q) = φ g := rfl
+@[simp, to_additive] lemma surjective_lift {φ : G →* M} (HN : N ≤ φ.ker) :
+  function.surjective (lift N φ HN) ↔ function.surjective φ :=
+quot.surjective_lift _
 
-@[simp, to_additive quotient_add_group.lift_mk']
-lemma lift_mk' {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) :
-  lift N φ HN (mk g : Q) = φ g := rfl
+@[simp, to_additive] lemma mrange_lift {φ : G →* M} (HN : N ≤ φ.ker) :
+  (lift N φ HN).mrange = φ.mrange :=
+set_like.ext' $ set.range_quotient_lift_on' _
 
-@[simp, to_additive quotient_add_group.lift_quot_mk]
-lemma lift_quot_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) :
-  lift N φ HN (quot.mk _ g : Q) = φ g := rfl
+@[simp, to_additive] lemma range_lift {φ : G →* H} (HN : N ≤ φ.ker) :
+  (lift N φ HN).range = φ.range :=
+set_like.ext' $ set.range_quotient_lift_on' _
 
 /-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/
-@[to_additive quotient_add_group.map "An `add_group` homomorphism `f : G →+ H` induces a map
+@[to_additive "An `add_group` 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 :=
-begin
-  refine quotient_group.lift N ((mk' M).comp f) _,
-  assume x hx,
-  refine quotient_group.eq.2 _,
-  rw [mul_one, subgroup.inv_mem_iff],
-  exact h hx,
-end
+quotient_group.lift N ((mk' M).comp f) $ by rwa [← (mk' M).comap_ker, ker_mk]
 
-@[simp, to_additive quotient_add_group.map_coe] lemma map_coe
-  (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+@[simp, to_additive]
+lemma map_coe (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
   map N M f h ↑x = ↑(f x) :=
-lift_mk' _ _ x
+rfl
 
-@[to_additive quotient_add_group.map_mk'] lemma map_mk'
-  (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+@[to_additive] lemma 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) :=
-quotient_group.lift_mk' _ _ x
+rfl
 
 @[to_additive]
 lemma map_id_apply (h : N ≤ subgroup.comap (monoid_hom.id _) N := (subgroup.comap_id N).le) (x) :
   map N N (monoid_hom.id _) h x = x :=
-begin
-  refine induction_on' x (λ x, _),
-  simp only [map_coe, monoid_hom.id_apply]
-end
+induction_on' x $ λ x, rfl
 
 @[simp, to_additive]
 lemma map_id (h : N ≤ subgroup.comap (monoid_hom.id _) N := (subgroup.comap_id N).le) :
@@ -263,85 +263,84 @@ rfl
 
 end congr
 
-variables (φ : G →* H)
+section ker_lift
+
+variables (φ : G →* M) (ψ : G →* H)
 
 open function monoid_hom
 
 /-- The induced map from the quotient by the kernel to the codomain. -/
-@[to_additive quotient_add_group.ker_lift "The induced map from the quotient by the kernel to the
-codomain."]
-def ker_lift : G ⧸ ker φ →* H :=
-lift _ φ $ λ g, φ.mem_ker.mp
+@[to_additive "The induced map from the quotient by the kernel to the codomain."]
+def ker_lift : G ⧸ ker φ →* M := lift φ.ker φ le_rfl
+
+@[simp, to_additive] lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g := rfl
+@[simp, to_additive] lemma ker_lift_mk' (g : G) : (ker_lift φ) (mk g) = φ g := rfl
 
-@[simp, to_additive quotient_add_group.ker_lift_mk]
-lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g :=
-lift_mk _ _ _
+@[to_additive] lemma ker_lift_injective : injective (ker_lift φ) := (lift_injective_iff _ _).2 rfl
 
-@[simp, to_additive quotient_add_group.ker_lift_mk']
-lemma ker_lift_mk' (g : G) : (ker_lift φ) (mk g) = φ g :=
-lift_mk' _ _ _
+@[simp, to_additive] lemma ker_ker_lift : (ker_lift φ).ker = ⊥ :=
+(ker_eq_bot_iff _).2 (ker_lift_injective _)
 
-@[to_additive quotient_add_group.ker_lift_injective]
-lemma ker_lift_injective : injective (ker_lift φ) :=
-assume a b, quotient.induction_on₂' a b $
-  assume a b (h : φ a = φ b), quotient.sound' $
-  by rw [left_rel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_self]
+@[simp, to_additive] lemma ker_lift_surjective : surjective (ker_lift φ) ↔ surjective φ :=
+surjective_lift _ _
 
--- Note that `ker φ` isn't definitionally `ker (φ.range_restrict)`
--- so there is a bit of annoying code duplication here
+@[simp, to_additive] lemma range_ker_lift_eq : (ker_lift ψ).range = ψ.range := range_lift _ _
 
 /-- The induced map from the quotient by the kernel to the range. -/
-@[to_additive quotient_add_group.range_ker_lift "The induced map from the quotient by the kernel to
-the range."]
-def range_ker_lift : G ⧸ ker φ →* φ.range :=
-lift _ φ.range_restrict $ λ g hg, (mem_ker _).mp $ by rwa range_restrict_ker
-
-@[to_additive quotient_add_group.range_ker_lift_injective]
-lemma range_ker_lift_injective : injective (range_ker_lift φ) :=
-assume a b, quotient.induction_on₂' a b $
-  assume a b (h : φ.range_restrict a = φ.range_restrict b), quotient.sound' $
-  by rw [left_rel_apply, ←range_restrict_ker, mem_ker,
-  φ.range_restrict.map_mul, ← h, φ.range_restrict.map_inv, inv_mul_self]
-
-@[to_additive quotient_add_group.range_ker_lift_surjective]
-lemma range_ker_lift_surjective : surjective (range_ker_lift φ) :=
-begin
-  rintro ⟨_, g, rfl⟩,
-  use mk g,
-  refl,
-end
+@[to_additive "The induced map from the quotient by the kernel to the range."]
+def range_ker_lift : G ⧸ ker ψ →* ψ.range := lift _ ψ.range_restrict ψ.ker_range_restrict.ge
+
+@[to_additive] lemma range_ker_lift_injective : injective (range_ker_lift ψ) :=
+(lift_injective_iff _ _).2 ψ.ker_range_restrict.symm
+
+@[to_additive] lemma range_ker_lift_surjective : surjective (range_ker_lift ψ) :=
+(surjective_lift _ _).2 ψ.range_restrict_surjective
+
+@[to_additive] lemma range_ker_lift_bijective : bijective (range_ker_lift ψ) :=
+⟨range_ker_lift_injective _, range_ker_lift_surjective _⟩
 
 /-- **Noether's first isomorphism theorem** (a definition): the canonical isomorphism between
 `G/(ker φ)` to `range φ`. -/
-@[to_additive quotient_add_group.quotient_ker_equiv_range "The first isomorphism theorem
-(a definition): the canonical isomorphism between `G/(ker φ)` to `range φ`."]
-noncomputable def quotient_ker_equiv_range : G ⧸ ker φ ≃* range φ :=
-mul_equiv.of_bijective (range_ker_lift φ) ⟨range_ker_lift_injective φ, range_ker_lift_surjective φ⟩
-
-/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a homomorphism `φ : G →* H`
-with a right inverse `ψ : H → G`. -/
-@[to_additive quotient_add_group.quotient_ker_equiv_of_right_inverse "The canonical isomorphism
-`G/(ker φ) ≃+ H` induced by a homomorphism `φ : G →+ H` with a right inverse `ψ : H → G`.",
-  simps]
-def quotient_ker_equiv_of_right_inverse (ψ : H → G) (hφ : function.right_inverse ψ φ) :
-  G ⧸ ker φ ≃* H :=
-{ to_fun := ker_lift φ,
+@[to_additive "The first isomorphism theorem (a definition): the canonical isomorphism between
+`G/(ker φ)` to `range φ`."]
+noncomputable def quotient_ker_equiv_range : G ⧸ ker ψ ≃* range ψ :=
+mul_equiv.of_bijective (range_ker_lift ψ) (range_ker_lift_bijective ψ)
+
+/-- The canonical isomorphism `G ⧸ N ≃* H`, `N = ker φ`, induced by a homomorphism `φ : G →* H`
+with a right inverse `ψ : H → G`.
+
+This version assumes `N = ker φ` to avoid issues with definitional equalities. -/
+@[to_additive "The canonical isomorphism `G ⧸ N ≃+ H`, `N = ker φ`, induced by a homomorphism
+`φ : G →+ H` with a right inverse `ψ : H → G`.
+
+This version assumes `N = ker φ` to avoid issues with definitional equalities.", simps]
+def quotient_equiv_of_right_inverse (ψ : M → G) (N : subgroup G) [N.normal] (HN : N = ker φ)
+  (hφ : function.right_inverse ψ φ) :
+  G ⧸ N ≃* M :=
+{ to_fun := lift N φ HN.le,
   inv_fun := mk ∘ ψ,
-  left_inv := λ x, ker_lift_injective φ (by rw [function.comp_app, ker_lift_mk', hφ]),
+  left_inv := λ x, (lift_injective_iff _ _).2 HN (by rw [function.comp_app, lift_mk', hφ]),
   right_inv := hφ,
-  .. ker_lift φ }
+  .. lift N φ HN.le }
 
-/-- The canonical isomorphism `G/⊥ ≃* G`. -/
-@[to_additive quotient_add_group.quotient_bot "The canonical isomorphism `G/⊥ ≃+ G`.", simps]
+/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a homomorphism `φ : G →* H`
+with a right inverse `ψ : H → G`. -/
+@[to_additive "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a homomorphism `φ : G →+ H`
+with a right inverse `ψ : H → G`.", simps]
+def quotient_ker_equiv_of_right_inverse (ψ : M → G) (hφ : function.right_inverse ψ φ) :
+  G ⧸ ker φ ≃* M :=
+quotient_equiv_of_right_inverse φ ψ _ rfl hφ
+
+/-- The canonical isomorphism `G ⧸ ⊥ ≃* G`. -/
+@[to_additive "The canonical isomorphism `G/⊥ ≃+ G`.", simps]
 def quotient_bot : G ⧸ (⊥ : subgroup G) ≃* G :=
-quotient_ker_equiv_of_right_inverse (monoid_hom.id G) id (λ x, rfl)
+quotient_equiv_of_right_inverse (monoid_hom.id G) id ⊥ (monoid_hom.ker_id _) (λ x, rfl)
 
 /-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a surjection `φ : G →* H`.
 
 For a `computable` version, see `quotient_group.quotient_ker_equiv_of_right_inverse`.
 -/
-@[to_additive quotient_add_group.quotient_ker_equiv_of_surjective "The canonical isomorphism
-`G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`.
+@[to_additive "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`.
 
 For a `computable` version, see `quotient_add_group.quotient_ker_equiv_of_right_inverse`."]
 noncomputable def quotient_ker_equiv_of_surjective (hφ : function.surjective φ) :
@@ -490,8 +489,7 @@ variables (M : subgroup G) [nM : M.normal]
 
 include nM nN
 
-@[to_additive quotient_add_group.map_normal]
-instance map_normal : (M.map (quotient_group.mk' N)).normal :=
+@[to_additive] instance map_normal : (M.map (quotient_group.mk' N)).normal :=
 { conj_mem := begin
     rintro _ ⟨x, hx, rfl⟩ y,
     refine induction_on' y (λ y, ⟨y * x * y⁻¹, subgroup.normal.conj_mem nM x hx y, _⟩),
@@ -501,8 +499,8 @@ instance map_normal : (M.map (quotient_group.mk' N)).normal :=
 variables (h : N ≤ M)
 
 /-- The map from the third isomorphism theorem for groups: `(G / N) / (M / N) → G / M`. -/
-@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux
-"The map from the third isomorphism theorem for additive groups: `(A / N) / (M / N) → A / M`."]
+@[to_additive "The map from the third isomorphism theorem for additive groups:
+`(A / N) / (M / N) → A / M`."]
 def quotient_quotient_equiv_quotient_aux :
   (G ⧸ N) ⧸ (M.map (mk' N)) →* G ⧸ M :=
 lift (M.map (mk' N))
@@ -510,20 +508,18 @@ lift (M.map (mk' N))
   (by { rintro _ ⟨x, hx, rfl⟩, rw map_mk' N M _ _ x,
         exact (quotient_group.eq_one_iff _).mpr hx })
 
-@[simp, to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe]
-lemma quotient_quotient_equiv_quotient_aux_coe (x : G ⧸ N) :
+@[simp, to_additive] lemma quotient_quotient_equiv_quotient_aux_coe (x : G ⧸ N) :
   quotient_quotient_equiv_quotient_aux N M h x = quotient_group.map N M (monoid_hom.id G) h x :=
 quotient_group.lift_mk' _ _ x
 
-@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe_coe]
-lemma quotient_quotient_equiv_quotient_aux_coe_coe (x : G) :
+@[to_additive] lemma quotient_quotient_equiv_quotient_aux_coe_coe (x : G) :
   quotient_quotient_equiv_quotient_aux N M h (x : G ⧸ N) =
     x :=
 quotient_group.lift_mk' _ _ x
 
-/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃ G / M`. -/
-@[to_additive quotient_add_group.quotient_quotient_equiv_quotient
-"**Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃ A / M`."]
+/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃* G / M`. -/
+@[to_additive "**Noether's third isomorphism theorem** for additive groups:
+`(A / N) / (M / N) ≃+ A / M`."]
 def quotient_quotient_equiv_quotient :
   (G ⧸ N) ⧸ (M.map (quotient_group.mk' N)) ≃* G ⧸ M :=
 monoid_hom.to_mul_equiv
@@ -554,7 +550,7 @@ top_unique $ λ x _,
 
 end trivial
 
-@[to_additive quotient_add_group.comap_comap_center]
+@[to_additive]
 lemma comap_comap_center {H₁ : subgroup G} [H₁.normal] {H₂ : subgroup (G ⧸ H₁)} [H₂.normal] :
   (((subgroup.center ((G ⧸ H₁) ⧸ H₂))).comap (mk' H₂)).comap (mk' H₁) =
   (subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁))) :=
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 3b59815b996ed..8edd695fdc43a 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -2087,9 +2087,17 @@ lemma mem_ker (f : G →* M) {x : G} : x ∈ f.ker ↔ f x = 1 := iff.rfl
 @[to_additive]
 lemma coe_ker (f : G →* M) : (f.ker : set G) = (f : G → M) ⁻¹' {1} := rfl
 
+@[simp, to_additive]
+lemma ker_to_hom_units {M} [monoid M] (f : G →* M) : f.to_hom_units.ker = f.ker :=
+by { ext x, simp [mem_ker, units.ext_iff] }
+
 @[to_additive]
-lemma eq_iff (f : G →* N) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker :=
-by rw [f.mem_ker, f.map_mul, f.map_inv, inv_mul_eq_one, eq_comm]
+lemma eq_iff (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker :=
+begin
+  split; intro h,
+  { rw [mem_ker, map_mul, h, ← map_mul, inv_mul_self, map_one] },
+  { rw [← one_mul x, ← mul_inv_self y, mul_assoc, map_mul, f.mem_ker.1 h, mul_one] }
+end
 
 @[to_additive]
 instance decidable_mem_ker [decidable_eq M] (f : G →* M) :
@@ -2105,24 +2113,19 @@ lemma comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker :
 @[simp, to_additive] lemma restrict_ker (f : G →* N) : (f.restrict K).ker = f.ker.subgroup_of K :=
 rfl
 
-@[to_additive] lemma range_restrict_ker  (f : G →* N) : ker (range_restrict f) = ker f :=
-begin
-  ext,
-  change (⟨f x, _⟩ : range f) = ⟨1, _⟩ ↔ f x = 1,
-  simp only [],
-end
+@[simp, to_additive] lemma ker_cod_restrict {S} [set_like S N] [submonoid_class S N] (f : G →* N)
+  (s : S) (h : ∀ x, f x ∈ s) : (f.cod_restrict s h).ker = f.ker :=
+set_like.ext $ λ x, subtype.ext_iff
 
-@[simp, to_additive]
-lemma ker_one : (1 : G →* M).ker = ⊤ :=
-by { ext, simp [mem_ker] }
+@[simp, to_additive] lemma ker_range_restrict  (f : G →* N) : ker (range_restrict f) = ker f :=
+ker_cod_restrict _ _ _
 
-@[to_additive] lemma ker_eq_bot_iff (f : G →* N) : f.ker = ⊥ ↔ function.injective f :=
-begin
-  split,
-  { intros h x y hxy,
-    rwa [←mul_inv_eq_one, ←map_inv, ←map_mul, ←mem_ker, h, mem_bot, mul_inv_eq_one] at hxy },
-  { exact λ h, le_bot_iff.mp (λ x hx, h (hx.trans f.map_one.symm)) },
-end
+@[simp, to_additive] lemma ker_one : (1 : G →* M).ker = ⊤ := set_like.ext $ λ x, eq_self_iff_true _
+@[simp, to_additive] lemma ker_id : (monoid_hom.id G).ker = ⊥ := rfl
+
+@[to_additive] lemma ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ function.injective f :=
+⟨λ h x y hxy, by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy,
+  λ h, bot_unique $ λ x hx, h (hx.trans f.map_one.symm)⟩
 
 @[simp, to_additive] lemma _root_.subgroup.ker_subtype (H : subgroup G) : H.subtype.ker = ⊥ :=
 H.subtype.ker_eq_bot_iff.mpr subtype.coe_injective
@@ -2142,24 +2145,26 @@ lemma ker_prod_map {G' : Type*} {N' : Type*} [group G'] [group N'] (f : G →* N
   (prod_map f g).ker = f.ker.prod g.ker :=
 by rw [←comap_bot, ←comap_bot, ←comap_bot, ←prod_map_comap_prod, bot_prod_bot]
 
+@[priority 100, to_additive]
+instance normal_ker (f : G →* M) : f.ker.normal :=
+⟨λ x hx y, by rw [mem_ker, map_mul, map_mul, f.mem_ker.1 hx, mul_one,
+  map_mul_eq_one f (mul_inv_self y)]⟩
+
 variables [monoid N]
 
-@[simp, to_additive] lemma preimage_mul_left_ker (f : G →* N) (x : G) :
+@[simp, to_additive] lemma preimage_mul_left_ker (f : G →* M) (x : G) :
   ((*) x) ⁻¹' f.ker = f ⁻¹' {f x⁻¹} :=
 begin
   ext y,
-  rcases mul_left_surjective x⁻¹ y with ⟨y, rfl⟩,
-  simp only [set.mem_preimage, set_like.mem_coe, set.mem_singleton_iff, mem_ker,
-    mul_inv_cancel_left, map_mul, ((group.is_unit _).map f).mul_right_eq_self]
+  simp only [eq_iff, set.mem_preimage, set_like.mem_coe, set.mem_singleton_iff, inv_inv]
 end
 
 @[simp, to_additive] lemma preimage_mul_right_ker (f : G →* N) (x : G) :
   (λ y, y * x) ⁻¹' f.ker = f ⁻¹' {f x⁻¹} :=
 begin
   ext y,
-  rcases mul_right_surjective x⁻¹ y with ⟨y, rfl⟩,
-  simp only [set.mem_preimage, set_like.mem_coe, set.mem_singleton_iff, mem_ker,
-    inv_mul_cancel_right, map_mul, ((group.is_unit _).map f).mul_left_eq_self]
+  simpa only [eq_iff, set.mem_preimage, set_like.mem_coe, set.mem_singleton_iff, inv_inv]
+    using f.normal_ker.mem_comm_iff
 end
 
 @[simp, to_additive] lemma image_mul_left_ker (f : G →* N) (x : G) :
@@ -2595,10 +2600,6 @@ lemma subgroup.normal.comap {H : subgroup N} (hH : H.normal) (f : G →* N) :
 instance subgroup.normal_comap {H : subgroup N}
   [nH : H.normal] (f : G →* N) :  (H.comap f).normal := nH.comap _
 
-@[priority 100, to_additive]
-instance monoid_hom.normal_ker (f : G →* N) : f.ker.normal :=
-by { rw [←f.comap_bot], apply_instance }
-
 @[priority 100, to_additive]
 instance subgroup.normal_inf (H N : subgroup G) [hN : N.normal] :
   ((H ⊓ N).comap H.subtype).normal :=
diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
index 244f95ddb959e..13307294b3278 100644
--- a/src/ring_theory/integral_domain.lean
+++ b/src/ring_theory/integral_domain.lean
@@ -121,6 +121,9 @@ instance subgroup_units_cyclic (S : subgroup Rˣ) [finite S] : is_cyclic S :=
 is_cyclic_of_subgroup_is_domain ((units.coe_hom R).comp S.subtype)
   (units.ext.comp subtype.coe_injective)
 
+instance is_domain.is_cyclic_quotient_ker [finite G] {f : G →* R} : is_cyclic (G ⧸ f.ker) :=
+is_cyclic_of_subgroup_is_domain (quotient_group.ker_lift f)
+
 variables [fintype G]
 
 /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.

From 335d2cfab6d2b8e891253efd2f8ff66a506b47ac Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 23 Nov 2022 13:07:37 -0600
Subject: [PATCH 05/12] Snapshot

---
 src/data/quot.lean      | 17 +++++++++++++----
 src/data/set/basic.lean | 29 ++++++++++++++++++++++++++---
 2 files changed, 39 insertions(+), 7 deletions(-)

diff --git a/src/data/quot.lean b/src/data/quot.lean
index b082163abe85a..0b17e5e3db445 100644
--- a/src/data/quot.lean
+++ b/src/data/quot.lean
@@ -21,6 +21,8 @@ quotient
 
 variables {α : Sort*} {β : Sort*}
 
+open function
+
 namespace setoid
 
 lemma ext {α : Sort*} :
@@ -72,13 +74,17 @@ lemma factor_mk_eq {α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y 
 variables {γ : Sort*} {r : α → α → Prop} {s : β → β → Prop}
 
 /-- **Alias** of `quot.lift_beta`. -/
-lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
-  quot.lift f h (quot.mk r a) = f a := quot.lift_beta f h a
+@[simp] lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
+  quot.lift f h (quot.mk r a) = f a := rfl
 
 @[simp]
 lemma lift_on_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
   quot.lift_on (quot.mk r a) f h = f a := rfl
 
+@[simp] lemma surjective_lift {f : α → γ} (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
+  surjective (lift f h) ↔ surjective f :=
+⟨λ hf, hf.comp quot.exists_rep, λ hf y, let ⟨x, hx⟩ := hf y in ⟨quot.mk _ x, hx⟩⟩
+
 /-- Descends a function `f : α → β → γ` to quotients of `α` and `β`. -/
 attribute [reducible, elab_as_eliminator]
 protected def lift₂
@@ -272,8 +278,7 @@ rfl
   quotient.lift_on₂ (quotient.mk x) (quotient.mk y) f h = f x y := rfl
 
 /-- `quot.mk r` is a surjective function. -/
-lemma surjective_quot_mk (r : α → α → Prop) : function.surjective (quot.mk r) :=
-quot.exists_rep
+lemma surjective_quot_mk (r : α → α → Prop) : surjective (quot.mk r) := quot.exists_rep
 
 /-- `quotient.mk` is a surjective function. -/
 lemma surjective_quotient_mk (α : Sort*) [s : setoid α] :
@@ -482,6 +487,10 @@ protected def lift_on' (q : quotient s₁) (f : α → φ)
 protected lemma lift_on'_mk' (f : α → φ) (h) (x : α) :
   quotient.lift_on' (@quotient.mk' _ s₁ x) f h = f x := rfl
 
+@[simp] lemma surjective_lift_on' {f : α → φ} (h : ∀ a b, @setoid.r α s₁ a b → f a = f b) :
+  surjective (λ x, quotient.lift_on' x f h) ↔ surjective f :=
+quot.surjective_lift _
+
 /-- A version of `quotient.lift_on₂` taking `{s₁ : setoid α} {s₂ : setoid β}` as implicit arguments
 instead of instance arguments. -/
 @[elab_as_eliminator, reducible]
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 65eab1507f17d..9d09eebaf500e 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -2284,13 +2284,36 @@ by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_d
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
 (surjective_quot_mk r).range_eq
 
-instance can_lift (c) (p) [can_lift α β c p] :
-  can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
-{ prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
+@[simp] theorem range_quot_lift {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) :
+  range (quot.lift f hf) = range f :=
+ext $ λ y, (surjective_quot_mk _).exists
+
+@[simp] theorem range_quot_lift_on {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) :
+  range (λ x, quot.lift_on x f hf) = range f :=
+range_quot_lift _
 
 @[simp] theorem range_quotient_mk [setoid α] : range (λx : α, ⟦x⟧) = univ :=
 range_quot_mk _
 
+@[simp] theorem range_quotient_lift [s : setoid ι] (hf) :
+  range (quotient.lift f hf : quotient s → α) = range f :=
+range_quot_lift _
+
+@[simp] theorem range_quotient_mk' {s : setoid α} : range (quotient.mk' : α → quotient s) = univ :=
+range_quot_mk _
+
+@[simp] theorem range_quotient_lift_on' {s : setoid ι} (hf) :
+  range (λ x : quotient s, quotient.lift_on' x f hf) = range f :=
+range_quot_lift _
+
+@[simp] theorem range_quotient_lift_on [s : setoid ι] (hf) :
+  range (λ x : quotient s, quotient.lift_on x f hf) = range f :=
+range_quot_lift _
+
+instance can_lift (c) (p) [can_lift α β c p] :
+  can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
+{ prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
+
 lemma range_const_subset {c : α} : range (λ x : ι, c) ⊆ {c} :=
 range_subset_iff.2 $ λ x, rfl
 

From 22747060da0509fb9c48c294189e3c4f2dac1467 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 23 Nov 2022 13:55:19 -0600
Subject: [PATCH 06/12] Snapshot

---
 src/algebra/hom/units.lean           |  6 ++-
 src/group_theory/subgroup/basic.lean | 66 ++++++++++++----------------
 2 files changed, 33 insertions(+), 39 deletions(-)

diff --git a/src/algebra/hom/units.lean b/src/algebra/hom/units.lean
index bd660360a96d1..9e5a0f813322b 100644
--- a/src/algebra/hom/units.lean
+++ b/src/algebra/hom/units.lean
@@ -142,8 +142,10 @@ units.lift_right f
   (λ g, ⟨f g, f g⁻¹, map_mul_eq_one f (mul_inv_self _), map_mul_eq_one f (inv_mul_self _)⟩)
   (λ g, rfl)
 
-@[simp] lemma coe_to_hom_units {G M : Type*} [group G] [monoid M] (f : G →* M) (g : G):
-  (f.to_hom_units g : M) = f g := rfl
+@[simp, to_additive]
+lemma coe_to_hom_units {G M : Type*} [group G] [monoid M] (f : G →* M) (g : G) :
+  (f.to_hom_units g : M) = f g :=
+rfl
 
 end monoid_hom
 
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 6e30356f5b31c..2d600055e260d 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -2087,9 +2087,17 @@ lemma mem_ker (f : G →* M) {x : G} : x ∈ f.ker ↔ f x = 1 := iff.rfl
 @[to_additive]
 lemma coe_ker (f : G →* M) : (f.ker : set G) = (f : G → M) ⁻¹' {1} := rfl
 
+@[simp, to_additive]
+lemma ker_to_hom_units {M} [monoid M] (f : G →* M) : f.to_hom_units.ker = f.ker :=
+by { ext x, simp [mem_ker, units.ext_iff] }
+
 @[to_additive]
-lemma eq_iff (f : G →* N) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker :=
-by rw [f.mem_ker, f.map_mul, f.map_inv, inv_mul_eq_one, eq_comm]
+lemma eq_iff (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker :=
+begin
+  split; intro h,
+  { rw [mem_ker, map_mul, h, ← map_mul, inv_mul_self, map_one] },
+  { rw [← one_mul x, ← mul_inv_self y, mul_assoc, map_mul, f.mem_ker.1 h, mul_one] }
+end
 
 @[to_additive]
 instance decidable_mem_ker [decidable_eq M] (f : G →* M) :
@@ -2105,24 +2113,19 @@ lemma comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker :
 @[simp, to_additive] lemma restrict_ker (f : G →* N) : (f.restrict K).ker = f.ker.subgroup_of K :=
 rfl
 
-@[to_additive] lemma range_restrict_ker  (f : G →* N) : ker (range_restrict f) = ker f :=
-begin
-  ext,
-  change (⟨f x, _⟩ : range f) = ⟨1, _⟩ ↔ f x = 1,
-  simp only [],
-end
+@[simp, to_additive] lemma ker_cod_restrict {S} [set_like S N] [submonoid_class S N] (f : G →* N)
+  (s : S) (h : ∀ x, f x ∈ s) : (f.cod_restrict s h).ker = f.ker :=
+set_like.ext $ λ x, subtype.ext_iff
 
-@[simp, to_additive]
-lemma ker_one : (1 : G →* M).ker = ⊤ :=
-by { ext, simp [mem_ker] }
+@[simp, to_additive] lemma ker_range_restrict  (f : G →* N) : ker (range_restrict f) = ker f :=
+ker_cod_restrict _ _ _
 
-@[to_additive] lemma ker_eq_bot_iff (f : G →* N) : f.ker = ⊥ ↔ function.injective f :=
-begin
-  split,
-  { intros h x y hxy,
-    rwa [←mul_inv_eq_one, ←map_inv, ←map_mul, ←mem_ker, h, mem_bot, mul_inv_eq_one] at hxy },
-  { exact λ h, le_bot_iff.mp (λ x hx, h (hx.trans f.map_one.symm)) },
-end
+@[simp, to_additive] lemma ker_one : (1 : G →* M).ker = ⊤ := set_like.ext $ λ x, eq_self_iff_true _
+@[simp, to_additive] lemma ker_id : (monoid_hom.id G).ker = ⊥ := rfl
+
+@[to_additive] lemma ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ function.injective f :=
+⟨λ h x y hxy, by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy,
+  λ h, bot_unique $ λ x hx, h (hx.trans f.map_one.symm)⟩
 
 @[simp, to_additive] lemma _root_.subgroup.ker_subtype (H : subgroup G) : H.subtype.ker = ⊥ :=
 H.subtype.ker_eq_bot_iff.mpr subtype.coe_injective
@@ -2142,6 +2145,10 @@ lemma ker_prod_map {G' : Type*} {N' : Type*} [group G'] [group N'] (f : G →* N
   (prod_map f g).ker = f.ker.prod g.ker :=
 by rw [←comap_bot, ←comap_bot, ←comap_bot, ←prod_map_comap_prod, bot_prod_bot]
 
+@[priority 100, to_additive]
+instance normal_ker (f : G →* M) : f.ker.normal :=
+⟨λ x hx y, by rw [mem_ker, map_mul, map_mul, f.mem_ker.1 hx, mul_one,
+  map_mul_eq_one f (mul_inv_self y)]⟩
 end ker
 
 /-- The subgroup of elements `x : G` such that `f x = g x` -/
@@ -2213,14 +2220,7 @@ namespace subgroup
 variables {N : Type*} [group N] (H : subgroup G)
 
 @[to_additive] lemma map_eq_bot_iff {f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker :=
-begin
-  rw eq_bot_iff,
-  split,
-  { exact λ h x hx, h ⟨x, hx, rfl⟩ },
-  { intros h x hx,
-    obtain ⟨y, hy, rfl⟩ := hx,
-    exact h hy },
-end
+(gc_map_comap f).l_eq_bot
 
 @[to_additive]
 lemma map_eq_bot_iff_of_injective {f : G →* N} (hf : function.injective f) : H.map f = ⊥ ↔ H = ⊥ :=
@@ -2257,10 +2257,8 @@ lemma le_comap_map (H : subgroup G) : H ≤ comap f (map f H) :=
 @[to_additive]
 lemma map_comap_eq (H : subgroup N) :
   map f (comap f H) = f.range ⊓ H :=
-set_like.ext' begin
-  convert set.image_preimage_eq_inter_range,
-  simp [set.inter_comm],
-end
+set_like.ext' $ by rw [coe_map, coe_comap, set.image_preimage_eq_inter_range, coe_inf, coe_range,
+  set.inter_comm]
 
 @[to_additive]
 lemma comap_map_eq (H : subgroup G) : comap f (map f H) = H ⊔ f.ker :=
@@ -2569,10 +2567,6 @@ lemma subgroup.normal.comap {H : subgroup N} (hH : H.normal) (f : G →* N) :
 instance subgroup.normal_comap {H : subgroup N}
   [nH : H.normal] (f : G →* N) :  (H.comap f).normal := nH.comap _
 
-@[priority 100, to_additive]
-instance monoid_hom.normal_ker (f : G →* N) : f.ker.normal :=
-by { rw [←f.comap_bot], apply_instance }
-
 @[priority 100, to_additive]
 instance subgroup.normal_inf (H N : subgroup G) [hN : N.normal] :
   ((H ⊓ N).comap H.subtype).normal :=
@@ -2810,9 +2804,7 @@ instance : is_modular_lattice (subgroup C) :=
   rw [mem_inf, mem_sup] at ha,
   rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩,
   rw mem_sup,
-  refine ⟨b, hb, c, mem_inf.2 ⟨hc, _⟩, rfl⟩,
-  rw ← inv_mul_cancel_left b c,
-  apply z.mul_mem (z.inv_mem (xz hb)) haz,
+  exact ⟨b, hb, c, mem_inf.2 ⟨hc, (mul_mem_cancel_left (xz hb)).1 haz⟩, rfl⟩
 end⟩
 
 end subgroup

From 289e66f86a043e9f29ea826ad903e55e592fb48a Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 23 Nov 2022 13:57:30 -0600
Subject: [PATCH 07/12] Revert

---
 src/group_theory/quotient_group.lean | 4 ++--
 src/group_theory/subgroup/basic.lean | 5 -----
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
index 774945da9661f..c7ba6b3dd8f4a 100644
--- a/src/group_theory/quotient_group.lean
+++ b/src/group_theory/quotient_group.lean
@@ -294,13 +294,13 @@ assume a b, quotient.induction_on₂' a b $
 @[to_additive quotient_add_group.range_ker_lift "The induced map from the quotient by the kernel to
 the range."]
 def range_ker_lift : G ⧸ ker φ →* φ.range :=
-lift _ φ.range_restrict $ λ g hg, (mem_ker _).mp $ by rwa range_restrict_ker
+lift _ φ.range_restrict $ λ g hg, (mem_ker _).mp $ by rwa ker_range_restrict
 
 @[to_additive quotient_add_group.range_ker_lift_injective]
 lemma range_ker_lift_injective : injective (range_ker_lift φ) :=
 assume a b, quotient.induction_on₂' a b $
   assume a b (h : φ.range_restrict a = φ.range_restrict b), quotient.sound' $
-  by rw [left_rel_apply, ←range_restrict_ker, mem_ker,
+  by rw [left_rel_apply, ←ker_range_restrict, mem_ker,
   φ.range_restrict.map_mul, ← h, φ.range_restrict.map_inv, inv_mul_self]
 
 @[to_additive quotient_add_group.range_ker_lift_surjective]
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 2d600055e260d..89739c2f5e712 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -2087,10 +2087,6 @@ lemma mem_ker (f : G →* M) {x : G} : x ∈ f.ker ↔ f x = 1 := iff.rfl
 @[to_additive]
 lemma coe_ker (f : G →* M) : (f.ker : set G) = (f : G → M) ⁻¹' {1} := rfl
 
-@[simp, to_additive]
-lemma ker_to_hom_units {M} [monoid M] (f : G →* M) : f.to_hom_units.ker = f.ker :=
-by { ext x, simp [mem_ker, units.ext_iff] }
-
 @[to_additive]
 lemma eq_iff (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker :=
 begin
@@ -2121,7 +2117,6 @@ set_like.ext $ λ x, subtype.ext_iff
 ker_cod_restrict _ _ _
 
 @[simp, to_additive] lemma ker_one : (1 : G →* M).ker = ⊤ := set_like.ext $ λ x, eq_self_iff_true _
-@[simp, to_additive] lemma ker_id : (monoid_hom.id G).ker = ⊥ := rfl
 
 @[to_additive] lemma ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ function.injective f :=
 ⟨λ h x y hxy, by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy,

From 62c93adf2d0c400e107612de44dda51247c1672e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 23 Nov 2022 16:19:34 -0600
Subject: [PATCH 08/12] Fix

---
 src/linear_algebra/matrix/sesquilinear_form.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/linear_algebra/matrix/sesquilinear_form.lean b/src/linear_algebra/matrix/sesquilinear_form.lean
index b2aa3ec2bcf12..53f690ff9cb04 100644
--- a/src/linear_algebra/matrix/sesquilinear_form.lean
+++ b/src/linear_algebra/matrix/sesquilinear_form.lean
@@ -315,11 +315,7 @@ by simp only [linear_map.to_matrix₂, linear_equiv.trans_apply, linear_map.to_m
 
 @[simp] lemma matrix.to_linear_map₂_apply (M : matrix n m R) (x : M₁) (y : M₂) :
   matrix.to_linear_map₂ b₁ b₂ M x y = ∑ i j, b₁.repr x i * M i j * b₂.repr y j :=
-begin
-  rw [matrix.to_linear_map₂, linear_map.to_matrix₂, linear_equiv.symm_trans_apply,
-    ←matrix.to_linear_map₂'],
-  simp [matrix.to_linear_map₂'_apply],
-end
+rfl
 
 -- Not a `simp` lemma since `linear_map.to_matrix₂` needs an extra argument
 lemma linear_map.to_matrix₂_aux_eq (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :

From 066adeafc7fa5f4f4b1fb1071adfc1490a04095f Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 23 Nov 2022 23:01:51 -0600
Subject: [PATCH 09/12] Apply suggestions from code review

---
 src/data/quot.lean      | 2 +-
 src/data/set/basic.lean | 8 --------
 2 files changed, 1 insertion(+), 9 deletions(-)

diff --git a/src/data/quot.lean b/src/data/quot.lean
index 0b17e5e3db445..ccc67d3f9a5b5 100644
--- a/src/data/quot.lean
+++ b/src/data/quot.lean
@@ -74,7 +74,7 @@ lemma factor_mk_eq {α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y 
 variables {γ : Sort*} {r : α → α → Prop} {s : β → β → Prop}
 
 /-- **Alias** of `quot.lift_beta`. -/
-@[simp] lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
+lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
   quot.lift f h (quot.mk r a) = f a := rfl
 
 @[simp]
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 9d09eebaf500e..fbc848343a423 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -2288,10 +2288,6 @@ by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_d
   range (quot.lift f hf) = range f :=
 ext $ λ y, (surjective_quot_mk _).exists
 
-@[simp] theorem range_quot_lift_on {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) :
-  range (λ x, quot.lift_on x f hf) = range f :=
-range_quot_lift _
-
 @[simp] theorem range_quotient_mk [setoid α] : range (λx : α, ⟦x⟧) = univ :=
 range_quot_mk _
 
@@ -2306,10 +2302,6 @@ range_quot_mk _
   range (λ x : quotient s, quotient.lift_on' x f hf) = range f :=
 range_quot_lift _
 
-@[simp] theorem range_quotient_lift_on [s : setoid ι] (hf) :
-  range (λ x : quotient s, quotient.lift_on x f hf) = range f :=
-range_quot_lift _
-
 instance can_lift (c) (p) [can_lift α β c p] :
   can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
 { prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }

From 9c9e80861bc97b7719ce0242ee4acec2d8042ea5 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 24 Nov 2022 10:40:57 -0600
Subject: [PATCH 10/12] Take advantage of `open function`

---
 src/data/quot.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/data/quot.lean b/src/data/quot.lean
index 0b17e5e3db445..dc8a2b0e20724 100644
--- a/src/data/quot.lean
+++ b/src/data/quot.lean
@@ -282,7 +282,7 @@ lemma surjective_quot_mk (r : α → α → Prop) : surjective (quot.mk r) := qu
 
 /-- `quotient.mk` is a surjective function. -/
 lemma surjective_quotient_mk (α : Sort*) [s : setoid α] :
-  function.surjective (quotient.mk : α → quotient s) :=
+  surjective (quotient.mk : α → quotient s) :=
 quot.exists_rep
 
 /-- Choose an element of the equivalence class using the axiom of choice.
@@ -324,7 +324,7 @@ end
   x.out ≈ y.out ↔ x = y :=
 by rw [← quotient.eq_mk_iff_out, quotient.out_eq]
 
-lemma quotient.out_injective {s : setoid α} : function.injective (@quotient.out α s) :=
+lemma quotient.out_injective {s : setoid α} : injective (@quotient.out α s) :=
 λ a b h, quotient.out_equiv_out.1 $ h ▸ setoid.refl _
 
 @[simp] lemma quotient.out_inj {s : setoid α} {x y : quotient s} :
@@ -474,7 +474,7 @@ instance argument. -/
 protected def mk' (a : α) : quotient s₁ := quot.mk s₁.1 a
 
 /-- `quotient.mk'` is a surjective function. -/
-lemma surjective_quotient_mk' : function.surjective (quotient.mk' : α → quotient s₁) :=
+lemma surjective_quotient_mk' : surjective (quotient.mk' : α → quotient s₁) :=
 quot.exists_rep
 
 /-- A version of `quotient.lift_on` taking `{s : setoid α}` as an implicit argument instead of an

From 37299303ba6b263f199eb3954723f4d91e85ea49 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 24 Nov 2022 10:44:17 -0600
Subject: [PATCH 11/12] Apply suggestions from code review

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
---
 src/group_theory/subgroup/basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 89739c2f5e712..0bb15d2a5a654 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -2106,7 +2106,7 @@ lemma comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker :
 @[simp, to_additive] lemma comap_bot (f : G →* N) :
   (⊥ : subgroup N).comap f = f.ker := rfl
 
-@[simp, to_additive] lemma restrict_ker (f : G →* N) : (f.restrict K).ker = f.ker.subgroup_of K :=
+@[simp, to_additive] lemma ker_restrict (f : G →* N) : (f.restrict K).ker = f.ker.subgroup_of K :=
 rfl
 
 @[simp, to_additive] lemma ker_cod_restrict {S} [set_like S N] [submonoid_class S N] (f : G →* N)
@@ -2144,6 +2144,7 @@ by rw [←comap_bot, ←comap_bot, ←comap_bot, ←prod_map_comap_prod, bot_pro
 instance normal_ker (f : G →* M) : f.ker.normal :=
 ⟨λ x hx y, by rw [mem_ker, map_mul, map_mul, f.mem_ker.1 hx, mul_one,
   map_mul_eq_one f (mul_inv_self y)]⟩
+
 end ker
 
 /-- The subgroup of elements `x : G` such that `f x = g x` -/

From 3ce812e850b126512da8d63048dfea8960ac825e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 24 Nov 2022 10:50:04 -0600
Subject: [PATCH 12/12] Fix

---
 src/group_theory/transfer.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/group_theory/transfer.lean b/src/group_theory/transfer.lean
index 0592f40c9e496..12fa2a55ae3b6 100644
--- a/src/group_theory/transfer.lean
+++ b/src/group_theory/transfer.lean
@@ -210,7 +210,7 @@ begin
   have := range_top_iff_surjective.mp (top_le_iff.mp (hf.2.ge.trans (map_le_range _ P))),
   rw [←(comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, set_like.ext'_iff,
       normal_mul, ←ker_eq_bot_iff, ←(map_injective (P : subgroup G).subtype_injective).eq_iff,
-      restrict_ker, subgroup_of_map_subtype, subgroup.map_bot, coe_top] at hf,
+      ker_restrict, subgroup_of_map_subtype, subgroup.map_bot, coe_top] at hf,
   exact is_complement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2,
 end