diff --git a/group_theory/coset.lean b/group_theory/coset.lean
index fdfb83e477756..ab98bb2a42d07 100644
--- a/group_theory/coset.lean
+++ b/group_theory/coset.lean
@@ -3,8 +3,7 @@ Copyright (c) 2018 Mitchell Rowett. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mitchell Rowett, Scott Morrison
 -/
-
-import group_theory.subgroup
+import group_theory.subgroup data.set.basic
 
 open set
 
@@ -35,89 +34,39 @@ end coset_mul
 section coset_semigroup
 variable [semigroup γ]
 
-lemma left_coset_assoc (s : set γ) (a b : γ) : a *l (b *l s) = (a * b) *l s :=
-have h : (λ x : γ, a * x) ∘ (λ x : γ, b * x) = (λ x : γ, (a * b) * x), from
-  funext (λ c : γ,
-    calc ((λ x : γ, a * x) ∘ (λ x : γ, b * x)) c = a * (b * c) : by simp
-    ... = (λ x : γ, (a * b) * x) c : by rw ← mul_assoc; simp ),
-calc a *l (b *l s) = image ((λ x : γ, a * x) ∘ (λ x : γ, b * x)) s :
-    by rw [left_coset, left_coset, ←image_comp]
-  ... = (a * b) *l s : by rw [left_coset, h]
-
-lemma right_coset_assoc (s : set γ) (a b : γ) : s *r a *r b = s *r (a * b) :=
-have h : (λ x : γ, x * b) ∘ (λ x : γ, x * a) = (λ x : γ, x * (a * b)), from
-  funext (λ c : γ,
-    calc ((λ x : γ, x * b) ∘ (λ x : γ, x * a)) c = c * a * b :
-        by simp
-      ... = (λ x : γ, x * (a * b)) c :
-        by rw mul_assoc; simp),
-calc s *r a *r b  = image ((λ x : γ, x * b) ∘ (λ x : γ, x * a)) s :
-    by rw [right_coset, right_coset, ←image_comp]
-  ... = s *r (a * b) :
-    by rw [right_coset, h]
-
-lemma left_coset_right_coset (s : set γ) (a b : γ) : a *l s *r  b = a *l (s *r b) :=
-have h : (λ x : γ, x * b) ∘ (λ x : γ, a * x) = (λ x : γ, a * (x * b)), from
-  funext (λ c : γ,
-    calc ((λ x : γ, x * b) ∘ (λ x : γ, a * x)) c = a * c * b : by simp
-      ... = (λ x : γ, a * (c * b)) c : by rw mul_assoc; simp),
-calc a *l s *r b   = image ((λ x : γ, x * b) ∘ (λ x : γ, a * x)) s :
-    by rw [right_coset, left_coset, ←image_comp]
-  ... = a *l (s *r b) :
-    by rw [right_coset, left_coset, ←image_comp, h]
+@[simp] lemma left_coset_assoc (s : set γ) (a b : γ) : a *l (b *l s) = (a * b) *l s :=
+by simp [left_coset, right_coset, (image_comp _ _ _).symm, function.comp, mul_assoc]
+
+@[simp] lemma right_coset_assoc (s : set γ) (a b : γ) : s *r a *r b = s *r (a * b) :=
+by simp [left_coset, right_coset, (image_comp _ _ _).symm, function.comp, mul_assoc]
+
+lemma left_coset_right_coset (s : set γ) (a b : γ) : a *l s *r b = a *l (s *r b) :=
+by simp [left_coset, right_coset, (image_comp _ _ _).symm, function.comp, mul_assoc]
 
 end coset_semigroup
 
-section coset_subgroup
-open is_submonoid
-open is_subgroup
-variables [group γ] (s : set γ) [is_subgroup s]
+section coset_monoid
+variables [monoid γ] (s : set γ)
 
-lemma left_coset_mem_left_coset {a : γ} (ha : a ∈ s) : a *l s = s :=
-begin
-  simp [left_coset, image, set_eq_def, mem_set_of_eq],
-  intro b,
-  split,
-  { intro h,
-    cases h with x hx,
-    cases hx with hxl hxr,
-    rw [←hxr],
-    exact mul_mem ha hxl },
-  { intro h,
-    existsi a⁻¹ * b,
-    split,
-    have : a⁻¹ ∈ s, from inv_mem ha,
-    exact mul_mem this h,
-    simp }
-end
+@[simp] lemma one_left_coset : 1 *l s = s :=
+set.ext $ by simp [left_coset]
 
