diff --git a/library/theories/finite_group_theory/group_theory.md b/library/theories/finite_group_theory/finite_group_theory.md
similarity index 93%
rename from library/theories/finite_group_theory/group_theory.md
rename to library/theories/finite_group_theory/finite_group_theory.md
index bfa271c71..85cf6b723 100644
--- a/library/theories/finite_group_theory/group_theory.md
+++ b/library/theories/finite_group_theory/finite_group_theory.md
@@ -1,5 +1,5 @@
-theories.group_theory
-=====================
+theories.finite_group_theory
+============================
 
 Group theory (especially finite group theory).
 
diff --git a/library/theories/group_theory/basic.lean b/library/theories/group_theory/basic.lean
new file mode 100644
index 000000000..b1bfe3d16
--- /dev/null
+++ b/library/theories/group_theory/basic.lean
@@ -0,0 +1,973 @@
+/-
+Copyright (c) 2016 Andrew Zipperer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Zipperer, Jeremy Avigad
+
+Basic group theory: subgroups, homomorphisms on a set, homomorphic images, cosets,
+  normal cosets and the normalizer, the kernel of a homomorphism, the centralizer, etc.
+
+For notation a * S and S * a for cosets, open the namespace "coset_notation".
+For notation a^b and S^a, open the namespace "conj_notation".
+
+TODO: homomorphisms on sets should be refactored and moved to algebra.
+-/
+import data.set algebra.homomorphism theories.topology.basic theories.move
+open eq.ops set function
+
+namespace group_theory
+
+variables {A B C : Type}
+
+/- subgroups -/
+
+structure is_one_closed [class] [has_one A] (S : set A) : Prop :=
+(one_mem : one ∈ S)
+
+proposition one_mem [has_one A] {S : set A} [is_one_closed S] : 1 ∈ S :=
+is_one_closed.one_mem _ S
+
+structure is_mul_closed [class] [has_mul A] (S : set A) : Prop :=
+(mul_mem : ∀₀ a ∈ S, ∀₀ b ∈ S, a * b ∈ S)
+
+proposition mul_mem [has_mul A] {S : set A} [is_mul_closed S] {a b : A} (aS : a ∈ S) (bS : b ∈ S) :
+  a * b ∈ S :=
+is_mul_closed.mul_mem _ S aS bS
+
+structure is_inv_closed [class] [has_inv A] (S : set A) : Prop :=
+(inv_mem : ∀₀ a ∈ S, a⁻¹ ∈ S)
+
+proposition inv_mem [has_inv A] {S : set A} [is_inv_closed S] {a : A} (aS : a ∈ S) : a⁻¹ ∈ S :=
+is_inv_closed.inv_mem _ S aS
+
+structure is_subgroup [class] [group A] (S : set A)
+  extends is_one_closed S, is_mul_closed S, is_inv_closed S : Prop
+
+section groupA
+  variable [group A]
+
+  proposition mem_of_inv_mem {a : A} {S : set A} [is_subgroup S] (H : a⁻¹ ∈ S) : a ∈ S :=
+  have (a⁻¹)⁻¹ ∈ S, from inv_mem H,
+  by rewrite inv_inv at this; apply this
+
+  proposition inv_mem_iff (a : A) (S : set A) [is_subgroup S] : a⁻¹ ∈ S ↔ a ∈ S :=
+  iff.intro mem_of_inv_mem inv_mem
+
+  proposition is_subgroup_univ [instance] : is_subgroup (@univ A) :=
+  ⦃ is_subgroup,
+    one_mem := trivial,
+    mul_mem := λ a au b bu, trivial,
+    inv_mem := λ a au, trivial ⦄
+
+  proposition is_subgroup_inter [instance] (G H : set A) [is_subgroup G] [is_subgroup H] :
+    is_subgroup (G ∩ H) :=
+  ⦃ is_subgroup,
+    one_mem := and.intro one_mem one_mem,
+    mul_mem := λ a ai b bi, and.intro (mul_mem (and.left ai) (and.left bi))
+                   (mul_mem (and.right ai) (and.right bi)),
+    inv_mem := λ a ai, and.intro (inv_mem (and.left ai)) (inv_mem (and.right ai)) ⦄
+end groupA
+
+
+/- homomorphisms on sets -/
+
+section has_mulABC
+  variables [has_mul A] [has_mul B] [has_mul C]
+
+  -- in group theory, we can use is_hom for is_mul_hom
+  abbreviation is_hom := @is_mul_hom
+
+  definition is_hom_on [class] (f : A → B) (S : set A) : Prop :=
+    ∀₀ a₁ ∈ S, ∀₀ a₂ ∈ S, f (a₁ * a₂) = f a₁ * f a₂
+
+  proposition hom_on_mul (f : A → B) {S : set A} [H : is_hom_on f S] {a₁ a₂ : A}
+      (a₁S : a₁ ∈ S) (a₂S : a₂ ∈ S) : f (a₁ * a₂) = (f a₁) * (f a₂) :=
+    H a₁S a₂S
+
+  proposition is_hom_on_of_is_hom (f : A → B) (S : set A) [H : is_hom f] : is_hom_on f S :=
+  forallb_of_forall₂ S S (hom_mul f)
+
+  proposition is_hom_of_is_hom_on_univ (f : A → B) [H : is_hom_on f univ] : is_hom f :=
+  is_mul_hom.mk (forall_of_forallb_univ₂ H)
+
+  proposition is_hom_on_univ_iff (f : A → B) : is_hom_on f univ ↔ is_hom f :=
+  iff.intro (λH, is_hom_of_is_hom_on_univ f) (λ H, is_hom_on_of_is_hom f univ)
+
+  proposition is_hom_on_of_subset (f : A → B) {S T : set A} (ssubt : S ⊆ T) [H : is_hom_on f T] :
+    is_hom_on f S :=
+  forallb_of_subset₂ ssubt ssubt H
+
+  proposition is_hom_on_id (S : set A) : is_hom_on id S :=
+  have H : is_hom (@id A), from is_mul_hom_id,
+  is_hom_on_of_is_hom id S
+
+  proposition is_hom_on_comp {S : set A} {T : set B} {g : B → C} {f : A → B}
+    (H₁ : is_hom_on f S) (H₂ : is_hom_on g T) (H₃ : maps_to f S T) : is_hom_on (g ∘ f) S :=
+  take a₁, assume a₁S, take a₂, assume a₂S,
+  have f a₁ ∈ T, from H₃ a₁S,
+  have f a₂ ∈ T, from H₃ a₂S,
+  show g (f (a₁ * a₂)) = g (f a₁) * g (f a₂), by rewrite [H₁ a₁S a₂S, H₂ `f a₁ ∈ T` `f a₂ ∈ T`]
+end has_mulABC
+
+section groupAB
+  variables [group A] [group B]
+
+  proposition hom_on_one (f : A → B) (G : set A) [is_subgroup G] [H : is_hom_on f G] : f 1 = 1 :=
+  have f 1 * f 1 = f 1 * 1, by rewrite [-H one_mem one_mem, *mul_one],
+  eq_of_mul_eq_mul_left' this
+
+  proposition hom_on_inv (f : A → B) {G : set A} [is_subgroup G] [H : is_hom_on f G]
+      {a : A} (aG : a ∈ G) :
+    f a⁻¹ = (f a)⁻¹ :=
+  have f a⁻¹ * f a = 1, by rewrite [-H (inv_mem aG) aG, mul.left_inv, hom_on_one f G],
+  eq_inv_of_mul_eq_one this
+
+  proposition is_subgroup_image [instance] (f : A → B) (G : set A)
+    [is_subgroup G] [is_hom_on f G] :
+  is_subgroup (f ' G) :=
+  ⦃ is_subgroup,
+    one_mem := mem_image one_mem (hom_on_one f G),
+    mul_mem := λ a afG b bfG,
+      obtain c (cG : c ∈ G)(Hc : f c = a), from afG,
+      obtain d (dG : d ∈ G)(Hd : f d = b), from bfG,
+      show a * b ∈ f ' G, from mem_image (mul_mem cG dG) (by rewrite [hom_on_mul f cG dG, Hc, Hd]),
+    inv_mem := λ a afG,
+      obtain c (cG : c ∈ G)(Hc : f c = a), from afG,
+      show a⁻¹ ∈ f ' G, from mem_image (inv_mem cG) (by rewrite [hom_on_inv f cG, Hc]) ⦄
+end groupAB
+
+
+/- cosets -/
+
+definition lcoset [has_mul A] (a : A) (N : set A) : set A := (mul a) 'N
+definition rcoset [has_mul A] (N : set A) (a : A) : set A := (mul^~ a) 'N
+
+-- overload multiplication
+namespace coset_notation
+  infix * := lcoset
+  infix * := rcoset
+end coset_notation
+
+open coset_notation
+
+section has_mulA
+  variable [has_mul A]
+
+  proposition mul_mem_lcoset {S : set A} {x : A} (a : A) (xS : x ∈ S) : a * x ∈ a * S :=
+  mem_image_of_mem (mul a) xS
+
+  proposition mul_mem_rcoset [has_mul A] {S : set A} {x : A} (xS : x ∈ S) (a : A) :
+    x * a ∈ S * a :=
+  mem_image_of_mem (mul^~ a) xS
+
+  definition lcoset_equiv (S : set A) (a b : A) : Prop := a * S = b * S
+
+  proposition equivalence_lcoset_equiv (S : set A) : equivalence (lcoset_equiv S) :=
+  mk_equivalence (lcoset_equiv S) (λ a, rfl) (λ a b, !eq.symm) (λ a b c, !eq.trans)
+
+  proposition lcoset_subset_lcoset {S T : set A} (a : A) (H : S ⊆ T) : a * S ⊆ a * T :=
+  image_subset _ H
+
+  proposition rcoset_subset_rcoset {S T : set A} (H : S ⊆ T) (a : A) : S * a ⊆ T * a :=
+  image_subset _ H
+
+  proposition image_lcoset_of_is_hom_on {B : Type} [has_mul B] {f : A → B} {S : set A} {a : A}
+      {G : set A} (SsubG : S ⊆ G) (aG : a ∈ G) [is_hom_on f G] :
+    f ' (a * S) = f a * f ' S :=
+  ext (take x, iff.intro
+    (assume fas : x ∈ f ' (a * S),
+      obtain t [s (sS : s ∈ S) (seq : a * s = t)] (teq : f t = x), from fas,
+      have x = f a * f s, by rewrite [-teq, -seq, hom_on_mul f aG (SsubG sS)],
+      show x ∈ f a * f ' S, by rewrite this; apply mul_mem_lcoset _ (mem_image_of_mem _ sS))
+    (assume fafs : x ∈ f a * f ' S,
+      obtain t [s (sS : s ∈ S) (seq : f s = t)] (teq : f a * t = x), from fafs,
+      have x = f (a * s), by rewrite [-teq, -seq, hom_on_mul f aG (SsubG sS)],
+      show x ∈ f ' (a * S), by rewrite this; exact mem_image_of_mem _ (mul_mem_lcoset _ sS)))
+
+  proposition image_rcoset_of_is_hom_on {B : Type} [has_mul B] {f : A → B} {S : set A} {a : A}
+    {G : set A} (SsubG : S ⊆ G) (aG : a ∈ G) [is_hom_on f G] :
+  f ' (S * a) = f ' S * f a :=
+  ext (take x, iff.intro
+    (assume fas : x ∈ f ' (S * a),
+      obtain t [s (sS : s ∈ S) (seq : s * a = t)] (teq : f t = x), from fas,
+      have x = f s * f a, by rewrite [-teq, -seq, hom_on_mul f (SsubG sS) aG],
+      show x ∈ f ' S * f a, by rewrite this; exact mul_mem_rcoset (mem_image_of_mem _ sS) _)
+    (assume fafs : x ∈ f ' S * f a,
+      obtain t [s (sS : s ∈ S) (seq : f s = t)] (teq : t * f a = x), from fafs,
+      have x = f (s * a), by rewrite [-teq, -seq, hom_on_mul f (SsubG sS) aG],
+      show x ∈ f ' (S * a), by rewrite this; exact mem_image_of_mem _ (mul_mem_rcoset sS _)))
+
+  proposition image_lcoset_of_is_hom {B : Type} [has_mul B] (f : A → B) (a : A) (S : set A)
+      [is_hom f] :
+    f ' (a * S) = f a * f ' S :=
+  have is_hom_on f univ, from is_hom_on_of_is_hom f univ,
+  image_lcoset_of_is_hom_on (subset_univ S) !mem_univ
+
+  proposition image_rcoset_of_is_hom {B : Type} [has_mul B] (f : A → B) (S : set A) (a : A)
+      [is_hom f] :
+    f ' (S * a) = f ' S * f a :=
+  have is_hom_on f univ, from is_hom_on_of_is_hom f univ,
+  image_rcoset_of_is_hom_on (subset_univ S) !mem_univ
+end has_mulA
+
+section semigroupA
+  variable [semigroup A]
+
+  proposition rcoset_rcoset (S : set A) (a b : A) : S * a * b = S * (a * b) :=
+  have H : (mul^~ b) ∘ (mul^~ a) = mul^~ (a * b), from funext (take x, !mul.assoc),
+  calc
+    S * a * b = ((mul^~ b) ∘ (mul^~ a)) 'S : image_comp
+          ... = S * (a * b)                : by rewrite [↑rcoset, H]
+
+  proposition lcoset_lcoset (S : set A) (a b : A) : a * (b * S)  = (a * b) * S :=
+  have H : (mul a) ∘ (mul b) = mul (a * b), from funext (take x, !mul.assoc⁻¹),
+  calc
+    a * (b * S) = ((mul a) ∘ (mul b)) 'S : image_comp
+            ... = (a * b) * S            : by rewrite [↑lcoset, H]
+
+  proposition lcoset_rcoset [semigroup A] (S : set A) (a b : A) : a * S * b = a * (S * b) :=
+  have H : (mul^~ b) ∘ (mul a) = (mul a) ∘ (mul^~ b), from funext (take x, !mul.assoc),
+  calc
+    a * S * b = ((mul^~ b) ∘ (mul a)) 'S : image_comp
+          ... = ((mul a) ∘ (mul^~ b)) 'S : H
+          ... = a * (S * b)              : image_comp
+end semigroupA
+
+section monoidA
+  variable [monoid A]
+
+  proposition one_lcoset (S : set A) : 1 * S = S :=
+  ext (take x, iff.intro
+    (suppose x ∈ 1 * S,
+      obtain s (sS : s ∈ S) (eqx : 1 * s = x), from this,
+      show x ∈ S, by rewrite [-eqx, one_mul]; apply sS)
+    (suppose x ∈ S,
+      have 1 * x ∈ 1 * S, from mem_image_of_mem (mul 1) this,
+      show x ∈ 1 * S, by rewrite one_mul at this; apply this))
+
+  proposition rcoset_one (S : set A) : S * 1 = S :=
+  ext (take x, iff.intro
+    (suppose x ∈ S * 1,
+      obtain s (sS : s ∈ S) (eqx : s * 1 = x), from this,
+      show x ∈ S, by rewrite [-eqx, mul_one]; apply sS)
+    (suppose x ∈ S,
+      have x * 1 ∈ S * 1, from mem_image_of_mem (mul^~ 1) this,
+      show x ∈ S * 1, by rewrite mul_one at this; apply this))
+end monoidA
+
+section groupA
+  variable [group A]
+
+  proposition lcoset_inv_lcoset (a : A) (S : set A) : a * (a⁻¹ * S) = S :=
+  by rewrite [lcoset_lcoset, mul.right_inv, one_lcoset]
+
+  proposition inv_lcoset_lcoset (a : A) (S : set A) : a⁻¹ * (a * S) = S :=
+  by rewrite [lcoset_lcoset, mul.left_inv, one_lcoset]
+
+  proposition rcoset_inv_rcoset (S : set A) (a : A) : (S * a⁻¹) * a = S :=
+  by rewrite [rcoset_rcoset, mul.left_inv, rcoset_one]
+
+  proposition rcoset_rcoset_inv (S : set A) (a : A) : (S * a) * a⁻¹ = S :=
+  by rewrite [rcoset_rcoset, mul.right_inv, rcoset_one]
+
+  proposition eq_of_lcoset_eq_lcoset {a : A} {S T : set A} (H : a * S = a * T) : S = T :=
+  by rewrite [-inv_lcoset_lcoset a S, -inv_lcoset_lcoset a T, H]
+
+  proposition eq_of_rcoset_eq_rcoset {a : A} {S T : set A} (H : S * a = T * a) : S = T :=
+  by rewrite [-rcoset_rcoset_inv S a, -rcoset_rcoset_inv T a, H]
+
+  proposition mem_of_mul_mem_lcoset {a b : A} {S : set A} (abaS : a * b ∈ a * S) : b ∈ S :=
+  have a⁻¹ * (a * b) ∈ a⁻¹ * (a * S), from mul_mem_lcoset _ abaS,
+  by rewrite [inv_mul_cancel_left at this, inv_lcoset_lcoset at this]; apply this
+
+  proposition mul_mem_lcoset_iff (a b : A) (S : set A) : a * b ∈ a * S ↔ b ∈ S :=
+  iff.intro !mem_of_mul_mem_lcoset !mul_mem_lcoset
+
+  proposition mem_of_mul_mem_rcoset {a b : A} {S : set A} (abSb : a * b ∈ S * b) : a ∈ S :=
+  have (a * b) * b⁻¹ ∈ (S * b) * b⁻¹, from mul_mem_rcoset abSb _,
+  by rewrite [mul_inv_cancel_right at this, rcoset_rcoset_inv at this]; apply this
+
+  proposition mul_mem_rcoset_iff (a b : A) (S : set A) : a * b ∈ S * b ↔ a ∈ S :=
+  iff.intro !mem_of_mul_mem_rcoset (λ H, mul_mem_rcoset H _)
+
+  proposition inv_mul_mem_of_mem_lcoset {a b : A} {S : set A} (abS : a ∈ b * S) : b⁻¹ * a ∈ S :=
+  have b⁻¹ * a ∈ b⁻¹ * (b * S), from mul_mem_lcoset b⁻¹ abS,
+  by rewrite inv_lcoset_lcoset at this; apply this
+
+  proposition mem_lcoset_of_inv_mul_mem {a b : A} {S : set A} (H : b⁻¹ * a ∈ S) : a ∈ b * S :=
+  have b * (b⁻¹ * a) ∈ b * S, from mul_mem_lcoset b H,
+  by rewrite mul_inv_cancel_left at this; apply this
+
+  proposition mem_lcoset_iff (a b : A) (S : set A) : a ∈ b * S ↔ b⁻¹ * a ∈ S :=
+  iff.intro inv_mul_mem_of_mem_lcoset mem_lcoset_of_inv_mul_mem
+
+  proposition mul_inv_mem_of_mem_rcoset {a b : A} {S : set A} (aSb : a ∈ S * b) : a * b⁻¹ ∈ S :=
+  have a * b⁻¹ ∈ (S * b) * b⁻¹, from mul_mem_rcoset aSb b⁻¹,
+  by rewrite rcoset_rcoset_inv at this; apply this
+
+  proposition mem_rcoset_of_mul_inv_mem {a b : A} {S : set A} (H : a * b⁻¹ ∈ S) : a ∈ S * b :=
+  have a * b⁻¹ * b ∈ S * b, from mul_mem_rcoset H b,
+  by rewrite inv_mul_cancel_right at this; apply this
+
+  proposition mem_rcoset_iff (a b : A) (S : set A) : a ∈ S * b ↔ a * b⁻¹ ∈ S :=
+  iff.intro mul_inv_mem_of_mem_rcoset mem_rcoset_of_mul_inv_mem
+
+  proposition lcoset_eq_iff_eq_inv_lcoset (a : A) (S T : set A) : (a * S = T) ↔ (S = a⁻¹ * T) :=
+  iff.intro (assume H, by rewrite [-H, inv_lcoset_lcoset])
+      (assume H, by rewrite [H, lcoset_inv_lcoset])
+
+  proposition rcoset_eq_iff_eq_rcoset_inv (a : A) (S T : set A) : (S * a = T) ↔ (S = T * a⁻¹) :=
+  iff.intro (assume H, by rewrite [-H, rcoset_rcoset_inv])
+      (assume H, by rewrite [H, rcoset_inv_rcoset])
+
+  proposition lcoset_inter (a : A) (S T : set A) [is_subgroup S] [is_subgroup T] :
+    a * (S ∩ T) = (a * S) ∩ (a * T) :=
+  eq_of_subset_of_subset
+    (image_inter_subset _ S T)
+    (take b, suppose b ∈ (a * S) ∩ (a * T),
+      obtain [s [smem (seq : a * s = b)]] [t [tmem (teq : a * t = b)]], from this,
+      have s = t, from eq_of_mul_eq_mul_left' (eq.trans seq (eq.symm teq)),
+      show b ∈ a * (S ∩ T),
+        begin
+          rewrite -seq,
+          apply mul_mem_lcoset,
+          apply and.intro smem,
+          rewrite this, apply tmem
+        end)
+
+  proposition inter_rcoset (a : A) (S T : set A) [is_subgroup S] [is_subgroup T] :
+    (S ∩ T) * a = (S * a) ∩ (T * a) :=
+  eq_of_subset_of_subset
+    (image_inter_subset _ S T)
+    (take b, suppose b ∈ (S * a) ∩ (T * a),
+      obtain [s [smem (seq : s * a = b)]] [t [tmem (teq : t * a = b)]], from this,
+      have s = t, from eq_of_mul_eq_mul_right' (eq.trans seq (eq.symm teq)),
+      show b ∈ (S ∩ T) * a,
+        begin
+          rewrite -seq,
+          apply mul_mem_rcoset,
+          apply and.intro smem,
+          rewrite this, apply tmem
+        end)
+end groupA
+
+section subgroupG
+  variables [group A] {G : set A} [is_subgroup G]
+
+  proposition lcoset_eq_self_of_mem {a : A} (aG : a ∈ G) : a * G = G :=
+  ext (take x, iff.intro
+    (assume xaG, obtain g [gG xeq], from xaG,
+      show x ∈ G, by rewrite -xeq; exact (mul_mem aG gG))
+    (assume xG, show x ∈ a * G, from mem_image
+      (show a⁻¹ * x ∈ G, from (mul_mem (inv_mem aG) xG)) !mul_inv_cancel_left))
+
+  proposition rcoset_eq_self_of_mem {a : A} (aG : a ∈ G) : G * a = G :=
+  ext (take x, iff.intro
+    (assume xGa, obtain g [gG xeq], from xGa,
+      show x ∈ G, by rewrite -xeq; exact (mul_mem gG aG))
+    (assume xG, show x ∈ G * a, from mem_image
+      (show x * a⁻¹ ∈ G, from (mul_mem xG (inv_mem aG))) !inv_mul_cancel_right))
+
+  proposition mem_lcoset_self (a : A) : a ∈ a * G :=
+  by rewrite [-mul_one a at {1}]; exact mul_mem_lcoset a one_mem
+
+  proposition mem_rcoset_self (a : A) : a ∈ G * a :=
+  by rewrite [-one_mul a at {1}]; exact mul_mem_rcoset one_mem a
+
+  proposition mem_of_lcoset_eq_self {a : A} (H : a * G = G) : a ∈ G :=
+  by rewrite [-H]; exact mem_lcoset_self a
+
+  proposition mem_of_rcoset_eq_self {a : A} (H : G * a = G) : a ∈ G :=
+  by rewrite [-H]; exact mem_rcoset_self a
+
+  variable (G)
+
+  proposition lcoset_eq_self_iff (a : A) : a * G = G ↔ a ∈ G :=
+  iff.intro mem_of_lcoset_eq_self lcoset_eq_self_of_mem
+
+  proposition rcoset_eq_self_iff (a : A) : G * a = G ↔ a ∈ G :=
+  iff.intro mem_of_rcoset_eq_self rcoset_eq_self_of_mem
+
+  variable {G}
+
+  proposition lcoset_eq_lcoset {a b : A} (H : b⁻¹ * a ∈ G) : a * G = b * G :=
+  have b⁻¹ * (a * G) = b⁻¹ * (b * G),
+    by rewrite [inv_lcoset_lcoset, lcoset_lcoset, lcoset_eq_self_of_mem H],
+  eq_of_lcoset_eq_lcoset this
+
+  proposition inv_mul_mem_of_lcoset_eq_lcoset {a b : A} (H : a * G = b * G) : b⁻¹ * a ∈ G :=
+  mem_of_lcoset_eq_self (by rewrite [-lcoset_lcoset, H, inv_lcoset_lcoset])
+
+  proposition lcoset_eq_lcoset_iff (a b : A) : a * G = b * G ↔ b⁻¹ * a ∈ G :=
+  iff.intro inv_mul_mem_of_lcoset_eq_lcoset lcoset_eq_lcoset
+
+  proposition rcoset_eq_rcoset {a b : A} (H : a * b⁻¹ ∈ G) : G * a = G * b :=
+  have G * a * b⁻¹ = G * b * b⁻¹,
+    by rewrite [rcoset_rcoset_inv, rcoset_rcoset, rcoset_eq_self_of_mem H],
+  eq_of_rcoset_eq_rcoset this
+
+  proposition mul_inv_mem_of_rcoset_eq_rcoset {a b : A} (H : G * a = G * b) : a * b⁻¹ ∈ G :=
+  mem_of_rcoset_eq_self (by rewrite [-rcoset_rcoset, H, rcoset_rcoset_inv])
+
+  proposition rcoset_eq_rcoset_iff (a b : A) : G * a = G * b ↔ a * b⁻¹ ∈ G :=
+  iff.intro mul_inv_mem_of_rcoset_eq_rcoset rcoset_eq_rcoset
+end subgroupG
+
+
+/- normal cosets and the normalizer -/
+
+section has_mulA
+  variable [has_mul A]
+
+  abbreviation normalizes [reducible] (a : A) (S : set A) : Prop := a * S = S * a
+
+  definition is_normal [class] (S : set A) : Prop := ∀ a, normalizes a S
+
+  definition normalizer (S : set A) : set A := { a : A | normalizes a S }
+
+  definition is_normal_in [class] (S T : set A) : Prop := T ⊆ normalizer S
+
+  abbreviation normalizer_in [reducible] (S T : set A) : set A := T ∩ normalizer S
+
+  proposition lcoset_eq_rcoset (a : A) (S : set A) [H : is_normal S] : a * S = S * a := H a
+
+  proposition subset_normalizer (S T : set A) [H : is_normal_in T S] : S ⊆ normalizer T := H
+
+  proposition lcoset_eq_rcoset_of_mem {a : A} (S : set A) {T : set A} [H : is_normal_in S T]
+      (amemT : a ∈ T) :
+    a * S = S * a := H amemT
+
+  proposition is_normal_in_of_is_normal (S T : set A) [H : is_normal S] : is_normal_in S T :=
+  forallb_of_forall T H
+
+  proposition is_normal_of_is_normal_in_univ {S : set A} (H : is_normal_in S univ) :
+    is_normal S :=
+  forall_of_forallb_univ H
+
+  proposition is_normal_in_univ_iff_is_normal (S : set A) : is_normal_in S univ ↔ is_normal S :=
+  forallb_univ_iff_forall _
+
+   proposition is_normal_in_of_subset {S T U : set A} (H : T ⊆ U) (H' : is_normal_in S U) :
+    is_normal_in S T :=
+  forallb_of_subset H H'
+
+  proposition normalizes_of_mem_normalizer {a : A} {S : set A} (H : a ∈ normalizer S) :
+    normalizes a S := H
+
+  proposition mem_normalizer_iff_normalizes (a : A) (S : set A) :
+    a ∈ normalizer S ↔ normalizes a S := iff.refl _
+
+  proposition is_normal_in_normalizer [instance] (S : set A) : is_normal_in S (normalizer S) :=
+  subset.refl (normalizer S)
+end has_mulA
+
+section groupA
+  variable [group A]
+
+  proposition is_normal_in_of_forall_subset {S G : set A} [is_subgroup G]
+    (H : ∀₀ x ∈ G, x * S ⊆ S * x) :
+  is_normal_in S G :=
+  take x, assume xG,
+  show x * S = S * x, from eq_of_subset_of_subset (H xG)
+    (have x * (x⁻¹ * S) * x ⊆ x * (S * x⁻¹) * x,
+      from rcoset_subset_rcoset (lcoset_subset_lcoset x (H (inv_mem xG))) x,
+      show S * x ⊆ x * S,
+        begin
+         rewrite [lcoset_inv_lcoset at this, lcoset_rcoset at this, rcoset_inv_rcoset at this],
+         exact this
+       end)
+
+  proposition is_normal_of_forall_subset {S : set A} (H : ∀ x, x * S ⊆ S * x) : is_normal S :=
+  begin
+    rewrite [-is_normal_in_univ_iff_is_normal],
+    apply is_normal_in_of_forall_subset,
+    intro x xuniv, exact H x
+  end
+
+  proposition subset_normalizer_self (G : set A) [is_subgroup G] : G ⊆ normalizer G :=
+  take a, assume aG, show a * G = G * a,
+    by rewrite [lcoset_eq_self_of_mem aG, rcoset_eq_self_of_mem aG]
+end groupA
+
+section normalG
+  variables [group A] (G : set A) [is_normal G]
+
+  proposition lcoset_equiv_mul {a₁ a₂ b₁ b₂ : A}
+    (H₁ : lcoset_equiv G a₁ a₂) (H₂ : lcoset_equiv G b₁ b₂) : lcoset_equiv G (a₁ * b₁) (a₂ * b₂) :=
+  begin
+    unfold lcoset_equiv at *,
+    rewrite [-lcoset_lcoset, H₂, lcoset_eq_rcoset, -lcoset_rcoset, H₁, lcoset_rcoset,
+             -lcoset_eq_rcoset, lcoset_lcoset]
+  end
+
+  proposition lcoset_equiv_inv {a₁ a₂ : A} (H : lcoset_equiv G a₁ a₂) : lcoset_equiv G a₁⁻¹ a₂⁻¹ :=
+  begin
+    unfold lcoset_equiv at *,
+    have a₁⁻¹ * G = a₂⁻¹ * (a₂ * G) * a₁⁻¹, by rewrite [inv_lcoset_lcoset, lcoset_eq_rcoset],
+    rewrite [this, -H, lcoset_rcoset, lcoset_eq_rcoset, rcoset_rcoset_inv]
+  end
+end normalG
+
+
+/- the normalizer is a subgroup -/
+
+section semigroupA
+  variable [semigroup A]
+
+  proposition mul_mem_normalizer {S : set A} {a b : A}
+    (Ha : a ∈ normalizer S) (Hb : b ∈ normalizer S) : a * b ∈ normalizer S :=
+  show a * b * S = S * (a * b),
+    by rewrite [-lcoset_lcoset, normalizes_of_mem_normalizer Hb, -lcoset_rcoset,
+                normalizes_of_mem_normalizer Ha, rcoset_rcoset]
+end semigroupA
+
+section monoidA
+  variable [monoid A]
+
+  proposition one_mem_normalizer (S : set A) : 1 ∈ normalizer S :=
+  by rewrite [↑normalizer, mem_set_of_iff, one_lcoset, rcoset_one]
+end monoidA
+
+section groupA
+  variable [group A]
+
+  proposition inv_mem_normalizer {S : set A} {a : A} (H : a ∈ normalizer S) : a⁻¹ ∈ normalizer S :=
+  have a⁻¹ * S = S * a⁻¹,
+  begin
+    apply iff.mp (rcoset_eq_iff_eq_rcoset_inv _ _ _),
+    rewrite [lcoset_rcoset, -normalizes_of_mem_normalizer H, inv_lcoset_lcoset]
+  end,
+  by rewrite [↑normalizer, mem_set_of_iff, this]
+
+  proposition is_subgroup_normalizer [instance] (S : set A) : is_subgroup (normalizer S) :=
+  ⦃ is_subgroup,
+    one_mem := one_mem_normalizer S,
+    mul_mem := λ a Ha b Hb, mul_mem_normalizer Ha Hb,
+    inv_mem := λ a H, inv_mem_normalizer H⦄
+end groupA
+
+section subgroupG
+  variables [group A] {G : set A} [is_subgroup G]
+
+  proposition normalizes_image_of_is_hom_on [group B] {a : A} (aG : a ∈ G) {S : set A}
+      (SsubG : S ⊆ G) (H : normalizes a S) (f : A → B) [is_hom_on f G] :
+    normalizes (f a) (f ' S) :=
+  by rewrite [-image_lcoset_of_is_hom_on SsubG aG, -image_rcoset_of_is_hom_on SsubG aG,
+              ↑normalizes at H, H]
+
+  proposition is_normal_in_image_image [group B] {S T : set A} (SsubT : S ⊆ T)
+      [H : is_normal_in S T] (f : A → B) [is_subgroup T] [is_hom_on f T] :
+    is_normal_in (f ' S) (f ' T) :=
+  take a, assume afT,
+  obtain b [bT (beq : f b = a)], from afT,
+  show normalizes a (f ' S),
+    begin rewrite -beq, apply (normalizes_image_of_is_hom_on bT SsubT (H bT)) end
+
+  proposition normalizes_image_of_is_hom [group B] {a : A} {S : set A}
+      (H : normalizes a S) (f : A → B) [is_hom f] :
+    normalizes (f a) (f ' S) :=
+  by rewrite [-image_lcoset_of_is_hom f a S, -image_rcoset_of_is_hom f S a,
+              ↑normalizes at H, H]
+
+  proposition is_normal_in_image_image_univ [group B] {S : set A}
+      [H : is_normal S] (f : A → B) [is_hom f] :
+    is_normal_in (f ' S) (f ' univ) :=
+  take a, assume afT,
+  obtain b [buniv (beq : f b = a)], from afT,
+  show normalizes a (f ' S),
+    begin rewrite -beq, apply (normalizes_image_of_is_hom (H b) f) end
+end subgroupG
+
+
+/- conjugation -/
+
+definition conj [reducible] [group A] (a b : A) : A := b⁻¹ * a * b
+
+definition set_conj [reducible] [group A] (S : set A)(a : A) : set A := a⁻¹ * S * a
+-- conj^~ a ' S
+
+namespace conj_notation
+  infix `^` := conj
+  infix `^` := set_conj
+end conj_notation
+
+open conj_notation
+
+section groupA
+  variables [group A]
+
+  proposition set_conj_eq_image_conj (S : set A) (a : A) : S^a = conj^~ a 'S :=
+  eq.symm !image_comp
+
+  proposition set_conj_eq_self_of_normalizes {S : set A} {a : A} (H : normalizes a S) : S^a = S :=
+  by rewrite [lcoset_rcoset, ↑normalizes at H, -H, inv_lcoset_lcoset]
+
+  proposition normalizes_of_set_conj_eq_self {S : set A} {a : A} (H : S^a = S) : normalizes a S :=
+  by rewrite [-H at {1}, ↑set_conj, lcoset_rcoset, lcoset_inv_lcoset]
+
+  proposition set_conj_eq_self_iff_normalizes (S : set A) (a : A) : S^a = S ↔ normalizes a S :=
+  iff.intro normalizes_of_set_conj_eq_self set_conj_eq_self_of_normalizes
+
+  proposition set_conj_eq_self_of_mem_normalizer {S : set A} {a : A} (H : a ∈ normalizer S) :
+    S^a = S := set_conj_eq_self_of_normalizes H
+
+  proposition mem_normalizer_of_set_conj_eq_self {S : set A} {a : A} (H : S^a = S) :
+    a ∈ normalizer S := normalizes_of_set_conj_eq_self H
+
+  proposition set_conj_eq_self_iff_mem_normalizer (S : set A) (a : A) :
+    S^a = S ↔ a ∈ normalizer S :=
+  iff.intro mem_normalizer_of_set_conj_eq_self set_conj_eq_self_of_mem_normalizer
+
+  proposition conj_one (a : A) : a ^ (1 : A) = a :=
+  by rewrite [↑conj, one_inv, one_mul, mul_one]
+
+  proposition conj_conj (a b c : A) : (a^b)^c = a^(b * c) :=
+  by rewrite [↑conj, mul_inv, *mul.assoc]
+
+  proposition conj_inv (a b : A) : (a^b)⁻¹ = (a⁻¹)^b :=
+  by rewrite[mul_inv, mul_inv, inv_inv, mul.assoc]
+
+  proposition mul_conj (a b c : A) : (a * b)^c = a^c * b^c :=
+  by rewrite[↑conj, *mul.assoc, mul_inv_cancel_left]
+end groupA
+
+
+/- the kernel -/
+
+definition ker [has_one B] (f : A → B) : set A := { x | f x = 1 }
+
+section hasoneB
+  variable [has_one B]
+
+  proposition eq_one_of_mem_ker {f : A → B} {a : A} (H : a ∈ ker f) : f a = 1 := H
+
+  proposition mem_ker_iff (f : A → B) (a : A) : a ∈ ker f ↔ f a = 1 := iff.rfl
+
+  proposition ker_eq_preimage_one (f : A → B) : ker f = f '- '{1} :=
+  ext (take x, by rewrite [mem_ker_iff, -mem_preimage_iff, mem_singleton_iff])
+
+  definition ker_in (f : A → B) (S : set A) : set A := ker f ∩ S
+
+  proposition ker_in_univ (f : A → B) : ker_in f univ = ker f :=
+  !inter_univ
+end hasoneB
+
+section groupAB
+  variables [group A] [group B]
+  variable  {f : A → B}
+
+  proposition eq_of_mul_inv_mem_ker [is_hom f] {a₁ a₂ : A} (H : a₁ * a₂⁻¹ ∈ ker f) :
+    f a₁ = f a₂ :=
+  eq_of_mul_inv_eq_one (by rewrite [-hom_inv f, -hom_mul f]; exact H)
+
+  proposition mul_inv_mem_ker_of_eq [is_hom f] {a₁ a₂ : A} (H : f a₁ = f a₂) :
+    a₁ * a₂⁻¹ ∈ ker f :=
+  show f (a₁ * a₂⁻¹) = 1, by rewrite [hom_mul f, hom_inv f, H, mul.right_inv]
+
+  proposition eq_iff_mul_inv_mem_ker [is_hom f] (a₁ a₂ : A) : f a₁ = f a₂ ↔ a₁ * a₂⁻¹ ∈ ker f :=
+  iff.intro mul_inv_mem_ker_of_eq eq_of_mul_inv_mem_ker
+
+  proposition eq_of_mul_inv_mem_ker_in {G : set A} [is_subgroup G] [is_hom_on f G]
+      {a₁ a₂ : A} (a₁G : a₁ ∈ G) (a₂G : a₂ ∈ G) (H : a₁ * a₂⁻¹ ∈ ker_in f G) :
+    f a₁ = f a₂ :=
+  eq_of_mul_inv_eq_one (by rewrite [-hom_on_inv f a₂G, -hom_on_mul f a₁G (inv_mem a₂G)];
+    exact and.left H)
+
+  proposition mul_inv_mem_ker_in_of_eq {G : set A} [is_subgroup G] [is_hom_on f G]
+      {a₁ a₂ : A} (a₁G : a₁ ∈ G) (a₂G : a₂ ∈ G) (H : f a₁ = f a₂) :
+    a₁ * a₂⁻¹ ∈ ker_in f G :=
+  and.intro
+    (show f (a₁ * a₂⁻¹) = 1,
+      by rewrite [hom_on_mul f a₁G (inv_mem a₂G), hom_on_inv f a₂G, H, mul.right_inv])
+    (mul_mem a₁G (inv_mem a₂G))
+
+  proposition eq_iff_mul_inv_mem_ker_in {G : set A} [is_subgroup G] [is_hom_on f G]
+      {a₁ a₂ : A} (a₁G : a₁ ∈ G) (a₂G : a₂ ∈ G) :
+    f a₁ = f a₂ ↔ a₁ * a₂⁻¹ ∈ ker_in f G :=
+  iff.intro (mul_inv_mem_ker_in_of_eq a₁G a₂G) (eq_of_mul_inv_mem_ker_in a₁G a₂G)
+
+  -- Ouch! These versions are not equivalent to the ones before.
+
+  proposition eq_of_inv_mul_mem_ker [is_hom f] {a₁ a₂ : A} (H : a₁⁻¹ * a₂ ∈ ker f) :
+    f a₁ = f a₂ :=
+  eq.symm (eq_of_inv_mul_eq_one (by rewrite [-hom_inv f, -hom_mul f]; exact H))
+
+  proposition inv_mul_mem_ker_of_eq [is_hom f] {a₁ a₂ : A} (H : f a₁ = f a₂) :
+    a₁⁻¹ * a₂ ∈ ker f :=
+  show f (a₁⁻¹ * a₂) = 1, by rewrite [hom_mul f, hom_inv f, H, mul.left_inv]
+
+  proposition eq_iff_inv_mul_mem_ker [is_hom f] (a₁ a₂ : A) : f a₁ = f a₂ ↔ a₁⁻¹ * a₂ ∈ ker f :=
+  iff.intro inv_mul_mem_ker_of_eq eq_of_inv_mul_mem_ker
+
+  proposition eq_of_inv_mul_mem_ker_in {G : set A} [is_subgroup G] [is_hom_on f G]
+      {a₁ a₂ : A} (a₁G : a₁ ∈ G) (a₂G : a₂ ∈ G) (H : a₁⁻¹ * a₂ ∈ ker_in f G) :
+    f a₁ = f a₂ :=
+  eq.symm (eq_of_inv_mul_eq_one (by rewrite [-hom_on_inv f a₁G, -hom_on_mul f (inv_mem a₁G) a₂G];
+    exact and.left H))
+
+  proposition inv_mul_mem_ker_in_of_eq {G : set A} [is_subgroup G] [is_hom_on f G]
+      {a₁ a₂ : A} (a₁G : a₁ ∈ G) (a₂G : a₂ ∈ G) (H : f a₁ = f a₂) :
+    a₁⁻¹ * a₂ ∈ ker_in f G :=
+  and.intro
+    (show f (a₁⁻¹ * a₂) = 1,
+      by rewrite [hom_on_mul f (inv_mem a₁G) a₂G, hom_on_inv f a₁G, H, mul.left_inv])
+    (mul_mem (inv_mem a₁G) a₂G)
+
+  proposition eq_iff_inv_mul_mem_ker_in {G : set A} [is_subgroup G] [is_hom_on f G]
+      {a₁ a₂ : A} (a₁G : a₁ ∈ G) (a₂G : a₂ ∈ G) :
+    f a₁ = f a₂ ↔ a₁⁻¹ * a₂ ∈ ker_in f G :=
+  iff.intro (inv_mul_mem_ker_in_of_eq a₁G a₂G) (eq_of_inv_mul_mem_ker_in a₁G a₂G)
+
+  proposition eq_one_of_eq_one_of_injective [is_hom f] (H : injective f) {x : A}
+      (H' : f x = 1) :
+    x = 1 :=
+  H (by rewrite [H', hom_one f])
+
+  proposition eq_one_iff_eq_one_of_injective [is_hom f] (H : injective f) (x : A) :
+    f x = 1 ↔ x = 1 :=
+  iff.intro (eq_one_of_eq_one_of_injective H) (λ H', by rewrite [H', hom_one f])
+
+  proposition injective_of_forall_eq_one [is_hom f] (H : ∀ x, f x = 1 → x = 1) : injective f :=
+  take a₁ a₂, assume Heq,
+  have f (a₁ * a₂⁻¹) = 1, by rewrite [hom_mul f, hom_inv f, Heq, mul.right_inv],
+  eq_of_mul_inv_eq_one (H _ this)
+
+  proposition injective_of_ker_eq_singleton_one [is_hom f] (H : ker f = '{1}) : injective f :=
+  injective_of_forall_eq_one
+    (take x, suppose x ∈ ker f, by rewrite [H at this]; exact eq_of_mem_singleton this)
+
+  proposition ker_eq_singleton_one_of_injective [is_hom f] (H : injective f) : ker f = '{1} :=
+  ext (take x, by rewrite [mem_ker_iff, mem_singleton_iff, eq_one_iff_eq_one_of_injective H])
+
+  variable (f)
+  proposition injective_iff_ker_eq_singleton_one [is_hom f] : injective f ↔ ker f = '{1} :=
+  iff.intro ker_eq_singleton_one_of_injective injective_of_ker_eq_singleton_one
+  variable {f}
+
+  proposition eq_one_of_eq_one_of_inj_on {G : set A} [is_subgroup G] [is_hom_on f G]
+    (H : inj_on f G) {x : A} (xG : x ∈ G) (H' : f x = 1) :
+    x = 1 :=
+  H xG one_mem (by rewrite [H', hom_on_one f G])
+
+  proposition eq_one_iff_eq_one_of_inj_on {G : set A} [is_subgroup G] [is_hom_on f G]
+    (H : inj_on f G) {x : A} (xG : x ∈ G) [is_hom_on f G] :
+    f x = 1 ↔ x = 1 :=
+  iff.intro (eq_one_of_eq_one_of_inj_on H xG) (λ H', by rewrite [H', hom_on_one f G])
+
+  proposition inj_on_of_forall_eq_one {G : set A} [is_subgroup G] [is_hom_on f G]
+    (H : ∀₀ x ∈ G, f x = 1 → x = 1) : inj_on f G :=
+  take a₁ a₂, assume a₁G a₂G Heq,
+  have f (a₁ * a₂⁻¹) = 1,
+    by rewrite [hom_on_mul f a₁G (inv_mem a₂G), hom_on_inv f a₂G, Heq, mul.right_inv],
+  eq_of_mul_inv_eq_one (H (mul_mem a₁G (inv_mem a₂G)) this)
+
+  proposition inj_on_of_ker_in_eq_singleton_one {G : set A} [is_subgroup G] [is_hom_on f G]
+    (H : ker_in f G = '{1}) : inj_on f G :=
+  inj_on_of_forall_eq_one
+    (take x, assume xG fxone,
+      have x ∈ ker_in f G, from and.intro fxone xG,
+      by rewrite [H at this]; exact eq_of_mem_singleton this)
+
+  proposition ker_in_eq_singleton_one_of_inj_on {G : set A} [is_subgroup G] [is_hom_on f G]
+    (H : inj_on f G) : ker_in f G = '{1} :=
+  ext (take x,
+    begin
+      rewrite [↑ker_in, mem_inter_iff, mem_ker_iff, mem_singleton_iff],
+      apply iff.intro,
+        {intro H', cases H' with fxone xG, exact eq_one_of_eq_one_of_inj_on H xG fxone},
+      intro xone, rewrite xone, split, exact hom_on_one f G, exact one_mem
+    end)
+
+  variable (f)
+  proposition inj_on_iff_ker_in_eq_singleton_one (G : set A) [is_subgroup G] [is_hom_on f G] :
+    inj_on f G ↔ ker_in f G = '{1} :=
+  iff.intro ker_in_eq_singleton_one_of_inj_on inj_on_of_ker_in_eq_singleton_one
+  variable {f}
+
+  proposition conj_mem_ker [is_hom f] {a₁ : A} (a₂ : A) (H : a₁ ∈ ker f) : a₁^a₂ ∈ ker f :=
+  show f (a₁^a₂) = 1,
+    by rewrite [↑conj, *(hom_mul f), hom_inv f, eq_one_of_mem_ker H, mul_one, mul.left_inv]
+
+  variable (f)
+
+  proposition is_subgroup_ker_in [instance] (S : set A) [is_subgroup S] [is_hom_on f S] :
+    is_subgroup (ker_in f S) :=
+  ⦃ is_subgroup,
+    one_mem := and.intro (hom_on_one f S) one_mem,
+    mul_mem := λ a aker b bker,
+                 obtain (fa : f a = 1) (aS : a ∈ S), from aker,
+                 obtain (fb : f b = 1) (bS : b ∈ S), from bker,
+                 and.intro (show f (a * b) = 1, by rewrite [hom_on_mul f aS bS, fa, fb, one_mul])
+                   (mul_mem aS bS),
+    inv_mem := λ a aker,
+                 obtain (fa : f a = 1) (aS : a ∈ S), from aker,
+                 and.intro (show f (a⁻¹) = 1, by rewrite [hom_on_inv f aS, fa, one_inv])
+                   (inv_mem aS)
+  ⦄
+
+  proposition is_subgroup_ker [instance] [is_hom f] : is_subgroup (ker f) :=
+  begin
+    rewrite [-ker_in_univ f],
+    have is_hom_on f univ, from is_hom_on_of_is_hom f univ,
+    apply is_subgroup_ker_in f univ
+  end
+
+  proposition is_normal_in_ker_in [instance] (G : set A) [is_subgroup G] [is_hom_on f G] :
+    is_normal_in (ker_in f G) G :=
+  is_normal_in_of_forall_subset
+    (take x, assume xG, take y, assume yker,
+      obtain z [[(fz : f z = 1) zG] (yeq : x * z = y)], from yker,
+      have y = x * z * x⁻¹ * x, by rewrite [yeq, inv_mul_cancel_right],
+      show y ∈ ker_in f G * x,
+        begin
+          rewrite this,
+          apply mul_mem_rcoset,
+          apply and.intro,
+          show f (x * z * x⁻¹) = 1,
+            by rewrite [hom_on_mul f (mul_mem xG zG) (inv_mem xG), hom_on_mul f xG zG, fz,
+                        hom_on_inv f xG, mul_one, mul.right_inv],
+          show x * z * x⁻¹ ∈ G, from mul_mem (mul_mem xG zG) (inv_mem xG)
+        end)
+
+  proposition is_normal_ker [instance] [H : is_hom f] : is_normal (ker f) :=
+  begin
+    rewrite [-ker_in_univ, -is_normal_in_univ_iff_is_normal],
+    apply is_normal_in_ker_in,
+    exact is_hom_on_of_is_hom f univ
+  end
+
+end groupAB
+
+section subgroupH
+  variables [group A] [group B] {H : set A} [is_subgroup H]
+  variables {f : A → B} [is_hom f]
+
+  proposition subset_ker_of_forall (hyp : ∀ x y, x * H = y * H → f x = f y) : H ⊆ ker f :=
+  take h, assume hH,
+  have h * H = 1 * H, by rewrite [lcoset_eq_self_of_mem hH, one_lcoset],
+  have f h = f 1, from hyp h 1 this,
+  show f h = 1, by rewrite [this, hom_one f]
+
+  proposition eq_of_lcoset_eq_lcoset_of_subset_ker {x y : A} (hyp₀ : x * H = y * H) (hyp₁ : H ⊆ ker f) :
+    f x = f y :=
+  have y⁻¹ * x ∈ H, from inv_mul_mem_of_lcoset_eq_lcoset hyp₀,
+  eq.symm (eq_of_inv_mul_mem_ker (hyp₁ this))
+
+  variables (H f)
+  proposition subset_ker_iff : H ⊆ ker f ↔ ∀ x y, x * H = y * H → f x = f y :=
+  iff.intro (λ h₁ x y h₀, eq_of_lcoset_eq_lcoset_of_subset_ker h₀ h₁) subset_ker_of_forall
+end subgroupH
+
+section subgroupGH
+  variables [group A] [group B] {G H : set A} [is_subgroup G] [is_subgroup H]
+  variables {f : A → B} [is_hom_on f G]
+
+  proposition subset_ker_in_of_forall (hyp₀ : ∀₀ x ∈ G, ∀₀ y ∈ G, x * H = y * H → f x = f y)
+      (hyp₁ : H ⊆ G) :
+    H ⊆ ker_in f G :=
+  take h, assume hH,
+    have hG : h ∈ G, from hyp₁ hH,
+    and.intro
+      (have h * H = 1 * H, by rewrite [lcoset_eq_self_of_mem hH, one_lcoset],
+        have f h = f 1, from hyp₀ hG one_mem this,
+        show f h = 1, by rewrite [this, hom_on_one f G])
+      hG
+
+  proposition eq_of_lcoset_eq_lcoset_of_subset_ker_in {x : A} (xG : x ∈ G) {y : A} (yG : y ∈ G)
+      (hyp₀ : x * H = y * H) (hyp₁ : H ⊆ ker_in f G) :
+    f x = f y :=
+  have y⁻¹ * x ∈ H, from inv_mul_mem_of_lcoset_eq_lcoset hyp₀,
+  eq.symm (eq_of_inv_mul_mem_ker_in yG xG (hyp₁ this))
+
+  variables (H f)
+  proposition subset_ker_in_iff :
+    H ⊆ ker_in f G ↔ (H ⊆ G ∧ ∀₀ x ∈ G, ∀₀ y ∈ G, x * H = y * H → f x = f y) :=
+  iff.intro
+    (λ h₁, and.intro
+      (subset.trans h₁ (inter_subset_right _ _))
+      (λ x xG y yG h₀, eq_of_lcoset_eq_lcoset_of_subset_ker_in xG yG h₀ h₁))
+    (λ h, subset_ker_in_of_forall (and.right h) (and.left h))
+end subgroupGH
+
+
+/- the centralizer -/
+
+section has_mulA
+  variable [has_mul A]
+
+  abbreviation centralizes [reducible] (a : A) (S : set A) : Prop := ∀₀ b ∈ S, a * b = b * a
+
+  definition centralizer (S : set A) : set A := { a : A | centralizes a S }
+
+  abbreviation is_centralized_by (S T : set A) : Prop := T ⊆ centralizer S
+
+  abbreviation centralizer_in (S T : set A) : set A := T ∩ centralizer S
+
+  proposition mem_centralizer_iff_centralizes (a : A) (S : set A) :
+    a ∈ centralizer S ↔ centralizes a S := iff.refl _
+
+  proposition normalizes_of_centralizes {a : A} {S : set A} (H : centralizes a S) :
+    normalizes a S :=
+  ext (take b, iff.intro
+    (suppose b ∈ a * S,
+      obtain s [ains (beq : a * s = b)], from this,
+      show b ∈ S * a, by rewrite[-beq, H ains]; apply mem_image_of_mem _ ains)
+    (suppose b ∈ S * a,
+      obtain s [ains (beq : s * a = b)], from this,
+      show b ∈ a * S, by rewrite[-beq, -H ains]; apply mem_image_of_mem _ ains))
+
+  proposition centralizer_subset_normalizer (S : set A) : centralizer S ⊆ normalizer S :=
+  λ a acent, normalizes_of_centralizes acent
+
+  proposition centralizer_subset_centralizer {S T : set A} (ssubt : S ⊆ T) :
+    centralizer T ⊆ centralizer S :=
+  λ x xCentT s sS, xCentT _ (ssubt sS)
+end has_mulA
+
+section groupA
+  variable [group A]
+
+  proposition is_subgroup_centralizer [instance] [group A] (S : set A) :
+    is_subgroup (centralizer S) :=
+  ⦃ is_subgroup,
+    one_mem := λ b bS, by rewrite [one_mul, mul_one],
+    mul_mem := λ a acent b bcent c cS, by rewrite [mul.assoc, bcent cS, -*mul.assoc, acent cS],
+    inv_mem := λ a acent c cS, eq_mul_inv_of_mul_eq
+      (by rewrite [mul.assoc, -acent cS, inv_mul_cancel_left])⦄
+end groupA
+
+
+/- the subgroup generated by a set -/
+
+section groupA
+  variable [group A]
+
+  inductive subgroup_generated_by (S : set A) : A → Prop :=
+  | generators_mem : ∀ x, x ∈ S → subgroup_generated_by S x
+  | one_mem        : subgroup_generated_by S 1
+  | mul_mem        : ∀ x y, subgroup_generated_by S x → subgroup_generated_by S y →
+                       subgroup_generated_by S (x * y)
+  | inv_mem        : ∀ x, subgroup_generated_by S x → subgroup_generated_by S (x⁻¹)
+
+  theorem generators_subset_subgroup_generated_by (S : set A) : S ⊆ subgroup_generated_by S :=
+  subgroup_generated_by.generators_mem
+
+  theorem is_subgroup_subgroup_generated_by [instance] (S : set A) :
+    is_subgroup (subgroup_generated_by S) :=
+  ⦃ is_subgroup,
+    one_mem := subgroup_generated_by.one_mem S,
+    mul_mem := λ a amem b bmem, subgroup_generated_by.mul_mem a b amem bmem,
+    inv_mem := λ a amem, subgroup_generated_by.inv_mem a amem ⦄
+
+  theorem subgroup_generated_by_subset {S G : set A} [is_subgroup G] (H : S ⊆ G) :
+    subgroup_generated_by S ⊆ G :=
+  begin
+    intro x xgenS,
+    induction xgenS with a aS a b agen bgen aG bG a agen aG,
+      {exact H aS},
+      {exact one_mem},
+      {exact mul_mem aG bG},
+    exact inv_mem aG
+  end
+end groupA
+
+end group_theory
diff --git a/library/theories/group_theory/group_theory.md b/library/theories/group_theory/group_theory.md
new file mode 100644
index 000000000..8f54a6b48
--- /dev/null
+++ b/library/theories/group_theory/group_theory.md
@@ -0,0 +1,6 @@
+theories.group_theory
+=====================
+
+* [basic](basic.lean)
+* [subgroup_to_group](subgroup_to_group.lean)
+* [quotient](quotient.lean)
diff --git a/library/theories/group_theory/quotient.lean b/library/theories/group_theory/quotient.lean
new file mode 100644
index 000000000..f265af55a
--- /dev/null
+++ b/library/theories/group_theory/quotient.lean
@@ -0,0 +1,566 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Zipperer, Jeremy Avigad
+
+We provide two versions of the quoptient construction. They use the same names and notation:
+one lives in the namespace 'quotient_group' and the other lives in the namespace
+'quotient_group_general'.
+
+The first takes a group, A, and a normal subgroup, H. We have
+
+  quotient H       := the quotient of A by H
+  qproj H a        := the projection, with notation a' * G
+  qproj H ' s      := the image of s, with notation s / G
+  extend H respf   := given f : A → B respecting the equivalence relation, we get a function
+                      f : quotient G → B
+  bar f            := the above, G = ker f)
+
+The definition is constructive, using quotient types. We prove all the characteristic properties.
+
+As in the SSReflect library, we also provide a construction to quotient by an *arbitrary subgroup*.
+Now we have
+
+  quotient H       := the quotient of normalizer H by H
+  qproj H a        := still denoted a '* H, the projection when a is in normalizer H,
+                      arbitrary otherwise
+  qproj H G        := still denoted G / H, the image of the above
+  extend H G respf := given a homomorphism on G with ker_in G f ⊆ H, extends to a
+                      homomorphism G / H
+  bar G f          := the above, with H = ker_in f G
+
+This quotient H is defined by composing the first one with the construction which turns
+normalizer H into a group.
+-/
+import .subgroup_to_group theories.move
+open set function subtype classical quot
+
+namespace group_theory
+open coset_notation
+
+variables {A B C : Type}
+
+/- the quotient group -/
+
+namespace quotient_group
+
+variables [group A] (H : set A) [is_normal H]
+
+definition lcoset_setoid [instance] : setoid A :=
+setoid.mk (lcoset_equiv H) (equivalence_lcoset_equiv H)
+
+definition quotient := quot (lcoset_setoid H)
+
+private definition qone : quotient H := ⟦ 1 ⟧
+
+private definition qmul : quotient H → quotient H → quotient H :=
+quot.lift₂
+  (λ a b, ⟦a * b⟧)
+  (λ a₁ a₂ b₁ b₂ e₁ e₂, quot.sound (lcoset_equiv_mul H e₁ e₂))
+
+private definition qinv : quotient H → quotient H :=
+quot.lift
+  (λ a, ⟦a⁻¹⟧)
+  (λ a₁ a₂ e, quot.sound (lcoset_equiv_inv H e))
+
+private proposition qmul_assoc (a b c : quotient H) :
+  qmul H (qmul H a b) c = qmul H a (qmul H b c) :=
+quot.induction_on₂ a b (λ a b, quot.induction_on c (λ c,
+  have H :  ⟦a * b * c⟧ = ⟦a * (b * c)⟧, by rewrite mul.assoc,
+  H))
+
+private proposition qmul_qone (a : quotient H) : qmul H a (qone H) = a :=
+quot.induction_on a (λ a', show ⟦a' * 1⟧ = ⟦a'⟧, by rewrite mul_one)
+
+private proposition qone_qmul (a : quotient H) : qmul H (qone H) a = a :=
+quot.induction_on a (λ a', show ⟦1 * a'⟧ = ⟦a'⟧, by rewrite one_mul)
+
+private proposition qmul_left_inv (a : quotient H) : qmul H (qinv H a) a = qone H :=
+quot.induction_on a (λ a', show ⟦a'⁻¹ * a'⟧ = ⟦1⟧, by rewrite mul.left_inv)
+
+protected definition group [instance] : group (quotient H) :=
+⦃ group,
+  mul          := qmul H,
+  inv          := qinv H,
+  one          := qone H,
+  mul_assoc    := qmul_assoc H,
+  mul_one      := qmul_qone H,
+  one_mul      := qone_qmul H,
+  mul_left_inv := qmul_left_inv H
+⦄
+
+-- these theorems characterize the quotient group
+
+definition qproj (a : A) : quotient H := ⟦a⟧
+
+infix ` '* `:65  := λ {A' : Type} [group A'] a H' [is_normal H'], qproj H' a
+infix ` / `      := λ {A' : Type} [group A'] G H' [is_normal H'], qproj H' ' G
+
+proposition is_hom_qproj [instance] : is_hom (qproj H) :=
+is_mul_hom.mk (λ a b, rfl)
+
+variable {H}
+
+proposition qproj_eq_qproj {a b : A} (h : a * H = b * H) : a '* H = b '* H :=
+quot.sound h
+
+proposition lcoset_eq_lcoset_of_qproj_eq_qproj {a b : A} (h : a '* H = b '* H) :  a * H = b * H :=
+quot.exact h
+
+variable (H)
+
+proposition qproj_eq_qproj_iff (a b : A) : a '* H = b '* H ↔ a * H = b * H :=
+iff.intro lcoset_eq_lcoset_of_qproj_eq_qproj qproj_eq_qproj
+
+proposition ker_qproj [is_subgroup H] : ker (qproj H) = H :=
+ext (take a,
+  begin
+    rewrite [↑ker, mem_set_of_iff, -hom_one (qproj H), qproj_eq_qproj_iff,
+      one_lcoset],
+    show a * H = H ↔ a ∈ H, from iff.intro mem_of_lcoset_eq_self lcoset_eq_self_of_mem
+  end)
+
+proposition qproj_eq_one_iff [is_subgroup H] (a : A) : a '* H = 1 ↔ a ∈ H :=
+have H : qproj H a = 1 ↔ a ∈ ker (qproj H), from iff.rfl,
+by rewrite [H, ker_qproj]
+
+variable {H}
+
+proposition qproj_eq_one_of_mem [is_subgroup H] {a : A} (aH : a ∈ H) : a '* H = 1 :=
+iff.mpr (qproj_eq_one_iff H a) aH
+
+proposition mem_of_qproj_eq_one [is_subgroup H] {a : A} (h : a '* H = 1) : a ∈ H :=
+iff.mp (qproj_eq_one_iff H a) h
+
+variable (H)
+
+proposition surjective_qproj : surjective (qproj H) :=
+take y, quot.induction_on y (λ a, exists.intro a rfl)
+
+variable {H}
+
+proposition quotient_induction {P : quotient H → Prop} (h : ∀ a, P (a '* H)) : ∀ a, P a :=
+surjective_induction (surjective_qproj H) h
+
+proposition quotient_induction₂ {P : quotient H → quotient H → Prop}
+    (h : ∀ a₁ a₂, P (a₁ '* H) (a₂ '* H)) :
+  ∀ a₁ a₂, P a₁ a₂ :=
+surjective_induction₂ (surjective_qproj H) h
+
+variable (H)
+
+proposition image_qproj_self [is_subgroup H] : H / H = '{1} :=
+eq_of_subset_of_subset
+  (image_subset_of_maps_to
+    (take x, suppose x ∈ H,
+      show x '* H ∈ '{1},
+        from mem_singleton_of_eq (qproj_eq_one_of_mem `x ∈ H`)))
+  (take x, suppose x ∈ '{1},
+    have x = 1, from eq_of_mem_singleton this,
+    show x ∈ H / H, by rewrite this; apply mem_image_of_mem _ one_mem)
+
+-- extending a function A → B to a function A / H → B
+
+section respf
+
+variable {H}
+variables {f : A → B} (respf : ∀ a₁ a₂, a₁ * H = a₂ * H → f a₁ = f a₂)
+
+definition extend : quotient H → B := quot.lift f respf
+
+proposition extend_qproj (a : A) : extend respf (a '* H) = f a := rfl
+
+proposition extend_comp_qproj : extend respf ∘ (qproj H) = f := rfl
+
+proposition image_extend (G : set A) : (extend respf) ' (G / H) = f ' G :=
+by rewrite [-image_comp]
+
+variable [group B]
+
+proposition is_hom_extend [instance] [is_hom f] : is_hom (extend respf) :=
+is_mul_hom.mk (take a b,
+  show (extend respf (a * b)) = (extend respf a) * (extend respf b), from
+    quot.induction_on₂ a b (take a b, hom_mul f a b))
+
+proposition ker_extend : ker (extend respf) = ker f / H :=
+eq_of_subset_of_subset
+  (quotient_induction
+    (take a, assume Ha : qproj H a ∈ ker (extend respf),
+      have f a = 1, from Ha,
+      show a '* H ∈ ker f / H,
+        from mem_image_of_mem _ this))
+  (image_subset_of_maps_to
+    (take a, assume h : a ∈ ker f,
+      show extend respf (a '* H) = 1, from h))
+
+end respf
+
+end quotient_group
+
+
+/- the first homomorphism theorem for the quotient group -/
+
+namespace quotient_group
+  variables [group A] [group B] (f : A → B) [is_hom f]
+
+  lemma eq_of_lcoset_equiv_ker ⦃a b : A⦄ (h : lcoset_equiv (ker f) a b) : f a = f b :=
+  have b⁻¹ * a ∈ ker f, from inv_mul_mem_of_lcoset_eq_lcoset h,
+  eq.symm (eq_of_inv_mul_mem_ker this)
+
+  definition bar : quotient (ker f) → B := extend (eq_of_lcoset_equiv_ker f)
+
+  proposition bar_qproj (a : A) : bar f (a '* ker f) = f a := rfl
+
+  proposition is_hom_bar [instance] : is_hom (bar f) := is_hom_extend _
+
+  proposition image_bar (G : set A) : bar f ' (G / ker f) = f ' G :=
+  by rewrite [↑bar, image_extend]
+
+  proposition image_bar_univ : bar f ' univ = f ' univ :=
+  by rewrite [↑bar, -image_eq_univ_of_surjective (surjective_qproj (ker f)),
+       image_extend]
+
+  proposition surj_on_bar : surj_on (bar f) univ (f ' univ) :=
+  by rewrite [↑surj_on, image_bar_univ]; apply subset.refl
+
+  proposition ker_bar_eq : ker (bar f) = '{1} :=
+  by rewrite [↑bar, ker_extend, image_qproj_self]
+
+  proposition injective_bar : injective (bar f) :=
+  injective_of_ker_eq_singleton_one (ker_bar_eq f)
+end quotient_group
+
+
+/- a generic morphism extension property -/
+
+section
+  variables [group A] [group B] [group C]
+  variables (G : set A) [is_subgroup G]
+  variables (g : A → C) (f : A → B)
+
+  noncomputable definition gen_extend : C → B := λ c, f (inv_fun g G 1 c)
+
+  variables {G g f}
+
+  proposition eq_of_ker_in_subset {a₁ a₂ : A} (a₁G : a₁ ∈ G) (a₂G : a₂ ∈ G)
+      [is_hom_on g G] [is_hom_on f G] (Hker : ker_in g G ⊆ ker f) (H' : g a₁ = g a₂) :
+    f a₁ = f a₂ :=
+  have memG : a₁⁻¹ * a₂ ∈ G, from mul_mem (inv_mem a₁G) a₂G,
+  have a₁⁻¹ * a₂ ∈ ker_in g G, from inv_mul_mem_ker_in_of_eq a₁G a₂G H',
+  have a₁⁻¹ * a₂ ∈ ker_in f G, from and.intro (Hker this) memG,
+  show f a₁ = f a₂, from eq_of_inv_mul_mem_ker_in a₁G a₂G this
+
+  proposition gen_extend_spec [is_hom_on g G] [is_hom_on f G] (Hker : ker_in g G ⊆ ker f)
+    {a : A} (aG : a ∈ G) : gen_extend G g f (g a) = f a :=
+  eq_of_ker_in_subset (inv_fun_spec' aG) aG Hker (inv_fun_spec aG)
+
+  proposition is_hom_on_gen_extend [is_hom_on g G] [is_hom_on f G] (Hker : ker_in g G ⊆ ker f) :
+    is_hom_on (gen_extend G g f) (g ' G) :=
+  have is_subgroup (g ' G), from is_subgroup_image g G,
+  take c₁, assume c₁gG : c₁ ∈ g ' G,
+  take c₂, assume c₂gG : c₂ ∈ g ' G,
+  let ginv := inv_fun g G 1 in
+  have Hginv : maps_to ginv (g ' G) G, from maps_to_inv_fun one_mem,
+  have ginvc₁ : ginv c₁ ∈ G, from Hginv c₁gG,
+  have ginvc₂ : ginv c₂ ∈ G, from Hginv c₂gG,
+  have ginvc₁c₂ : ginv (c₁ * c₂) ∈ G, from Hginv (mul_mem c₁gG c₂gG),
+  have HH : ∀₀ c ∈ g ' G, g (ginv c) = c,
+    from λ a aG, right_inv_on_inv_fun_of_surj_on _ (surj_on_image g G) aG,
+  have eq₁ : g (ginv c₁) = c₁, from HH c₁gG,
+  have eq₂ : g (ginv c₂) = c₂, from HH c₂gG,
+  have eq₃ : g (ginv (c₁ * c₂)) = c₁ * c₂, from HH (mul_mem c₁gG c₂gG),
+  have g (ginv (c₁ * c₂)) = g ((ginv c₁) * (ginv c₂)),
+    by rewrite [eq₃, hom_on_mul g ginvc₁ ginvc₂, eq₁, eq₂],
+  have f (ginv (c₁ * c₂)) = f (ginv c₁ * ginv c₂),
+    from eq_of_ker_in_subset (ginvc₁c₂) (mul_mem ginvc₁ ginvc₂) Hker this,
+  show f (ginv (c₁ * c₂)) = f (ginv c₁) * f (ginv c₂),
+    by rewrite [this, hom_on_mul f ginvc₁ ginvc₂]
+end
+
+
+/- quotient by an arbitrary group, not necessarily normal -/
+
+namespace quotient_group_general
+
+variables [group A] (H : set A) [is_subgroup H]
+
+lemma is_normal_to_group_of_normalizer [instance] :
+  is_normal (to_group_of (normalizer H) ' H) :=
+have H1 : is_normal_in (to_group_of (normalizer H) ' H)
+                       (to_group_of (normalizer H) ' (normalizer H)),
+  from is_normal_in_image_image (subset_normalizer_self H) (to_group_of (normalizer H)),
+have H2 : to_group_of (normalizer H) ' (normalizer H) = univ,
+  from image_to_group_of_eq_univ (normalizer H),
+is_normal_of_is_normal_in_univ (by rewrite -H2; exact H1)
+
+section quotient_group
+open quotient_group
+
+noncomputable definition quotient : Type := quotient (to_group_of (normalizer H) ' H)
+
+noncomputable definition group_quotient  [instance] : group (quotient H) :=
+quotient_group.group (to_group_of (normalizer H) ' H)
+
+noncomputable definition qproj : A → quotient H :=
+qproj (to_group_of (normalizer H) ' H) ∘ (to_group_of (normalizer H))
+
+infix ` '* `:65  := λ {A' : Type} [group A'] a H' [is_subgroup H'], qproj H' a
+infix ` / `      := λ {A' : Type} [group A'] G H' [is_subgroup H'], qproj H' ' G
+
+proposition is_hom_on_qproj [instance] : is_hom_on (qproj H) (normalizer H) :=
+have H₀ : is_hom_on (to_group_of (normalizer H)) (normalizer H),
+  from is_hom_on_to_group_of (normalizer H),
+have H₁ : is_hom_on (quotient_group.qproj (to_group_of (normalizer H) ' H)) univ,
+  from iff.mpr (is_hom_on_univ_iff (quotient_group.qproj (to_group_of (normalizer H) ' H)))
+         (is_hom_qproj (to_group_of (normalizer H) ' H)),
+is_hom_on_comp H₀ H₁ (maps_to_univ (to_group_of (normalizer H)) (normalizer H))
+
+proposition is_hom_on_qproj' [instance] (G : set A) [is_normal_in H G] :
+  is_hom_on (qproj H) G :=
+is_hom_on_of_subset (qproj H) (subset_normalizer G H)
+
+proposition ker_in_qproj : ker_in (qproj H) (normalizer H) = H :=
+let tg := to_group_of (normalizer H) in
+begin
+  rewrite [↑ker_in, ker_eq_preimage_one, ↑qproj, preimage_comp, -ker_eq_preimage_one],
+  have is_hom_on tg H, from is_hom_on_of_subset _ (subset_normalizer_self H),
+  have is_subgroup (tg ' H), from is_subgroup_image tg H,
+  krewrite [ker_qproj, to_group_of_preimage_to_group_of_image (subset_normalizer_self H)]
+end
+
+end quotient_group
+
+variable {H}
+
+proposition qproj_eq_qproj_iff {a b : A} (Ha : a ∈ normalizer H) (Hb : b ∈ normalizer H) :
+   a '* H = b '* H ↔ a * H = b * H :=
+by rewrite [lcoset_eq_lcoset_iff, eq_iff_inv_mul_mem_ker_in Ha Hb, ker_in_qproj,
+            -inv_mem_iff, mul_inv, inv_inv]
+
+proposition qproj_eq_qproj {a b : A} (Ha : a ∈ normalizer H) (Hb : b ∈ normalizer H)
+    (h : a * H = b * H) :
+  a '* H = b '* H :=
+iff.mpr (qproj_eq_qproj_iff Ha Hb) h
+
+proposition lcoset_eq_lcoset_of_qproj_eq_qproj {a b : A}
+    (Ha : a ∈ normalizer H) (Hb : b ∈ normalizer H) (h : a '* H = b '* H) :
+  a * H = b * H :=
+iff.mp (qproj_eq_qproj_iff Ha Hb) h
+
+variable (H)
+
+proposition qproj_mem {a : A} {G : set A} (aG : a ∈ G) : a '* H ∈ G / H :=
+mem_image_of_mem _ aG
+
+proposition qproj_one : 1 '* H = 1 := hom_on_one (qproj H) (normalizer H)
+
+variable {H}
+
+proposition mem_of_qproj_mem {a : A} (anH : a ∈ normalizer H)
+    {G : set A} (HsubG : H ⊆ G) [is_subgroup G] [is_normal_in H G]
+  (aHGH : a '* H ∈ G / H): a ∈ G :=
+have GH : G ⊆ normalizer H, from subset_normalizer G H,
+obtain b [bG (bHeq : b '* H = a '* H)], from aHGH,
+have b * H = a * H, from lcoset_eq_lcoset_of_qproj_eq_qproj (GH bG) anH bHeq,
+have a ∈ b * H, by rewrite this; apply mem_lcoset_self,
+have a ∈ b * G, from lcoset_subset_lcoset b HsubG this,
+show a ∈ G, by rewrite [lcoset_eq_self_of_mem bG at this]; apply this
+
+proposition qproj_eq_one_iff {a : A} (Ha : a ∈ normalizer H) : a '* H = 1 ↔ a ∈ H :=
+by rewrite [-hom_on_one (qproj H) (normalizer H), qproj_eq_qproj_iff Ha one_mem, one_lcoset,
+        lcoset_eq_self_iff]
+
+proposition qproj_eq_one_of_mem {a : A} (aH : a ∈ H) : a '* H = 1 :=
+iff.mpr (qproj_eq_one_iff (subset_normalizer_self H aH)) aH
+
+proposition mem_of_qproj_eq_one {a : A} (Ha : a ∈ normalizer H) (h : a '* H = 1) : a ∈ H :=
+iff.mp (qproj_eq_one_iff Ha) h
+
+variable (H)
+
+section
+open quotient_group
+proposition surj_on_qproj_normalizer : surj_on (qproj H) (normalizer H) univ :=
+have H₀ : surj_on (to_group_of (normalizer H)) (normalizer H) univ,
+  from surj_on_to_group_of_univ (normalizer H),
+have H₁ : surj_on (quotient_group.qproj (to_group_of (normalizer H) ' H)) univ univ,
+  from surj_on_univ_of_surjective univ (surjective_qproj _),
+surj_on_comp H₁ H₀
+end
+
+variable {H}
+
+proposition quotient_induction {P : quotient H → Prop} (hyp : ∀₀ a ∈ normalizer H, P (a '* H)) :
+  ∀ a, P a :=
+surj_on_univ_induction (surj_on_qproj_normalizer H) hyp
+
+proposition quotient_induction₂ {P : quotient H → quotient H → Prop}
+    (hyp : ∀₀ a₁ ∈ normalizer H, ∀₀ a₂ ∈ normalizer H, P (a₁ '* H) (a₂ '* H)) :
+  ∀ a₁ a₂, P a₁ a₂ :=
+surj_on_univ_induction₂ (surj_on_qproj_normalizer H) hyp
+
+variable (H)
+
+proposition image_qproj_self : H / H = '{1} :=
+eq_of_subset_of_subset
+  (image_subset_of_maps_to
+    (take x, suppose x ∈ H,
+      show x '* H ∈ '{1},
+        from mem_singleton_of_eq (qproj_eq_one_of_mem `x ∈ H`)))
+  (take x, suppose x ∈ '{1},
+    have x = 1, from eq_of_mem_singleton this,
+    show x ∈ H / H,
+      by rewrite [this, -qproj_one H]; apply mem_image_of_mem _ one_mem)
+
+section respf
+
+variable (H)
+variables [group B] (G : set A) [is_subgroup G] (f : A → B)
+
+noncomputable definition extend : quotient H → B := gen_extend G (qproj H) f
+
+variables [is_hom_on f G] [is_normal_in H G]
+
+private proposition aux : is_hom_on (qproj H) G :=
+is_hom_on_of_subset (qproj H) (subset_normalizer G H)
+
+local attribute [instance] aux
+
+variables {H f}
+
+private proposition aux' (respf : H ⊆ ker f) : ker_in (qproj H) G ⊆ ker f :=
+subset.trans
+  (show ker_in (qproj H) G ⊆ ker_in (qproj H) (normalizer H),
+    from inter_subset_inter_left _ (subset_normalizer G H))
+  (by rewrite [ker_in_qproj]; apply respf)
+
+variable {G}
+
+proposition extend_qproj (respf : H ⊆ ker f) {a : A} (aG : a ∈ G) :
+  extend H G f (a '* H) = f a :=
+gen_extend_spec (aux' G respf) aG
+
+proposition image_extend (respf : H ⊆ ker f) {s : set A} (ssubG : s ⊆ G) :
+  extend H G f ' (s / H) = f ' s :=
+begin
+  rewrite [-image_comp],
+  apply image_eq_image_of_eq_on,
+  intro a amems,
+  apply extend_qproj respf (ssubG amems)
+end
+
+variable (G)
+
+proposition is_hom_on_extend [instance] (respf : H ⊆ ker f) : is_hom_on (extend H G f) (G / H) :=
+by unfold extend; apply is_hom_on_gen_extend (aux' G respf)
+
+variable {G}
+
+proposition ker_in_extend [is_subgroup G] (respf : H ⊆ ker f) (HsubG : H ⊆ G) :
+  ker_in (extend H G f) (G / H) = (ker_in f G) / H :=
+begin
+  apply ext,
+  intro aH,
+  cases surj_on_qproj_normalizer H (show aH ∈ univ, from trivial) with a atemp,
+  cases atemp with anH aHeq,
+  rewrite -aHeq,
+  apply iff.intro,
+  { intro akerin,
+    cases akerin with aker ain,
+    have a '* H ∈ G / H, from ain,
+    have a ∈ G, from mem_of_qproj_mem anH HsubG this,
+    have a '* H ∈ ker (extend H G f), from aker,
+    have extend H G f (a '* H) = 1, from this,
+    have f a = extend H G f (a '* H), from eq.symm (extend_qproj respf `a ∈ G`),
+    have f a = 1, by rewrite this; assumption,
+    have a ∈ ker_in f G, from and.intro this `a ∈ G`,
+    show a '* H ∈ (ker_in f G) / H, from qproj_mem H this},
+  intro aHker,
+  have aker : a ∈ ker_in f G,
+    begin
+      have Hsub : H ⊆ ker_in f G, from subset_inter respf HsubG,
+      have is_normal_in H (ker_in f G),
+        from subset.trans (inter_subset_right (ker f) G) (subset_normalizer G H),
+      apply (mem_of_qproj_mem anH Hsub aHker)
+    end,
+  have a ∈ G, from and.right aker,
+  have f a = 1, from and.left aker,
+  have extend H G f (a '* H) = 1,
+    from eq.trans (extend_qproj respf `a ∈ G`) this,
+  show a '* H ∈ ker_in (extend H G f) (G / H),
+    from and.intro this (qproj_mem H `a ∈ G`)
+end
+
+/- (comment from Jeremy)
+This version kills the elaborator. I don't know why.
+Tracing class instances doesn't show a problem. My best guess is that it is
+the backgracking from the "obtain".
+
+proposition ker_in_extend [is_subgroup G] (respf : H ⊆ ker f) (HsubG : H ⊆ G) :
+  ker_in (extend H G f) (qproj H ' G) = qproj H ' (ker_in f G) :=
+ext (take aH,
+  obtain a [(anH : a ∈ normalizer H) (aHeq : a '* H = aH)],
+    from surj_on_qproj_normalizer H (show aH ∈ univ, from trivial),
+  begin
+    rewrite -aHeq, apply iff.intro, unfold ker_in,
+    exact
+      (assume aker : a '* H ∈ ker (extend H G f) ∩ (qproj H ' G),
+        have a '* H ∈ qproj H ' G, from and.right aker,
+        have a ∈ G, from mem_of_qproj_mem anH HsubG this,
+        -- Uncommenting the next line of code slows things down dramatically.
+        -- Uncommenting the one after kills the system.
+        -- have a '* H ∈ ker (extend H G f), from and.left aker,
+        -- have extend H G f (a '* H) = 1, from this,
+        -- have f a = extend H G f (a '* H), from eq.symm (extend_qproj respf `a ∈ G`),
+        -- have f a = 1, by rewrite [-this, extend_qproj respf aG],
+        -- have a ∈ ker_in f G, from and.intro this `a ∈ G`,
+        show a '* H ∈ qproj H ' (ker_in f G), from sorry),
+    exact
+      (assume hyp : a '* H ∈ qproj H ' (ker_in f G),
+        show a '* H ∈ ker_in (extend H G f) (qproj H ' G), from sorry)
+  end)
+-/
+
+end respf
+
+attribute quotient [irreducible]
+
+end quotient_group_general
+
+/- the first homomorphism theorem for general quotient groups -/
+
+namespace quotient_group_general
+
+variables [group A] [group B] (G : set A) [is_subgroup G]
+variables (f : A → B) [is_hom_on f G]
+
+noncomputable definition bar : quotient (ker_in f G) → B :=
+extend (ker_in f G) G f
+
+proposition bar_qproj {a : A} (aG : a ∈ G) : bar G f (a '* ker_in f G) = f a :=
+extend_qproj (inter_subset_left _ _) aG
+
+proposition is_hom_on_bar [instance] : is_hom_on (bar G f) (G / ker_in f G) :=
+have is_subgroup (ker f ∩ G), from is_subgroup_ker_in f G,
+have is_normal_in (ker f ∩ G) G, from is_normal_in_ker_in f G,
+is_hom_on_extend G (inter_subset_left _ _)
+
+proposition image_bar {s : set A} (ssubG : s ⊆ G) : bar G f ' (s / ker_in f G) = f ' s :=
+have is_subgroup (ker f ∩ G), from is_subgroup_ker_in f G,
+have is_normal_in (ker f ∩ G) G, from is_normal_in_ker_in f G,
+image_extend (inter_subset_left _ _) ssubG
+
+proposition surj_on_bar : surj_on (bar G f) (G / ker_in f G) (f ' G) :=
+by rewrite [↑surj_on, image_bar G f (@subset.refl _ G)]; apply subset.refl
+
+proposition ker_in_bar : ker_in (bar G f) (G / ker_in f G) = '{1} :=
+have H₀ : ker_in f G ⊆ ker f, from inter_subset_left _ _,
+have H₁ : ker_in f G ⊆ G, from inter_subset_right _ _,
+by rewrite [↑bar, ker_in_extend H₀ H₁, image_qproj_self]
+
+proposition inj_on_bar : inj_on (bar G f) (G / ker_in f G) :=
+inj_on_of_ker_in_eq_singleton_one (ker_in_bar G f)
+
+end quotient_group_general
+
+end group_theory
diff --git a/library/theories/group_theory/subgroup_to_group.lean b/library/theories/group_theory/subgroup_to_group.lean
new file mode 100644
index 000000000..52dad6c44
--- /dev/null
+++ b/library/theories/group_theory/subgroup_to_group.lean
@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad
+
+Turn a subgroup into a group on the corresponding subtype. Given
+
+  variables {A : Type} [group A] (G : set A) [is_subgroup G]
+
+we have:
+
+  group_of G      := G, viewed as a group
+  to_group_of G a := if a is in G, returns the image in group_of G, or 1 otherwise
+  to_subgroup a   := given a : group_of G, return the underlying element
+-/
+import .basic
+open set function subtype classical
+
+variables {A B C : Type}
+
+namespace group_theory
+
+definition group_of (G : set A) : Type := subtype G
+
+definition subgroup_to_group {G : set A} ⦃a : A⦄ (aG : a ∈ G) : group_of G := tag a aG
+
+definition to_subgroup {G : set A} (a : group_of G) : A := elt_of a
+
+proposition to_subgroup_mem {G : set A} (a : group_of G) : to_subgroup a ∈ G := has_property a
+
+variables [group A] (G : set A) [is_subgroup G]
+
+definition group_of.group [instance] : group (group_of G) :=
+⦃ group,
+  mul          := λ a b,  subgroup_to_group (mul_mem (to_subgroup_mem a) (to_subgroup_mem b)),
+  mul_assoc    := λ a b c, subtype.eq !mul.assoc,
+  one          := subgroup_to_group (@one_mem A _ G _),
+  one_mul      := λ a, subtype.eq !one_mul,
+  mul_one      := λ a, subtype.eq !mul_one,
+  inv          := λ a, tag (elt_of a)⁻¹ (inv_mem (to_subgroup_mem a)),
+  mul_left_inv := λ a, subtype.eq !mul.left_inv
+⦄
+
+proposition is_hom_group_to_subgroup [instance] : is_hom (@to_subgroup A G) :=
+is_mul_hom.mk
+  (take g₁ g₂ : group_of G,
+    show to_subgroup (g₁ * g₂) = to_subgroup g₁ * to_subgroup g₂,
+      by cases g₁; cases g₂; reflexivity)
+
+noncomputable definition to_group_of (a : A) : group_of G :=
+if H : a ∈ G then subgroup_to_group H else 1
+
+proposition is_hom_on_to_group_of [instance] : is_hom_on (to_group_of G) G :=
+take g₁, assume g₁G, take g₂, assume g₂G,
+show to_group_of G (g₁ * g₂) = to_group_of G g₁ * to_group_of G g₂,
+  by rewrite [↑to_group_of, dif_pos g₁G, dif_pos g₂G, dif_pos (mul_mem g₁G g₂G)]
+
+proposition to_group_to_subgroup : left_inverse (to_group_of G) to_subgroup :=
+begin
+  intro a, rewrite [↑to_group_of, dif_pos (to_subgroup_mem a)],
+  apply subtype.eq, reflexivity
+end
+
+-- proposition to_subgroup_to_group {a : A} (aG : a ∈ G) : to_subgroup (to_group_of G a) = a :=
+-- by rewrite [↑to_group_of, dif_pos aG]
+-- curiously, in the next version, "by rewrite [↑to_group_of, dif_pos aG]" doesn't work.
+
+proposition to_subgroup_to_group : left_inv_on to_subgroup (to_group_of G) G :=
+λ a aG, by xrewrite [dif_pos aG]
+
+variable {G}
+proposition inj_on_to_group_of : inj_on (to_group_of G) G :=
+inj_on_of_left_inv_on (to_subgroup_to_group G)
+variable (G)
+
+proposition surj_on_to_group_of_univ : surj_on (to_group_of G) G univ :=
+take y, assume yuniv, mem_image (to_subgroup_mem y) (to_group_to_subgroup G y)
+
+proposition image_to_group_of_eq_univ : to_group_of G ' G = univ :=
+image_eq_of_maps_to_of_surj_on (maps_to_univ _ _) (surj_on_to_group_of_univ G)
+
+proposition surjective_to_group_of : surjective (to_group_of G) :=
+surjective_of_has_right_inverse (exists.intro _ (to_group_to_subgroup G))
+
+variable {G}
+proposition to_group_of_preimage_to_group_of_image {S : set A} (SsubG : S ⊆ G) :
+  (to_group_of G) '- (to_group_of G ' S) ∩ G = S :=
+ext (take x, iff.intro
+  (assume H,
+    obtain Hx (xG : x ∈ G), from H,
+    have to_group_of G x ∈ to_group_of G ' S, from mem_of_mem_preimage Hx,
+    obtain y [(yS : y ∈ S) (Heq : to_group_of G y = to_group_of G x)], from this,
+    have y = x, from inj_on_to_group_of (SsubG yS) xG Heq,
+    show x ∈ S, by rewrite -this; exact yS)
+  (assume xS, and.intro
+     (mem_preimage (show to_group_of G x ∈ to_group_of G ' S, from mem_image_of_mem _ xS))
+     (SsubG xS)))
+
+end group_theory
diff --git a/library/theories/move.lean b/library/theories/move.lean
index 0126644fd..b2d468368 100644
--- a/library/theories/move.lean
+++ b/library/theories/move.lean
@@ -7,9 +7,46 @@ Temporary file; move in Lean3.
 import data.set algebra.order_bigops
 import data.finset data.list.sort
 
--- move to data.set
+-- move this to init.function
+
+section
+open function
+postfix `^~` :std.prec.max_plus := swap
+end
+
+-- move to algebra
+
+theorem eq_of_inv_mul_eq_one {A : Type} {a b : A} [group A] (H : b⁻¹ * a = 1) : a = b :=
+have a⁻¹ * 1 = a⁻¹, by inst_simp,
+by inst_simp
+
+-- move to init.quotient
+
+namespace quot
+open classical
+
+variables {A : Type} [s : setoid A]
+
+protected theorem exists_eq_mk (x : quot s) : ∃ a : A, x = ⟦a⟧ :=
+quot.induction_on x (take a, exists.intro _ rfl)
+
+protected noncomputable definition repr (x : quot s) : A := some (quot.exists_eq_mk x)
+
+protected theorem mk_repr_eq (x : quot s) : ⟦ quot.repr x ⟧ = x :=
+eq.symm (some_spec (quot.exists_eq_mk x))
+
+open setoid
+include s
+protected theorem repr_mk_equiv (a : A) : quot.repr ⟦a⟧ ≈ a :=
+quot.exact (by rewrite quot.mk_repr_eq)
+
+end quot
+
+
+-- move to data.set.basic
 
 namespace set
+open function
 
 lemma inter_eq_self_of_subset {X : Type} {s t : set X} (Hst : s ⊆ t) : s ∩ t = s :=
 ext (take x, iff.intro
@@ -81,6 +118,146 @@ proposition preimage_Union {I X Y : Type} (f : X → Y) (u : I → set Y) :
   f '- (⋃ i, u i) = ⋃ i, (f '- (u i)) :=
 ext (take x, !iff.refl)
 
+-- TODO: rename "injective" to "inj"
+-- TODO: turn around equality in definition of image
+-- TODO: use ∀₀ in definition of injective (and define notation for ∀₀ x y ∈ s, ...)
+
+attribute [trans] subset.trans -- really? this was never declared? And all the variants...
+
+proposition mem_set_of_iff {X : Type} (P : X → Prop) (a : X) : a ∈ { x : X | P x } ↔ P a :=
+ iff.refl _
+
+proposition mem_set_of {X : Type} {P : X → Prop} {a : X} (Pa : P a) : a ∈ { x : X | P x } := Pa
+
+proposition of_mem_set_of {X : Type} {P : X → Prop} {a : X} (H : a ∈ { x : X | P x }) : P a := H
+
+proposition forallb_of_forall {X : Type} {P : X → Prop} (s : set X) (H : ∀ x, P x) :
+  ∀₀ x ∈ s, P x :=
+λ x xs, H x
+
+proposition forall_of_forallb_univ {X : Type} {P : X → Prop} (H : ∀₀ x ∈ univ, P x) : ∀ x, P x :=
+λ x, H trivial
+
+proposition forallb_univ_iff_forall {X : Type} (P : X → Prop) : (∀₀ x ∈ univ, P x) ↔ ∀ x, P x :=
+iff.intro forall_of_forallb_univ !forallb_of_forall
+
+proposition forallb_of_subset {X : Type} {s t : set X} {P : X → Prop}
+  (ssubt : s ⊆ t) (Ht : ∀₀ x ∈ t, P x) : ∀₀ x ∈ s, P x :=
+λ x xs, Ht (ssubt xs)
+
+proposition forallb_of_forall₂ {X Y : Type} {P : X → Y → Prop} (s : set X) (t : set Y)
+  (H : ∀ x y, P x y) : ∀₀ x ∈ s, ∀₀ y ∈ t, P x y :=
+λ x xs y yt, H x y
+
+proposition forall_of_forallb_univ₂ {X Y : Type} {P : X → Y → Prop}
+  (H : ∀₀ x ∈ univ, ∀₀ y ∈ univ, P x y) : ∀ x y, P x y :=
+λ x y, H trivial trivial
+
+proposition forallb_univ_iff_forall₂ {X Y : Type} (P : X → Y → Prop) :
+  (∀₀ x ∈ univ, ∀₀ y ∈ univ, P x y) ↔ ∀ x y, P x y :=
+iff.intro forall_of_forallb_univ₂ !forallb_of_forall₂
+
+proposition forallb_of_subset₂ {X Y : Type} {s₁ t₁ : set X} {s₂ t₂ : set Y} {P : X → Y → Prop}
+    (ssubt₁ : s₁ ⊆ t₁) (ssubt₂ : s₂ ⊆ t₂) (Ht : ∀₀ x ∈ t₁, ∀₀ y ∈ t₂, P x y) :
+  ∀₀ x ∈ s₁, ∀₀ y ∈ s₂, P x y :=
+λ x xs y ys, Ht (ssubt₁ xs) (ssubt₂ ys)
+
+theorem maps_to_univ {X Y : Type} (f : X → Y) (a : set X) : maps_to f a univ :=
+take x, assume H, trivial
+
+theorem surj_on_image {X Y : Type} (f : X → Y) (a : set X) : surj_on f a (f ' a) :=
+λ y Hy, Hy
+
+theorem image_eq_univ_of_surjective {X Y : Type} {f : X → Y} (H : surjective f) :
+  f ' univ = univ :=
+ext (take y, iff.intro (λ H', trivial)
+  (λ H', obtain x xeq, from H y,
+    show y ∈ f ' univ, from mem_image trivial xeq))
+
+proposition image_inter_subset {X Y : Type} (f : X → Y) (s t : set X) :
+  f ' (s ∩ t) ⊆ f ' s ∩ f ' t :=
+take y, assume ymem,
+obtain x [[xs xt] (xeq : f x = y)], from ymem,
+show y ∈ f ' s ∩ f ' t,
+  begin
+    rewrite -xeq,
+    exact (and.intro (mem_image_of_mem f xs) (mem_image_of_mem f xt))
+  end
+
+--proposition image_eq_of_maps_to_of_surj_on {X Y : Type} {f : X → Y} {s : set X} {t : set Y}
+--    (H : maps_to f s t) (H' : surj_on f s t) :
+--  f ' s = t :=
+--eq_of_subset_of_subset (image_subset_of_maps_to H) H'
+
+proposition surj_on_of_image_eq {X Y : Type} {f : X → Y} {s : set X} {t : set Y}
+    (H : f ' s = t) :
+  surj_on f s t :=
+by rewrite [↑surj_on, H]; apply subset.refl
+
+proposition surjective_induction {X Y : Type} {P : Y → Prop} {f : X → Y}
+    (surjf : surjective f) (H : ∀ x, P (f x)) :
+  ∀ y, P y :=
+take y,
+obtain x (yeq : f x = y), from surjf y,
+show P y, by rewrite -yeq; apply H x
+
+proposition surjective_induction₂ {X Y : Type} {P : Y → Y → Prop} {f : X → Y}
+    (surjf : surjective f) (H : ∀ x₁ x₂, P (f x₁) (f x₂)) :
+  ∀ y₁ y₂, P y₁ y₂ :=
+take y₁ y₂,
+obtain x₁ (y₁eq : f x₁ = y₁), from surjf y₁,
+obtain x₂ (y₂eq : f x₂ = y₂), from surjf y₂,
+show P y₁ y₂, by rewrite [-y₁eq, -y₂eq]; apply H x₁ x₂
+
+proposition surj_on_univ_induction {X Y : Type} {P : Y → Prop} {f : X → Y} {s : set X}
+    (surjfs : surj_on f s univ) (H : ∀₀ x ∈ s, P (f x)) :
+  ∀ y, P y :=
+take y,
+obtain x [xs (yeq : f x = y)], from surjfs trivial,
+show P y, by rewrite -yeq; apply H xs
+
+proposition surj_on_univ_induction₂ {X Y : Type} {P : Y → Y → Prop} {f : X → Y} {s : set X}
+    (surjfs : surj_on f s univ) (H : ∀₀ x₁ ∈ s, ∀₀ x₂ ∈ s, P (f x₁) (f x₂)) :
+  ∀ y₁ y₂, P y₁ y₂ :=
+take y₁ y₂,
+obtain x₁ [x₁s (y₁eq : f x₁ = y₁)], from surjfs trivial,
+obtain x₂ [x₂s (y₂eq : f x₂ = y₂)], from surjfs trivial,
+show P y₁ y₂, by rewrite [-y₁eq, -y₂eq]; apply H x₁s x₂s
+
+proposition surj_on_univ_of_surjective {X Y : Type} {f : X → Y} (s : set Y) (H : surjective f) :
+  surj_on f univ s :=
+take y, assume ys,
+obtain x yeq, from H y,
+mem_image !mem_univ yeq
+
+proposition mem_of_mem_image_of_injective {X Y : Type} {f : X → Y} {s : set X} {a : X}
+    (injf : injective f) (H : f a ∈ f ' s) :
+  a ∈ s :=
+obtain b [bs faeq], from H,
+have b = a, from injf faeq,
+by rewrite -this; apply bs
+
+proposition mem_of_mem_image_of_inj_on {X Y : Type} {f : X → Y} {s t : set X} {a : X} (Ha : a ∈ t)
+    (Hs : s ⊆ t) (injft : inj_on f t) (H : f a ∈ f ' s)  :
+  a ∈ s :=
+obtain b [bs faeq], from H,
+have b = a, from injft (Hs bs) Ha faeq,
+by rewrite -this; apply bs
+
+proposition eq_singleton_of_forall_eq {A : Type} {s : set A} {x : A} (xs : x ∈ s) (H : ∀₀ y ∈ s, y = x) :
+  s = '{x} :=
+ext (take y, iff.intro
+  (assume ys, mem_singleton_of_eq (H ys))
+  (assume yx, by rewrite (eq_of_mem_singleton yx); assumption))
+
+proposition insert_subset {A : Type} {s t : set A} {a : A} (amem : a ∈ t) (ssubt : s ⊆ t) : insert a s ⊆ t :=
+take x, assume xias,
+  or.elim (eq_or_mem_of_mem_insert xias)
+    (by simp)
+    (take H, ssubt H)
+
+-- move to data.set.finite
+
 lemma finite_sUnion {A : Type} {S : set (set A)} [H : finite S] :
   (∀s, s ∈ S → finite s) → finite ⋃₀S :=
 induction_on_finite S
@@ -100,6 +277,49 @@ lemma finite_of_finite_sUnion {A : Type} (S : set (set A)) (H : finite ⋃₀S)
 have finite (𝒫 (⋃₀ S)), from finite_powerset _,
 show finite S, from finite_subset (subset_powerset_sUnion S)
 
+section nat
+open nat
+
+proposition ne_empty_of_card_pos {A : Type} {s : set A} (H : card s > 0) : s ≠ ∅ :=
+take H', begin rewrite [H' at H, card_empty at H], exact lt.irrefl 0 H end
+
+lemma eq_of_card_eq_one {A : Type} {S : set A} (H : card S = 1) {x y : A} (Hx : x ∈ S) (Hy : y ∈ S) :
+  x = y :=
+have finite S,
+  from classical.by_contradiction
+    (assume nfinS, begin rewrite (card_of_not_finite nfinS) at H, contradiction end),
+classical.by_contradiction
+(assume H0 : x ≠ y,
+  have H1 : '{x, y} ⊆ S, from insert_subset Hx (insert_subset Hy (empty_subset _)),
+  have x ∉ '{y}, from assume H, H0 (eq_of_mem_singleton H),
+  have 2 ≤ 1, from calc
+    2 = card '{x, y} : by rewrite [card_insert_of_not_mem this,
+                            card_insert_of_not_mem (not_mem_empty _), card_empty]
+      ... ≤ card S   : card_le_card_of_subset H1
+      ... = 1        : H,
+  show false, from dec_trivial this)
+
+proposition eq_singleton_of_card_eq_one {A : Type} {s : set A} {x : A} (H : card s = 1) (xs : x ∈ s) :
+  s = '{x} :=
+eq_singleton_of_forall_eq xs (take y, assume ys, eq.symm (eq_of_card_eq_one H xs ys))
+
+proposition exists_eq_singleton_of_card_eq_one {A : Type} {s : set A} (H : card s = 1) : ∃ x, s = '{x} :=
+have s ≠ ∅, from ne_empty_of_card_pos (by rewrite H; apply dec_trivial),
+obtain (x : A) (xs : x ∈ s), from exists_mem_of_ne_empty this,
+exists.intro x (eq_singleton_of_card_eq_one H xs)
+
+end nat
+
+-- move to data.set.classical_inverse (and rename file to "inverse")
+
+theorem inv_fun_spec {X Y : Type} {f : X → Y} {a : set X} {dflt : X} {x : X} (xa : x ∈ a) :
+  f (inv_fun f a dflt (f x)) = f x :=
+and.right (inv_fun_pos (exists.intro x (and.intro xa rfl)))
+
+theorem inv_fun_spec' {X Y : Type} {f : X → Y} {a : set X} {dflt : X} {x : X} (xa : x ∈ a) :
+  inv_fun f a dflt (f x) ∈ a :=
+and.left (inv_fun_pos (exists.intro x (and.intro xa rfl)))
+
 end set
 
 
diff --git a/library/theories/theories.md b/library/theories/theories.md
index 4b2a8c301..2b54a8bcd 100644
--- a/library/theories/theories.md
+++ b/library/theories/theories.md
@@ -3,7 +3,8 @@ theories
 
 * [number_theory](number_theory/number_theory.md)
 * [combinatorics](combinatorics/combinatorics.md)
-* [finite_group_theory](group_theory/group_theory.md) : group theory based on finsets
+* [group_theory](group_theory/group_theory.md)
+* [finite_group_theory](finite_group_theory/finite_group_theory.md) : group theory based on finsets
 * [topology](topology/topology.md)
 * [analysis](analysis/analysis.md)
 * [measure_theory](measure_theory/measure_theory.md)
\ No newline at end of file