diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
index 7c766acbb953f..3ea06ddf286e6 100644
--- a/src/data/multiset/basic.lean
+++ b/src/data/multiset/basic.lean
@@ -2169,6 +2169,14 @@ end rel
 
 section sum_inequalities
 
+lemma le_sum_of_mem [canonically_ordered_add_monoid α] {m : multiset α} {a : α}
+  (h : a ∈ m) : a ≤ m.sum :=
+begin
+  obtain ⟨m', rfl⟩ := exists_cons_of_mem h,
+  rw [sum_cons],
+  exact _root_.le_add_right (le_refl a),
+end
+
 variables [ordered_add_comm_monoid α]
 
 lemma sum_map_le_sum
diff --git a/src/group_theory/perm/cycle_type.lean b/src/group_theory/perm/cycle_type.lean
index a47f89187309f..bb895276667cd 100644
--- a/src/group_theory/perm/cycle_type.lean
+++ b/src/group_theory/perm/cycle_type.lean
@@ -281,6 +281,42 @@ begin
     rw [hd.cycle_type, ← extend_domain_mul, (hd.extend_domain f).cycle_type, hσ, hτ] }
 end
 
+lemma mem_cycle_type_iff {n : ℕ} {σ : perm α} :
+  n ∈ cycle_type σ ↔ ∃ c τ : perm α, σ = c * τ ∧ disjoint c τ ∧ is_cycle c ∧ c.support.card = n :=
+begin
+  split,
+  { intro h,
+    obtain ⟨l, rfl, hlc, hld⟩ := trunc_cycle_factors σ,
+    rw cycle_type_eq _ rfl hlc hld at h,
+    obtain ⟨c, cl, rfl⟩ := list.exists_of_mem_map h,
+    rw (list.perm_cons_erase cl).pairwise_iff (λ _ _ hd, _) at hld,
+    swap, { exact hd.symm },
+    refine ⟨c, (l.erase c).prod, _, _, hlc _ cl, rfl⟩,
+    { rw [← list.prod_cons,
+        (list.perm_cons_erase cl).symm.prod_eq' (hld.imp (λ a b ab, ab.mul_comm))] },
+    { exact disjoint_prod_right _ (λ g, list.rel_of_pairwise_cons hld) } },
+  { rintros ⟨c, t, rfl, hd, hc, rfl⟩,
+    simp [hd.cycle_type, hc.cycle_type] }
+end
+
+lemma le_card_support_of_mem_cycle_type {n : ℕ} {σ : perm α} (h : n ∈ cycle_type σ) :
+  n ≤ σ.support.card :=
+(le_sum_of_mem h).trans (le_of_eq σ.sum_cycle_type)
+
+lemma cycle_type_of_card_le_mem_cycle_type_add_two {n : ℕ} {g : perm α}
+  (hn2 : fintype.card α < n + 2) (hng : n ∈ g.cycle_type) :
+  g.cycle_type = {n} :=
+begin
+  obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycle_type_iff.1 hng,
+  by_cases g'1 : g' = 1,
+  { rw [hd.cycle_type, hc.cycle_type, multiset.singleton_eq_singleton, multiset.singleton_coe,
+      g'1, cycle_type_one, add_zero] },
+  contrapose! hn2,
+  apply le_trans _ (c * g').support.card_le_univ,
+  rw [hd.card_support_mul],
+  exact add_le_add_left (two_le_card_support_of_ne_one g'1) _,
+end
+
 end cycle_type
 
 lemma is_cycle_of_prime_order' {σ : perm α} (h1 : (order_of σ).prime)
@@ -401,6 +437,19 @@ by rwa [is_three_cycle, cycle_type_inv]
 @[simp] lemma inv_iff {f : perm α} : is_three_cycle (f⁻¹) ↔ is_three_cycle f :=
 ⟨by { rw ← inv_inv f, apply inv }, inv⟩
 
+lemma order_of {g : perm α} (ht : is_three_cycle g) :
+  order_of g = 3 :=
+by rw [←lcm_cycle_type, ht.cycle_type, multiset.singleton_eq_singleton,
+  multiset.lcm_singleton, nat.normalize_eq]
+
+lemma is_three_cycle_sq {g : perm α} (ht : is_three_cycle g) :
+  is_three_cycle (g * g) :=
+begin
+  rw [←pow_two, ←card_support_eq_three_iff, support_pow_coprime, ht.card_support],
+  rw [ht.order_of, nat.coprime_iff_gcd_eq_one],
+  norm_num,
+end
+
 end is_three_cycle
 
 section
diff --git a/src/group_theory/specific_groups/alternating.lean b/src/group_theory/specific_groups/alternating.lean
index 16a471e661f0c..13d7ba2b53640 100644
--- a/src/group_theory/specific_groups/alternating.lean
+++ b/src/group_theory/specific_groups/alternating.lean
@@ -5,6 +5,7 @@ Authors: Aaron Anderson
 -/
 
 import group_theory.perm.fin
+import tactic.interval_cases
 
 /-!
 # Alternating Groups
@@ -21,7 +22,11 @@ consisting of the even permutations.
   the permutation group it is a subgroup of.
 
 * `closure_three_cycles_eq_alternating` shows that the alternating group is
-  generated by three-cycles.
+  generated by 3-cycles.
+
+* `alternating_group.is_simple_group_five` shows that the alternating group on `fin 5` is simple.
+  The proof shows that the normal closure of any non-identity element of this group contains a
+  3-cycle.
 
 ## Tags
 alternating group permutation
@@ -146,6 +151,8 @@ closure_eq_of_le _ (λ σ hσ, mem_alternating_group.2 hσ.sign) $ λ σ hσ, be
     (ih _ (λ g hg, hl g (list.mem_cons_of_mem _ (list.mem_cons_of_mem _ hg))) hn),
 end
 
+/-- A key lemma to prove $A_5$ is simple. Shows that any normal subgroup of an alternating group on
+  at least 5 elements is the entire alternating group if it contains a 3-cycle. -/
 lemma is_three_cycle.alternating_normal_closure (h5 : 5 ≤ fintype.card α)
   {f : perm α} (hf : is_three_cycle f) :
   normal_closure ({⟨f, hf.mem_alternating_group⟩} : set (alternating_group α)) = ⊤ :=
@@ -161,11 +168,45 @@ eq_top_iff.2 begin
   exact ⟨⟨f, hf.mem_alternating_group⟩, set.mem_singleton _, is_three_cycle_is_conj h5 hf h⟩
 end
 
+/-- Part of proving $A_5$ is simple. Shows that the square of any element of $A_5$ with a 3-cycle in
+  its cycle decomposition is a 3-cycle, so the normal closure of the original element must be
+  $A_5$. -/
+lemma is_three_cycle_sq_of_three_mem_cycle_type_five {g : perm (fin 5)} (h : 3 ∈ cycle_type g) :
+  is_three_cycle (g * g) :=
+begin
+  obtain ⟨c, g', rfl, hd, hc, h3⟩ := mem_cycle_type_iff.1 h,
+  simp only [mul_assoc],
+  rw [hd.mul_comm, ← mul_assoc g'],
+  suffices hg' : order_of g' ∣ 2,
+  { rw [← pow_two, order_of_dvd_iff_pow_eq_one.1 hg', one_mul],
+    exact (card_support_eq_three_iff.1 h3).is_three_cycle_sq },
+  rw [← lcm_cycle_type, multiset.lcm_dvd],
+  intros n hn,
+  rw le_antisymm (two_le_of_mem_cycle_type hn) (le_trans (le_card_support_of_mem_cycle_type hn) _),
+  apply le_of_add_le_add_left,
+  rw [← hd.card_support_mul, h3],
+  exact (c * g').support.card_le_univ,
+end
+
 end equiv.perm
 
 namespace alternating_group
 open equiv.perm
 
+lemma nontrivial_of_three_le_card (h3 : 3 ≤ card α) : nontrivial (alternating_group α) :=
+begin
+  haveI := fintype.one_lt_card_iff_nontrivial.1 (lt_trans dec_trivial h3),
+  rw ← fintype.one_lt_card_iff_nontrivial,
+  refine lt_of_mul_lt_mul_left _ (le_of_lt nat.prime_two.pos),
+  rw [two_mul_card_alternating_group, card_perm, ← nat.succ_le_iff],
+  exact le_trans h3 (card α).self_le_factorial,
+end
+
+instance {n : ℕ} : nontrivial (alternating_group (fin (n + 3))) :=
+nontrivial_of_three_le_card (by { rw card_fin, exact le_add_left (le_refl 3) })
+
+/-- The normal closure of the 5-cycle `fin_rotate 5` within $A_5$ is the whole group. This will be
+  used to show that the normal closure of any 5-cycle within $A_5$ is the whole group. -/
 lemma normal_closure_fin_rotate_five :
   (normal_closure ({⟨fin_rotate 5, fin_rotate_bit1_mem_alternating_group⟩} :
     set (alternating_group (fin 5)))) = ⊤ :=
@@ -182,4 +223,111 @@ eq_top_iff.2 begin
     ⟨fin.cycle_range 2, fin.is_three_cycle_cycle_range_two.mem_alternating_group⟩) (inv_mem _ h),
 end
 
+/-- The normal closure of $(04)(13)$ within $A_5$ is the whole group. This will be
+  used to show that the normal closure of any permutation of cycle type $(2,2)$ is the whole group.
+  -/
+lemma normal_closure_swap_mul_swap_five :
+  (normal_closure ({⟨swap 0 4 * swap 1 3, mem_alternating_group.2 dec_trivial⟩} :
+    set (alternating_group (fin 5)))) = ⊤ :=
+begin
+  let g1 := (⟨swap 0 2 * swap 0 1, mem_alternating_group.2 dec_trivial⟩ :
+    alternating_group (fin 5)),
+  let g2 := (⟨swap 0 4 * swap 1 3, mem_alternating_group.2 dec_trivial⟩ :
+    alternating_group (fin 5)),
+  have h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨fin_rotate 5, fin_rotate_bit1_mem_alternating_group⟩,
+  { rw subtype.ext_iff,
+    simp only [fin.coe_mk, subgroup.coe_mul, subgroup.coe_inv, fin.coe_mk],
+    dec_trivial },
+  rw [eq_top_iff, ← normal_closure_fin_rotate_five],
+  refine normal_closure_le_normal _,
+  rw [set.singleton_subset_iff, set_like.mem_coe, ← h5],
+  have h : g2 ∈ normal_closure {g2} :=
+    set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)),
+  exact mul_mem _ (subgroup.normal_closure_normal.conj_mem _ h g1) (inv_mem _ h),
+end
+
+/-- Shows that any non-identity element of $A_5$ whose cycle decomposition consists only of swaps
+  is conjugate to $(04)(13)$. This is used to show that the normal closure of such a permutation
+  in $A_5$ is $A_5$. -/
+lemma is_conj_swap_mul_swap_of_cycle_type_two {g : perm (fin 5)}
+  (ha : g ∈ alternating_group (fin 5))
+  (h1 : g ≠ 1)
+  (h2 : ∀ n, n ∈ cycle_type (g : perm (fin 5)) → n = 2) :
+  is_conj (swap 0 4 * swap 1 3) g :=
+begin
+  have h := g.support.card_le_univ,
+  rw [← sum_cycle_type, multiset.eq_repeat_of_mem h2, multiset.sum_repeat, smul_eq_mul] at h,
+  rw [← multiset.eq_repeat'] at h2,
+  have h56 : 5 ≤ 3 * 2 := nat.le_succ 5,
+  have h := le_of_mul_le_mul_right (le_trans h h56) dec_trivial,
+  rw [mem_alternating_group, sign_of_cycle_type, h2, multiset.map_repeat, multiset.prod_repeat,
+    int.units_pow_two, units.ext_iff, units.coe_one, units.coe_pow, units.coe_neg_one,
+      nat.neg_one_pow_eq_one_iff_even _] at ha,
+  swap, { dec_trivial },
+  rw [is_conj_iff_cycle_type_eq, h2],
+  interval_cases multiset.card g.cycle_type,
+  { exact (h1 (card_cycle_type_eq_zero.1 h_1)).elim },
+  { contrapose! ha,
+    simp [h_1] },
+  { have h04 : (0 : fin 5) ≠ 4 := dec_trivial,
+    have h13 : (1 : fin 5) ≠ 3 := dec_trivial,
+    rw [h_1, disjoint.cycle_type, (is_cycle_swap h04).cycle_type, (is_cycle_swap h13).cycle_type,
+      card_support_swap h04, card_support_swap h13],
+    { refl },
+    { rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13],
+      dec_trivial } },
+  { contrapose! ha,
+    simp [h_1] }
+end
+
+/-- Shows that $A_5$ is simple by taking an arbitrary non-identity element and showing by casework
+  on its cycle type that its normal closure is all of $A_5$.   -/
+instance is_simple_group_five : is_simple_group (alternating_group (fin 5)) :=
+⟨exists_pair_ne _, λ H, begin
+  introI Hn,
+  refine or_not.imp (id) (λ Hb, _),
+  rw [eq_bot_iff_forall] at Hb,
+  push_neg at Hb,
+  obtain ⟨⟨g, gA⟩, gH, g1⟩ : ∃ (x : ↥(alternating_group (fin 5))), x ∈ H ∧ x ≠ 1 := Hb,
+  -- `g` is a non-identity alternating permutation in a normal subgroup `H` of $A_5$.
+  rw [← set_like.mem_coe, ← set.singleton_subset_iff] at gH,
+  refine eq_top_iff.2 (le_trans (ge_of_eq _) (normal_closure_le_normal gH)),
+  -- It suffices to show that the normal closure of `g` in $A_5$ is $A_5$.
+  by_cases h2 : ∀ n ∈ g.cycle_type, n = 2,
+  { -- If the cycle decomposition of `g` consists entirely of swaps, then the cycle type is $(2,2)$.
+    -- This means that it is conjugate to $(04)(13)$, whose normal closure is $A_5$.
+    rw [ne.def, subtype.ext_iff] at g1,
+    exact (is_conj_swap_mul_swap_of_cycle_type_two gA g1 h2).normal_closure_eq_top_of
+      normal_closure_swap_mul_swap_five },
+  push_neg at h2,
+  obtain ⟨n, ng, n2⟩ : ∃ (n : ℕ), n ∈ g.cycle_type ∧ n ≠ 2 := h2,
+  -- `n` is the size of a non-swap cycle in the decomposition of `g`.
+  have n2' : 2 < n := lt_of_le_of_ne (two_le_of_mem_cycle_type ng) n2.symm,
+  have n5 : n ≤ 5 := le_trans _ g.support.card_le_univ,
+  -- We check that `2 < n ≤ 5`, so that `interval_cases` has a precise range to check.
+  swap, { obtain ⟨m, hm⟩ := multiset.exists_cons_of_mem ng,
+    rw [← sum_cycle_type, hm, multiset.sum_cons],
+    exact le_add_right (le_refl _) },
+  interval_cases n, -- This breaks into cases `n = 3`, `n = 4`, `n = 5`.
+  { -- If `n = 3`, then `g` has a 3-cycle in its decomposition, so `g^2` is a 3-cycle.
+    -- `g^2` is in the normal closure of `g`, so that normal closure must be $A_5$.
+    rw [eq_top_iff, ← (is_three_cycle_sq_of_three_mem_cycle_type_five ng).alternating_normal_closure
+      (by rw card_fin )],
+    refine normal_closure_le_normal _,
+    rw [set.singleton_subset_iff, set_like.mem_coe],
+    have h := set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)),
+    exact mul_mem _ h h },
+  { -- The case `n = 4` leads to contradiction, as no element of $A_5$ includes a 4-cycle.
+    have con := mem_alternating_group.1 gA,
+    contrapose! con,
+    rw [sign_of_cycle_type, cycle_type_of_card_le_mem_cycle_type_add_two dec_trivial ng],
+    simp only [multiset.singleton_eq_singleton, multiset.map_cons, mul_one, multiset.prod_cons,
+      units.neg_mul, multiset.prod_zero, multiset.map_zero],
+    dec_trivial },
+  { -- If `n = 5`, then `g` is itself a 5-cycle, conjugate to `fin_rotate 5`.
+    refine (is_conj_iff_cycle_type_eq.2 _).normal_closure_eq_top_of
+      normal_closure_fin_rotate_five,
+    rw [cycle_type_of_card_le_mem_cycle_type_add_two dec_trivial ng, cycle_type_fin_rotate] }
+end⟩
+
 end alternating_group
diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean
index fa8040e922605..b677c1320d4f0 100644
--- a/src/group_theory/subgroup.lean
+++ b/src/group_theory/subgroup.lean
@@ -1238,6 +1238,11 @@ def cod_restrict (f : G →* N) (S : subgroup N) (h : ∀ x, f x ∈ S) : G →*
   map_one' := subtype.eq f.map_one,
   map_mul' := λ x y, subtype.eq (f.map_mul x y) }
 
+@[simp, to_additive]
+lemma cod_restrict_apply {G : Type*} [group G] {N : Type*} [group N] (f : G →* N)
+  (S : subgroup N) (h : ∀ (x : G), f x ∈ S) {x : G} :
+    f.cod_restrict S h x = ⟨f x, h x⟩ := rfl
+
 /-- Computable alternative to `monoid_hom.of_injective`. -/
 def of_left_inverse {f : G →* N} {g : N →* G} (h : function.left_inverse g f) : G ≃* f.range :=
 { to_fun := f.range_restrict,
@@ -1823,6 +1828,37 @@ end subgroup
 
 end pointwise
 
+namespace is_conj
+open subgroup
+
+lemma normal_closure_eq_top_of {N : subgroup G} [hn : N.normal]
+  {g g' : G} {hg : g ∈ N} {hg' : g' ∈ N} (hc : is_conj g g')
+  (ht : normal_closure ({⟨g, hg⟩} : set N) = ⊤) :
+  normal_closure ({⟨g', hg'⟩} : set N) = ⊤ :=
+begin
+  obtain ⟨c, rfl⟩ := is_conj_iff.1 hc,
+  have h : ∀ x : N, (mul_aut.conj c) x ∈ N,
+  { rintro ⟨x, hx⟩,
+    exact hn.conj_mem _ hx c },
+  have hs : function.surjective (((mul_aut.conj c).to_monoid_hom.restrict N).cod_restrict _ h),
+  { rintro ⟨x, hx⟩,
+    refine ⟨⟨c⁻¹ * x * c, _⟩, _⟩,
+    { have h := hn.conj_mem _ hx c⁻¹,
+      rwa [inv_inv] at h },
+    simp only [monoid_hom.cod_restrict_apply, mul_equiv.coe_to_monoid_hom, mul_aut.conj_apply,
+      coe_mk, monoid_hom.restrict_apply, subtype.mk_eq_mk, ← mul_assoc, mul_inv_self, one_mul],
+    rw [mul_assoc, mul_inv_self, mul_one] },
+  have ht' := map_mono (eq_top_iff.1 ht),
+  rw [← monoid_hom.range_eq_map, monoid_hom.range_top_of_surjective _ hs] at ht',
+  refine eq_top_iff.2 (le_trans ht' (map_le_iff_le_comap.2 (normal_closure_le_normal _))),
+  rw [set.singleton_subset_iff, set_like.mem_coe],
+  simp only [monoid_hom.cod_restrict_apply, mul_equiv.coe_to_monoid_hom, mul_aut.conj_apply, coe_mk,
+    monoid_hom.restrict_apply, mem_comap],
+  exact subset_normal_closure (set.mem_singleton _),
+end
+
+end is_conj
+
 /-! ### Actions by `subgroup`s
 
 These are just copies of the definitions about `submonoid` starting from `submonoid.mul_action`.