-lemma right_coset_mem_right_coset {a : γ} (ha : a ∈ s) : s *r a = s :=
-begin
-  simp [right_coset, image, set_eq_def, mem_set_of_eq],
-  intro b,
-  split,
-  { intro h,
-    cases h with x hx,
-    cases hx with hxl hxr,
-    rw [←hxr],
-    exact mul_mem hxl ha },
-  { intro h,
-    existsi b * a⁻¹,
-    split,
-    have : a⁻¹ ∈ s, from inv_mem ha,
-    exact mul_mem h this,
-    simp }
-end
-
-lemma one_left_coset : 1 *l s = s := left_coset_mem_left_coset s (one_mem s)
-
-lemma one_right_coset : s *r 1 = s := right_coset_mem_right_coset s (one_mem s)
+@[simp] lemma right_coset_one : s *r 1 = s :=
+set.ext $ by simp [right_coset]
+
+end coset_monoid
+
+section coset_submonoid
+open is_submonoid
+variables [monoid γ] (s : set γ) [is_submonoid s]
 
 lemma mem_own_left_coset (a : γ) : a ∈ a *l s :=
-by conv in a {rw ←mul_one a}; exact (mem_left_coset a (one_mem s))
+suffices a * 1 ∈ a *l s, by simpa,
+mem_left_coset a (one_mem s)
 
 lemma mem_own_right_coset (a : γ) : a ∈ s *r a :=
-by conv in a {rw ←one_mul a}; exact (mem_right_coset a (one_mem s))
+suffices 1 * a ∈ s *r a, by simpa,
+mem_right_coset a (one_mem s)
 
 lemma mem_left_coset_left_coset {a : γ} (ha : a *l s = s) : a ∈ s :=
 by rw [←ha]; exact mem_own_left_coset s a
@@ -125,42 +74,42 @@ by rw [←ha]; exact mem_own_left_coset s a
 lemma mem_right_coset_right_coset {a : γ} (ha : s *r a = s) : a ∈ s :=
 by rw [←ha]; exact mem_own_right_coset s a
 
-lemma mem_mem_left_coset {a x : γ} (hx : x ∈ s) (hax : a * x ∈ s) : a ∈ s :=
-begin
-  apply mem_left_coset_left_coset s,
-  conv in s { rw ←left_coset_mem_left_coset s hx },
-  rw [left_coset_assoc, left_coset_mem_left_coset s hax]
-end
-
-theorem normal_of_eq_cosets [normal_subgroup s] : ∀ g, g *l s = s *r g :=
-begin
-  intros g,
-  apply eq_of_subset_of_subset,
-  all_goals { simp [left_coset, right_coset, image], intros a n ha hn },
-  existsi g * n * g⁻¹, tactic.swap, existsi g⁻¹ * n * (g⁻¹)⁻¹,
-  all_goals {split, apply normal_subgroup.normal, assumption },
-  { rw inv_inv g, rw [←mul_assoc, ←mul_assoc], simp, assumption },
-  { simp, assumption }
-end
-
-theorem eq_cosets_of_normal (h : ∀ g, g *l s = s *r g) : normal_subgroup s:=
-begin
-  split,
-  intros n hn g,
-  have hl : g * n ∈ g *l s, from mem_left_coset g hn,
-  rw h at hl,
-  simp [right_coset] at hl,
-  cases hl with x hx,
-  cases hx with hxl hxr,
-  have : g * n * g⁻¹ = x, { calc
-    g * n * g⁻¹ = x * g * g⁻¹ : by rw ←hxr
-    ...         = x           : by simp
-  },
-  rw this,
-  exact hxl
-end
+end coset_submonoid
+
+section coset_group
+variables [group γ] {s : set γ} {x : γ}
+
+lemma mem_left_coset_iff (a : γ) : x ∈ a *l s ↔ a⁻¹ * x ∈ s :=
+iff.intro
+  (assume ⟨b, hb, eq⟩, by simp [eq.symm, hb])
+  (assume h, ⟨a⁻¹ * x, h, by simp⟩)
+
+lemma mem_right_coset_iff (a : γ) : x ∈ s *r a ↔ x * a⁻¹ ∈ s :=
+iff.intro
+  (assume ⟨b, hb, eq⟩, by simp [eq.symm, hb])
+  (assume h, ⟨x * a⁻¹, h, by simp⟩)
+
+end coset_group
+
+section coset_subgroup
+open is_submonoid
+open is_subgroup
+variables [group γ] (s : set γ) [is_subgroup s]
+
+lemma left_coset_mem_left_coset {a : γ} (ha : a ∈ s) : a *l s = s :=
+set.ext $ by simp [mem_left_coset_iff, mul_mem_cancel_right s (inv_mem ha)]
+
+lemma right_coset_mem_right_coset {a : γ} (ha : a ∈ s) : s *r a = s :=
+set.ext $ assume b, by simp [mem_right_coset_iff, mul_mem_cancel_left s (inv_mem ha)]
+
+theorem normal_of_eq_cosets [normal_subgroup s] (g : γ) : g *l s = s *r g :=
+set.ext $ assume a, by simp [mem_left_coset_iff, mem_right_coset_iff]; rw [mem_norm_comm_iff]
+
+theorem eq_cosets_of_normal (h : ∀ g, g *l s = s *r g) : normal_subgroup s :=
+⟨assume a ha g, show g * a * g⁻¹ ∈ s,
+  by rw [← mem_right_coset_iff, ← h]; exact mem_left_coset g ha⟩
 
 theorem normal_iff_eq_cosets : normal_subgroup s ↔ ∀ g, g *l s = s *r g :=
 ⟨@normal_of_eq_cosets _ _ s _, eq_cosets_of_normal s⟩
 
