diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
index a8d5ad8fdc841..deb1758de2aba 100644
--- a/src/algebra/group/units.lean
+++ b/src/algebra/group/units.lean
@@ -490,6 +490,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/coset.lean b/src/group_theory/coset.lean
index 01fc5e6c7e3e5..af09f85fa0945 100644
--- a/src/group_theory/coset.lean
+++ b/src/group_theory/coset.lean
@@ -329,10 +329,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 f4145c16e1f07..9bb38467b9222 100644
--- a/src/group_theory/quotient_group.lean
+++ b/src/group_theory/quotient_group.lean
@@ -43,11 +43,12 @@ isomorphism theorems, quotient groups
 -/
 
 open function
-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. -/
@@ -99,12 +100,10 @@ begin
   rw [mul_one, subgroup.inv_mem_iff],
 end
 
-@[simp, to_additive]
-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]
-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 _),
@@ -157,13 +156,7 @@ lemma lift_quot_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) :
 `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] lemma map_coe (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f)
   (x : G) :
@@ -248,7 +241,9 @@ rfl
 
 end congr
 
-variables (φ : G →* H)
+section ker_lift
+
+variables (φ : G →* M) (ψ : G →* H)
 
 open monoid_hom
 
@@ -269,8 +264,10 @@ 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]
 
--- Note that `ker φ` isn't definitionally `ker (φ.range_restrict)`
--- so there is a bit of annoying code duplication here
+@[simp, to_additive] lemma ker_lift_surjective : surjective (ker_lift φ) ↔ surjective φ :=
+surjective_lift _ _
+
+@[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 "The induced map from the quotient by the kernel to the range."]
@@ -314,7 +311,7 @@ def quotient_ker_equiv_of_right_inverse (ψ : H → G) (hφ : right_inverse ψ 
 /-- 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`.
 
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 26cf2cc379965..5055540c0d7d3 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -2011,6 +2011,36 @@ 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)]⟩
 
+@[simp, to_additive] lemma preimage_mul_left_ker (f : G →* M) (x : G) :
+  ((*) x) ⁻¹' f.ker = f ⁻¹' {f x⁻¹} :=
+begin
+  ext y,
+  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 →* M) (x : G) :
+  (λ y, y * x) ⁻¹' f.ker = f ⁻¹' {f x⁻¹} :=
+begin
+  ext y,
+  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 →* M) (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 →* M) (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 →* M) (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
 
 section eq_locus
diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
index 1f325173541f9..1238a6ec208b9 100644
--- a/src/ring_theory/integral_domain.lean
+++ b/src/ring_theory/integral_domain.lean
@@ -144,20 +144,13 @@ 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
+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)
 
-end
+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)
 
 section euclidean_division
 
@@ -184,55 +177,40 @@ end euclidean_division
 
 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) :
-  (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], }
-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 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