From 318ec36d528e3f3c0ca7f43a0615d0116abf9c0f Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+dorhinj@users.noreply.github.com>
Date: Wed, 19 Sep 2018 10:24:25 +0100
Subject: [PATCH] feat(group_theory/perm): sign_cycle and sign_bij (#347)

---
 algebra/group_power.lean |  10 ++
 data/equiv/basic.lean    |   6 +-
 group_theory/perm.lean   | 319 ++++++++++++++++++++++++++++++++++++++-
 3 files changed, 327 insertions(+), 8 deletions(-)

diff --git a/algebra/group_power.lean b/algebra/group_power.lean
index 7a81e800387df..19fcd26a89a6e 100644
--- a/algebra/group_power.lean
+++ b/algebra/group_power.lean
@@ -442,3 +442,13 @@ by rw pow_two; exact mul_self_nonneg _
 theorem pow_ge_one_add_sub_mul [linear_ordered_ring α]
   {a : α} (H : a ≥ 1) (n : ℕ) : 1 + n • (a - 1) ≤ a ^ n :=
 by simpa using pow_ge_one_add_mul (sub_nonneg.2 H) n
+
+namespace int
+
+lemma units_pow_two (u : units ℤ) : u ^ 2 = 1 :=
+(units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
+
+lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :=
+by conv {to_lhs, rw ← nat.mod_add_div n 2}; simp [pow_add, pow_mul, units_pow_two]
+
+end int
\ No newline at end of file
diff --git a/data/equiv/basic.lean b/data/equiv/basic.lean
index a9f5481bca296..5f0d9d40b5af5 100644
--- a/data/equiv/basic.lean
+++ b/data/equiv/basic.lean
@@ -612,16 +612,16 @@ eq_of_to_fun_eq $ funext $ λ r, swap_core_comm r _ _
 theorem swap_apply_def (a b x : α) : swap a b x = if x = a then b else if x = b then a else x :=
 rfl
 
-theorem swap_apply_left (a b : α) : swap a b a = b :=
+@[simp] theorem swap_apply_left (a b : α) : swap a b a = b :=
 if_pos rfl
 
-theorem swap_apply_right (a b : α) : swap a b b = a :=
+@[simp] theorem swap_apply_right (a b : α) : swap a b b = a :=
 by by_cases b = a; simp [swap_apply_def, *]
 
 theorem swap_apply_of_ne_of_ne {a b x : α} : x ≠ a → x ≠ b → swap a b x = x :=
 by simp [swap_apply_def] {contextual := tt}
 
-theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = equiv.refl _ :=
+@[simp] theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = equiv.refl _ :=
 eq_of_to_fun_eq $ funext $ λ x, swap_core_swap_core _ _ _
 
 theorem swap_comp_apply {a b x : α} (π : perm α) :
diff --git a/group_theory/perm.lean b/group_theory/perm.lean
index 9ecbe315ca785..4dc0fc5b9b5fb 100644
--- a/group_theory/perm.lean
+++ b/group_theory/perm.lean
@@ -7,12 +7,113 @@ import data.fintype
 
 universes u v
 open equiv function finset fintype
-variables {α : Type u} {β : Type v} [decidable_eq α]
+variables {α : Type u} {β : Type v}
 
 namespace equiv.perm
 
+def subtype_perm (f : perm α) {p : α → Prop} (h : ∀ x, p x ↔ p (f x)) : perm {x // p x} :=
+⟨λ x, ⟨f x, (h _).1 x.2⟩, λ x, ⟨f⁻¹ x, (h (f⁻¹ x)).2 $ by simpa using x.2⟩,
+  λ _, by simp, λ _, by simp⟩
+
+def of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) : perm α :=
+⟨λ x, if h : p x then f ⟨x, h⟩ else x, λ x, if h : p x then f⁻¹ ⟨x, h⟩ else x,
+  λ x, have h : ∀ h : p x, p (f ⟨x, h⟩), from λ h, (f ⟨x, h⟩).2,
+    by simp; split_ifs at *; simp * at *,
+  λ x, have h : ∀ h : p x, p (f⁻¹ ⟨x, h⟩), from λ h, (f⁻¹ ⟨x, h⟩).2,
+    by simp; split_ifs at *; simp * at *⟩
+
+instance of_subtype.is_group_hom {p : α → Prop} [decidable_pred p] : is_group_hom (@of_subtype α p _) :=
+⟨λ f g, equiv.ext _ _ $ λ x, begin
+  rw [of_subtype, of_subtype, of_subtype],
+  by_cases h : p x,
+  { have h₁ : p (f (g ⟨x, h⟩)), from (f (g ⟨x, h⟩)).2,
+    have h₂ : p (g ⟨x, h⟩), from (g ⟨x, h⟩).2,
+    simp [h, h₁, h₂] },
+  { simp [h] }
+end⟩
+
+lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y :=
+by conv {to_lhs, rw [← injective.eq_iff f.bijective.1, apply_inv_self]}
+
+lemma inv_eq_iff_eq {f : perm α} {x y : α} : f⁻¹ x = y ↔ x = f y :=
+by rw [eq_comm, eq_inv_iff_eq, eq_comm]
+
+def is_cycle (f : perm α) := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y
+
+lemma exists_int_pow_eq_of_is_cycle {f : perm α} (hf : is_cycle f) {x y : α}
+  (hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℤ, (f ^ i) x = y :=
+let ⟨g, hg⟩ := hf in
+let ⟨a, ha⟩ := hg.2 x hx in
+let ⟨b, hb⟩ := hg.2 y hy in
+⟨b - a, by rw [← ha, ← mul_apply, ← gpow_add, sub_add_cancel, hb]⟩
+
+lemma of_subtype_subtype_perm {f : perm α} {p : α → Prop} [decidable_pred p] (h₁ : ∀ x, p x ↔ p (f x))
+  (h₂ : ∀ x, f x ≠ x → p x) : of_subtype (subtype_perm f h₁) = f :=
+equiv.ext _ _ $ λ x, begin
+  rw [of_subtype, subtype_perm],
+  by_cases hx : p x,
+  { simp [hx] },
+  { haveI := classical.prop_decidable,
+    simp [hx, not_not.1 (mt (h₂ x) hx)] }
+end
+
+lemma of_subtype_apply_of_not_mem {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) {x : α} (hx : ¬ p x) :
+  of_subtype f x = x := dif_neg hx
+
+lemma mem_iff_of_subtype_apply_mem {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) (x : α) :
+  p x ↔ p ((of_subtype f : α → α) x) :=
+if h : p x then by dsimp [of_subtype]; simpa [h] using (f ⟨x, h⟩).2
+else by simp [h, of_subtype_apply_of_not_mem f h]
+
+@[simp] lemma subtype_perm_of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) :
+  subtype_perm (of_subtype f) (mem_iff_of_subtype_apply_mem f) = f :=
+equiv.ext _ _ $ λ ⟨x, hx⟩, by dsimp [subtype_perm, of_subtype]; simp [show p x, from hx]
+
+lemma pow_apply_eq_of_apply_apply_eq_self_nat {f : perm α} {x : α} (hffx : f (f x) = x) :
+  ∀ n : ℕ, (f ^ n) x = x ∨ (f ^ n) x = f x
+| 0     := or.inl rfl
+| (n+1) := (pow_apply_eq_of_apply_apply_eq_self_nat n).elim
+  (λ h, or.inr (by rw [pow_succ, mul_apply, h]))
+  (λ h, or.inl (by rw [pow_succ, mul_apply, h, hffx]))
+
+lemma pow_apply_eq_of_apply_apply_eq_self_int {f : perm α} {x : α} (hffx : f (f x) = x) :
+  ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x
+| (n : ℕ) := pow_apply_eq_of_apply_apply_eq_self_nat hffx n
+| -[1+ n] :=
+  by rw [gpow_neg_succ, inv_eq_iff_eq, ← injective.eq_iff f.bijective.1, ← mul_apply, ← pow_succ,
+    eq_comm, inv_eq_iff_eq, ← mul_apply, ← pow_succ', @eq_comm _ x, or.comm];
+  exact pow_apply_eq_of_apply_apply_eq_self_nat hffx _
+
+variable [decidable_eq α]
+
+def support [fintype α] (f : perm α) := univ.filter (λ x, f x ≠ x)
+
+@[simp] lemma mem_support [fintype α] {f : perm α} {x : α} : x ∈ f.support ↔ f x ≠ x :=
+by simp [support]
+
 def is_swap (f : perm α) := ∃ x y, x ≠ y ∧ f = swap x y
 
+lemma swap_mul_eq_mul_swap (f : perm α) (x y : α) : swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y) :=
+equiv.ext _ _ $ λ z, begin
+  simp [mul_apply, swap_apply_def],
+  split_ifs;
+  simp [*, eq_inv_iff_eq] at * <|> cc
+end
+
+lemma mul_swap_eq_swap_mul (f : perm α) (x y : α) : f * swap x y = swap (f x) (f y) * f :=
+by rw [swap_mul_eq_mul_swap, inv_apply_self, inv_apply_self]
+
+lemma is_swap_of_subtype {p : α → Prop} [decidable_pred p]
+  {f : perm (subtype p)} (h : is_swap f) : is_swap (of_subtype f) :=
+let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h in
+⟨x, y, by simp at hxy; tauto,
+  equiv.ext _ _ $ λ z, begin
+    rw [hxy.2, of_subtype],
+    simp [swap_apply_def],
+    split_ifs;
+    cc <|> simp * at *
+  end⟩
+
 lemma support_swap_mul {f : perm α} {x : α}
   {y : α} (hy : (swap x (f x) * f) y ≠ y) : f y ≠ y ∧ y ≠ x :=
 begin
@@ -261,12 +362,44 @@ def sign [fintype α] (f : perm α) := sign_aux3 f mem_univ
 instance sign.is_group_hom [fintype α] : is_group_hom (@sign α _ _) :=
 ⟨λ f g, (sign_aux3_mul_and_swap f g _ mem_univ).1⟩
 
+@[simp] lemma sign_mul [fintype α] (f g : perm α) : sign (f * g) = sign f * sign g :=
+is_group_hom.mul sign _ _
+
+@[simp] lemma sign_one [fintype α] : (sign (1 : perm α)) = 1 :=
+is_group_hom.one sign
+
+@[simp] lemma sign_inv [fintype α] (f : perm α) : sign f⁻¹ = sign f :=
+by rw [is_group_hom.inv sign, int.units_inv_eq_self]; apply_instance
+
 lemma sign_swap [fintype α] {x y : α} (h : x ≠ y) : sign (swap x y) = -1 :=
 (sign_aux3_mul_and_swap 1 1 _ mem_univ).2 x y h
 
 lemma sign_eq_of_is_swap [fintype α] {f : perm α} (h : is_swap f) : sign f = -1 :=
 let ⟨x, y, hxy⟩ := h in hxy.2.symm ▸ sign_swap hxy.1
 
+lemma sign_aux3_symm_trans_trans [fintype α] [decidable_eq β] [fintype β] (f : perm α)
+  (e : α ≃ β) {s : multiset α} {t : multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
+  sign_aux3 ((e.symm.trans f).trans e) ht = sign_aux3 f hs :=
+quotient.induction_on₂ t s
+  (λ l₁ l₂ h₁ h₂, show sign_aux2 _ _ = sign_aux2 _ _,
+    from let n := trunc.out (equiv_fin β) in
+    by rw [← sign_aux_eq_sign_aux2 _ _ n (λ _ _, h₁ _),
+        ← sign_aux_eq_sign_aux2 _ _ (e.trans n) (λ _ _, h₂ _)];
+      exact congr_arg sign_aux (equiv.ext _ _ (λ x, by simp)))
+  ht hs
+
+lemma sign_symm_trans_trans [fintype α] [decidable_eq β] [fintype β] (f : perm α)
+  (e : α ≃ β) : sign ((e.symm.trans f).trans e) = sign f :=
+sign_aux3_symm_trans_trans f e mem_univ mem_univ
+
+lemma sign_prod_list_swap [fintype α] {l : list (perm α)}
+  (hl : ∀ g ∈ l, is_swap g) : sign l.prod = -1 ^ l.length :=
+have h₁ : l.map sign = list.repeat (-1) l.length :=
+  list.eq_repeat.2 ⟨by simp, λ u hu,
+  let ⟨g, hg⟩ := list.mem_map.1 hu in
+  hg.2 ▸ sign_eq_of_is_swap (hl _ hg.1)⟩,
+by rw [← list.prod_repeat, ← h₁, ← is_group_hom.prod (@sign α _ _)]
+
 lemma eq_sign_of_surjective_hom [fintype α] {s : perm α → units ℤ}
   [is_group_hom s] (hs : surjective s) : s = sign :=
 have ∀ {f}, is_swap f → s f = -1 :=
@@ -286,9 +419,185 @@ funext $ λ f,
 let ⟨l, hl₁, hl₂⟩ := trunc.out (trunc_swap_factors f) in
 have hsl : ∀ a ∈ l.map s, a = (-1 : units ℤ) := λ a ha,
   let ⟨g, hg⟩ := list.mem_map.1 ha in hg.2 ▸  this (hl₂ _ hg.1),
-have hsignl :  ∀ a ∈ l.map sign, a = (-1 : units ℤ) := λ a ha,
-  let ⟨g, hg⟩ := list.mem_map.1 ha in hg.2 ▸ sign_eq_of_is_swap (hl₂ _ hg.1),
-by rw [← hl₁, is_group_hom.prod s, is_group_hom.prod (@sign α _ _),
-  list.eq_repeat'.2 hsl, list.eq_repeat'.2 hsignl, list.length_map, list.length_map]
+by rw [← hl₁, is_group_hom.prod s, list.eq_repeat'.2 hsl, list.length_map,
+     list.prod_repeat, sign_prod_list_swap hl₂]
+
+lemma sign_subtype_perm [fintype α] (f : perm α) {p : α → Prop} [decidable_pred p]
+  (h₁ : ∀ x, p x ↔ p (f x)) (h₂ : ∀ x, f x ≠ x → p x) : sign (subtype_perm f h₁) = sign f :=
+let l := trunc.out (trunc_swap_factors (subtype_perm f h₁)) in
+have hl' : ∀ g' ∈ l.1.map of_subtype, is_swap g' :=
+  λ g' hg',
+  let ⟨g, hg⟩ := list.mem_map.1 hg' in
+  hg.2 ▸ is_swap_of_subtype (l.2.2 _ hg.1),
+have hl'₂ : (l.1.map of_subtype).prod = f,
+  by rw [← is_group_hom.prod of_subtype l.1, l.2.1, of_subtype_subtype_perm _ h₂],
+by conv {congr, rw ← l.2.1, skip, rw ← hl'₂};
+  rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', list.length_map]
+
+@[simp] lemma sign_of_subtype [fintype α] {p : α → Prop} [decidable_pred p]
+  (f : perm (subtype p)) : sign (of_subtype f) = sign f :=
+have ∀ x, of_subtype f x ≠ x → p x, from λ x, not_imp_comm.1 (of_subtype_apply_of_not_mem f),
+by conv {to_rhs, rw [← subtype_perm_of_subtype f, sign_subtype_perm _ _ this]}
+
+lemma sign_eq_sign_of_equiv [fintype α] [decidable_eq β] [fintype β] (f : perm α) (g : perm β)
+  (e : α ≃ β) (h : ∀ x, e (f x) = g (e x)) : sign f = sign g :=
+have hg : g = (e.symm.trans f).trans e, from equiv.ext _ _ $ by simp [h],
+by rw [hg, sign_symm_trans_trans]
+
+lemma sign_bij [fintype α] [decidable_eq β] [fintype β]
+  {f : perm α} {g : perm β} (i : Π x : α, f x ≠ x → β)
+  (h : ∀ x hx hx', i (f x) hx' = g (i x hx))
+  (hi : ∀ x₁ x₂ hx₁ hx₂, i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂)
+  (hg : ∀ y, g y ≠ y → ∃ x hx, i x hx = y) :
+  sign f = sign g :=
+calc sign f = sign (@subtype_perm _ f (λ x, f x ≠ x) (by simp)) :
+  eq.symm (sign_subtype_perm _ _ (λ _, id))
+... = sign (@subtype_perm _ g (λ x, g x ≠ x) (by simp)) :
+  sign_eq_sign_of_equiv _ _
+    (equiv.of_bijective
+      (show function.bijective (λ x : {x // f x ≠ x},
+        (⟨i x.1 x.2, have f (f x) ≠ f x, from mt (λ h, f.bijective.1 h) x.2,
+          by rw [← h _ x.2 this]; exact mt (hi _ _ this x.2) x.2⟩ : {y // g y ≠ y})),
+        from ⟨λ ⟨x, hx⟩ ⟨y, hy⟩ h, subtype.eq (hi _ _ _ _ (subtype.mk.inj h)),
+          λ ⟨y, hy⟩, let ⟨x, hfx, hx⟩ := hg y hy in ⟨⟨x, hfx⟩, subtype.eq hx⟩⟩))
+      (λ ⟨x, _⟩, subtype.eq (h x _ _))
+... = sign g : sign_subtype_perm _ _ (λ _, id)
+
+lemma is_cycle_swap {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
+⟨y, by rwa swap_apply_right,
+  λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
+    if hya : y = a then ⟨0, hya⟩
+    else ⟨1, by rw [gpow_one, swap_apply_def]; split_ifs at *; cc⟩⟩
+
+lemma is_cycle_inv {f : perm α} (hf : is_cycle f) : is_cycle (f⁻¹) :=
+let ⟨x, hx⟩ := hf in
+⟨x, by simp [eq_inv_iff_eq, inv_eq_iff_eq, *] at *; cc,
+  λ y hy, let ⟨i, hi⟩ := hx.2 y (by simp [eq_inv_iff_eq, inv_eq_iff_eq, *] at *; cc) in
+    ⟨-i, by rwa [gpow_neg, inv_gpow, inv_inv]⟩⟩
+
+lemma is_cycle_swap_mul_aux₁ : ∀ (n : ℕ) {b x : α} {f : perm α}
+  (hf : is_cycle f) (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
+  ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
+| 0         := λ b x f hf hb h, ⟨0, h⟩
+| (n+1 : ℕ) := λ b x f hf hb h,
+  if hfbx : f x = b then ⟨0, hfbx⟩
+  else
+    have f b ≠ b ∧ b ≠ x, from support_swap_mul hb,
+    have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b,
+      by rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx),
+          ne.def, ← injective.eq_iff f.bijective.1, apply_inv_self];
+        exact this.1,
+    let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hf hb'
+      (f.bijective.1 $
+        by rw [apply_inv_self];
+        rwa [pow_succ, mul_apply] at h) in
+    ⟨i + 1, by rw [add_comm, gpow_add, mul_apply, hi, gpow_one, mul_apply, apply_inv_self,
+        swap_apply_of_ne_of_ne (support_swap_mul hb).2 (ne.symm hfbx)]⟩
+
+lemma is_cycle_swap_mul_aux₂ : ∀ (n : ℤ) {b x : α} {f : perm α}
+  (hf : is_cycle f) (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
+  ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
+| (n : ℕ) := λ b x f hf, is_cycle_swap_mul_aux₁ n hf
+| -[1+ n] := λ b x f hf hb h,
+  if hfbx : f⁻¹ x = b then ⟨-1, by rwa [gpow_neg, gpow_one, mul_inv_rev, mul_apply, swap_inv, swap_apply_right]⟩
+  else if hfbx' : f x = b then ⟨0, hfbx'⟩
+  else
+  have f b ≠ b ∧ b ≠ x := support_swap_mul hb,
+  have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b,
+    by rw [mul_apply, swap_apply_def];
+      split_ifs;
+      simp [inv_eq_iff_eq, eq_inv_iff_eq] at *; cc,
+  let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n (is_cycle_inv hf) hb
+    (show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b, by
+      rw [← gpow_coe_nat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, gpow_neg_succ, ← inv_pow, pow_succ', mul_assoc,
+        mul_assoc, inv_mul_self, mul_one, gpow_coe_nat, ← pow_succ', ← pow_succ]) in
+  have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x, by rw [mul_apply, inv_apply_self, swap_apply_left],
+  ⟨-i, by rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, gpow_add, gpow_one, gpow_neg, ← inv_gpow,
+      mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x, gpow_add, gpow_one,
+      mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx')]⟩
+
+lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {f : perm α} (hf : is_cycle f) {x : α}
+  (hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
+equiv.ext _ _ $ λ y,
+let ⟨z, hz⟩ := hf in
+let ⟨i, hi⟩ := hz.2 x hfx in
+if hyx : y = x then by simp [hyx]
+else if hfyx : y = f x then by simp [hfyx, hffx]
+else begin
+  rw [swap_apply_of_ne_of_ne hyx hfyx],
+  refine by_contradiction (λ hy, _),
+  cases hz.2 y hy with j hj,
+  rw [← sub_add_cancel j i, gpow_add, mul_apply, hi] at hj,
+  cases pow_apply_eq_of_apply_apply_eq_self_int hffx (j - i) with hji hji,
+  { rw [← hj, hji] at hyx, cc },
+  { rw [← hj, hji] at hfyx, cc }
+end
+
+lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
+  (hx : f x ≠ x) (hffx : f (f x) ≠ x) : is_cycle (swap x (f x) * f) :=
+⟨f x, by simp only [swap_apply_def, mul_apply];
+        split_ifs; simp [injective.eq_iff f.bijective.1] at *; cc,
+  λ y hy,
+  let ⟨i, hi⟩ := exists_int_pow_eq_of_is_cycle hf hx (support_swap_mul hy).1 in
+  have hi : (f ^ (i - 1)) (f x) = y, from
+    calc (f ^ (i - 1)) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ)) x : by rw [gpow_one, mul_apply]
+    ... =  y : by rwa [← gpow_add, sub_add_cancel],
+  is_cycle_swap_mul_aux₂ (i - 1) hf hy hi⟩
+
+lemma support_swap_mul_cycle [fintype α] {f : perm α} (hf : is_cycle f) {x : α}
+  (hx : f x ≠ x) (hffx : f (f x) ≠ x) : (swap x (f x) * f).support = f.support.erase x :=
+finset.ext.2 $ λ y, begin
+  have h1 : swap x (f x) * f ≠ 1,
+    from λ h1, hffx $ by
+      rw [mul_eq_one_iff_inv_eq, swap_inv] at h1;
+      rw ← h1; simp,
+  have hfyxor : f y ≠ x ∨ f x ≠ y :=
+    not_and_distrib.1 (λ h, h1 $
+      by have := eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx (by rw [h.2, h.1]);
+      rw [← this, this, mul_def, swap_swap, one_def]),
+  rw [mem_support, mem_erase, mem_support],
+  split,
+  { assume h,
+    refine not_or_distrib.1 (λ h₁, h₁.elim
+      (λ hyx, by simpa [hyx, mul_apply] using h) _),
+    assume hfy,
+    have hyx : x ≠ y := λ h, by rw h at hx; tauto,
+    have hfyx : f x ≠ y := by rwa [← hfy, ne.def, injective.eq_iff f.bijective.1],
+    simpa [mul_apply, hfy, swap_apply_of_ne_of_ne hyx.symm hfyx.symm] using h },
+  { assume h,
+    simp [swap_apply_def],
+    split_ifs; cc }
+end
+
+@[simp] lemma support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
+finset.ext.2 $ λ a, by simp [swap_apply_def]; split_ifs; cc
+
+lemma card_support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
+show (swap x y).support.card = finset.card ⟨x::y::0, by simp [hxy]⟩,
+from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext]; cc
+
+lemma sign_cycle [fintype α] : ∀ {f : perm α} (hf : is_cycle f),
+  sign f = -(-1 ^ f.support.card)
+| f := λ hf,
+let ⟨x, hx⟩ := hf in
+calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
+  by rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]
+... = -(-1 ^ f.support.card) :
+  if h1 : f (f x) = x
+  then
+    have h : swap x (f x) * f = 1,
+      by conv in (f) {rw eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1 };
+        simp [mul_def, one_def],
+    by rw [sign_mul, sign_swap hx.1.symm, h, sign_one, eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1,
+        card_support_swap hx.1.symm]; refl
+  else
+    have h : card (support (swap x (f x) * f)) + 1 = card (support f),
+      by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_cycle hf hx.1 h1,
+        card_insert_of_not_mem (not_mem_erase _ _)],
+    have wf : card (support (swap x (f x) * f)) < card (support f),
+      from h ▸ nat.lt_succ_self _,
+    by rw [sign_mul, sign_swap hx.1.symm, sign_cycle (is_cycle_swap_mul hf hx.1 h1), ← h];
+      simp [pow_add]
+using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
 
 end equiv.perm
\ No newline at end of file