-end coset_subgroup
\ No newline at end of file
+end coset_subgroup
diff --git a/group_theory/subgroup.lean b/group_theory/subgroup.lean
index e0157bec20143..4e4f6a09db0eb 100644
--- a/group_theory/subgroup.lean
+++ b/group_theory/subgroup.lean
@@ -274,33 +274,25 @@ end
 
 end order_of
 
-class normal_subgroup [group α] (S : set α) extends is_subgroup S : Prop :=
-(normal : ∀ n ∈ S, ∀ g : α, g * n * g⁻¹ ∈ S)
+class normal_subgroup [group α] (s : set α) extends is_subgroup s : Prop :=
+(normal : ∀ n ∈ s, ∀ g : α, g * n * g⁻¹ ∈ s)
 
 namespace is_subgroup
 variable [group α]
 
 -- Normal subgroup properties
-lemma mem_norm_comm {a b : α} {S : set α} [normal_subgroup S] (hab : a * b ∈ S) : b * a ∈ S :=
-have h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ S, from normal_subgroup.normal (a * b) hab a⁻¹,
+lemma mem_norm_comm {a b : α} {s : set α} [normal_subgroup s] (hab : a * b ∈ s) : b * a ∈ s :=
+have h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ s, from normal_subgroup.normal (a * b) hab a⁻¹,
 by simp at h; exact h
 
+lemma mem_norm_comm_iff {a b : α} {s : set α} [normal_subgroup s] : a * b ∈ s ↔ b * a ∈ s :=
+iff.intro mem_norm_comm mem_norm_comm
+
 -- Examples of subgroups
 def trivial (α : Type*) [group α] : set α := {1}
 
-lemma eq_one_of_trivial_mem [group α] {g : α} (p : g ∈ trivial α) : g = 1 :=
-begin
-  cases p,
-  assumption,
-  cases p,
-end
-
-lemma trivial_mem_of_eq_one [group α] {g : α} (p : g = 1) : g ∈ trivial α :=
-begin
-  rw p,
-  unfold trivial,
-  simp,
-end
+@[simp] lemma mem_trivial [group α] {g : α} : g ∈ trivial α ↔ g = 1 :=
+by simp [trivial]
 
 instance trivial_normal : normal_subgroup (trivial α) :=
 by refine {..}; simp [trivial] {contextual := tt}
@@ -310,31 +302,22 @@ by refine {..}; simp
 
 def center (α : Type*) [group α] : set α := {z | ∀ g, g * z = z * g}
 
+lemma mem_center {a : α} : a ∈ center α ↔ (∀g, g * a = a * g) :=
+iff.refl _
+
 instance center_normal : normal_subgroup (center α) := {
   one_mem := by simp [center],
-  mul_mem :=
-    begin
-      intros a b ha hb g,
-      rw [center, mem_set_of_eq] at *,
-      rw [←mul_assoc, ha g, mul_assoc, hb g, ←mul_assoc]
-    end,
-  inv_mem :=
-    begin
-      assume a ha g,
-      simp [center] at *,
-      calc
-        g * a⁻¹ = a⁻¹ * (g * a) * a⁻¹     : by simp [ha g]
-        ...     = a⁻¹ * g                 : by rw [←mul_assoc, mul_assoc]; simp
-    end,
-  normal :=
-    begin
-      simp [center, mem_set_of_eq],
-      intros n ha g h,
-      calc
-        h * (g * n * g⁻¹) = h * n               : by simp [ha g, mul_assoc]
-        ...               = g * g⁻¹ * n * h     : by rw ha h; simp
-        ...               = g * n * g⁻¹ * h     : by rw [mul_assoc g, ha g⁻¹, ←mul_assoc]
-    end
+  mul_mem := assume a b ha hb g,
+    by rw [←mul_assoc, mem_center.2 ha g, mul_assoc, mem_center.2 hb g, ←mul_assoc],
+  inv_mem := assume a ha g,
+    calc
+      g * a⁻¹ = a⁻¹ * (g * a) * a⁻¹ : by simp [ha g]
+      ...     = a⁻¹ * g             : by rw [←mul_assoc, mul_assoc]; simp,
+  normal := assume n ha g h,
+    calc
+      h * (g * n * g⁻¹) = h * n           : by simp [ha g, mul_assoc]
+      ...               = g * g⁻¹ * n * h : by rw ha h; simp
+      ...               = g * n * g⁻¹ * h : by rw [mul_assoc g, ha g⁻¹, ←mul_assoc]
 }
 
 end is_subgroup
@@ -345,91 +328,68 @@ open is_submonoid
 open is_subgroup
 variables [group α] [group β]
 
-def kernel (f : α → β) [is_group_hom f] : set α := preimage f (trivial β)
+def ker (f : α → β) [is_group_hom f] : set α := preimage f (trivial β)
 
-lemma mem_ker_one (f : α → β) [is_group_hom f] {x : α} (h : x ∈ kernel f) : f x = 1 := eq_one_of_trivial_mem h
+lemma mem_ker (f : α → β) [is_group_hom f] {x : α} : x ∈ ker f ↔ f x = 1 :=
+mem_trivial
 
-lemma one_ker_inv (f : α → β) [is_group_hom f] {a b : α} (h : f (a * b⁻¹) = 1) : f a = f b := by rw ←inv_inv (f b); rw [mul f, inv f] at h; exact eq_inv_of_mul_eq_one h
+lemma one_ker_inv (f : α → β) [is_group_hom f] {a b : α} (h : f (a * b⁻¹) = 1) : f a = f b :=
+begin
+  rw [mul f, inv f] at h,
+  rw [←inv_inv (f b), eq_inv_of_mul_eq_one h]
+end
 
 lemma inv_ker_one (f : α → β) [is_group_hom f] {a b : α} (h : f a = f b) : f (a * b⁻¹) = 1 :=
-have f a * (f b)⁻¹ = 1, by rw h; apply mul_right_inv,
-by rw [←inv f, ←mul f] at this; exact this
-
-lemma ker_inv (f : α → β) [is_group_hom f] {a b : α} (h : a * b⁻¹ ∈ kernel f) : f a = f b := one_ker_inv f $ mem_ker_one f h
-
-lemma inv_ker (f : α → β) [is_group_hom f] {a b : α} (h : f a = f b) : a * b⁻¹ ∈ kernel f := by simp [kernel,mem_set_of_eq]; exact trivial_mem_of_eq_one (inv_ker_one f h)
+have f a * (f b)⁻¹ = 1, by rw [h, mul_right_inv],
+by rwa [←inv f, ←mul f] at this
 
 lemma one_iff_ker_inv (f : α → β) [is_group_hom f] (a b : α) : f a = f b ↔ f (a * b⁻¹) = 1 :=
 ⟨inv_ker_one f, one_ker_inv f⟩
 
-lemma inv_iff_ker (f : α → β) [w : is_group_hom f] (a b : α) : f a = f b ↔ a * b⁻¹ ∈ kernel f :=
-/- TODO: I don't understand why I can't just write
-    ⟨inv_ker f, ker_inv f⟩
-  here. This still gives typeclass errors; it can't find `w`. -/
-⟨@inv_ker _ _ _ _ f w _ _, @ker_inv _ _ _ _ f w _ _⟩
+lemma inv_iff_ker (f : α → β) [w : is_group_hom f] (a b : α) : f a = f b ↔ a * b⁻¹ ∈ ker f :=
+by rw [mem_ker]; exact one_iff_ker_inv _ _ _
 
-instance image_subgroup (f : α → β) [is_group_hom f] (S : set α) [is_subgroup S] : is_subgroup (f '' S) :=
+instance image_subgroup (f : α → β) [is_group_hom f] (s : set α) [is_subgroup s] :
+  is_subgroup (f '' s) :=
 { mul_mem := assume a₁ a₂ ⟨b₁, hb₁, eq₁⟩ ⟨b₂, hb₂, eq₂⟩,
              ⟨b₁ * b₂, mul_mem hb₁ hb₂, by simp [eq₁, eq₂, mul f]⟩,
-  one_mem := ⟨1, one_mem S, one f⟩,
+  one_mem := ⟨1, one_mem s, one f⟩,
   inv_mem := assume a ⟨b, hb, eq⟩, ⟨b⁻¹, inv_mem hb, by rw inv f; simp *⟩ }
 
 local attribute [simp] one_mem inv_mem mul_mem normal_subgroup.normal
 
-private lemma inv' (f : α → β) [is_group_hom f] (a : α) : (f a)⁻¹ = f a⁻¹ := by rw ←inv f
+instance preimage (f : α → β) [is_group_hom f] (s : set β) [is_subgroup s] :
+  is_subgroup (f ⁻¹' s) :=
+by refine {..}; simp [mul f, one f, inv f, @inv_mem β _ _ s] {contextual:=tt}
 
-instance preimage (f : α → β) [is_group_hom f] (S : set β) [is_subgroup S] : is_subgroup (f ⁻¹' S) :=
-begin
- refine {..};
- simp [mul f, one f, inv' f] {contextual:=tt},
- intros g w,
- rw inv f,
- exact (inv_mem_iff S).2 w,
-end
+instance preimage_normal (f : α → β) [is_group_hom f] (s : set β) [normal_subgroup s] :
+  normal_subgroup (f ⁻¹' s) :=
+{ normal := by simp [mul f, inv f] {contextual:=tt} }
 
-instance preimage_normal (f : α → β) [is_group_hom f] (S : set β) [normal_subgroup S] :
-  normal_subgroup (f ⁻¹' S) :=
-begin
- refine {..},
- { simp [one f] },
- { simp [mul f] {contextual:=tt} },
- { simp [inv' f],
-   intros g w,
-   rw inv f,
-   exact (inv_mem_iff S).2 w },
- { simp [mul f, inv f] {contextual:=tt} }
-end
-
-instance kernel_normal (f : α → β) [is_group_hom f] : normal_subgroup (kernel f) :=
+instance normal_subgroup_ker (f : α → β) [is_group_hom f] : normal_subgroup (ker f) :=
 is_group_hom.preimage_normal f (trivial β)
 
-lemma inj_of_trivial_kernel (f : α → β) [is_group_hom f] (h : kernel f = trivial α) :
+lemma inj_of_trivial_ker (f : α → β) [is_group_hom f] (h : ker f = trivial α) :
   function.injective f :=
 begin
   intros a₁ a₂ hfa,
-  simp [set_eq_def, kernel, is_subgroup.trivial] at h,
+  simp [set_eq_def, ker, is_subgroup.trivial] at h,
   have ha : a₁ * a₂⁻¹ = 1, by rw ←h; exact inv_ker_one f hfa,
   rw [eq_inv_of_mul_eq_one ha, inv_inv a₂]
 end
 
-lemma trivial_kernel_of_inj (f : α → β) [w : is_group_hom f] (h : function.injective f) :
-  kernel f = trivial α :=
-begin
-  apply set.ext,
-  intro,
-  split,
-  { assume hx,
-    have hi : f x = f 1,
-    { simp [one f]; rw (@mem_ker_one _ _ _ _ f w _ hx) }, -- TODO not finding the typeclass
-    apply trivial_mem_of_eq_one,
-    simp [h hi, one f] },
-  { assume hx, rw eq_one_of_trivial_mem hx, simp }
-end
+lemma trivial_ker_of_inj (f : α → β) [w : is_group_hom f] (h : function.injective f) :
+  ker f = trivial α :=
+set.ext $ assume x, iff.intro
+  (assume hx,
+    suffices f x = f 1, by simpa using h this,
+    by simp [one f]; rwa [mem_ker] at hx)
+  (by simp [mem_ker, is_group_hom.one f] {contextual := tt})
 
-lemma inj_iff_trivial_kernel (f : α → β) [w : is_group_hom f] :
-  function.injective f ↔ kernel f = trivial α :=
+lemma inj_iff_trivial_ker (f : α → β) [w : is_group_hom f] :
+  function.injective f ↔ ker f = trivial α :=
 -- TODO: still not finding the typeclass. ⟨trivial_kernel_of_inj f, inj_of_trivial_kernel f⟩
-⟨@trivial_kernel_of_inj _ _ _ _ f w, @inj_of_trivial_kernel _ _ _ _ f w⟩
+⟨@trivial_ker_of_inj _ _ _ _ f w, @inj_of_trivial_ker _ _ _ _ f w⟩
 
 end is_group_hom