diff --git a/src/data/set/function.lean b/src/data/set/function.lean
index b51f2b6bb7f0e..ad181e2038170 100644
--- a/src/data/set/function.lean
+++ b/src/data/set/function.lean
@@ -1449,6 +1449,12 @@ lemma inv_on : inv_on e e.symm t s :=
 lemma bij_on_image : bij_on e s (e '' s) := (e.injective.inj_on _).bij_on_image
 lemma bij_on_symm_image : bij_on e.symm (e '' s) s := e.bij_on_image.symm e.inv_on
 
+variables {e}
+
+@[simp] lemma bij_on_symm : bij_on e.symm t s ↔ bij_on e s t := bij_on_comm e.symm.inv_on
+
+alias bij_on_symm ↔ _root_.set.bij_on.of_equiv_symm _root_.set.bij_on.equiv_symm
+
 variables [decidable_eq α] {a b : α}
 
 lemma bij_on_swap (ha : a ∈ s) (hb : b ∈ s) : bij_on (swap a b) s s :=
diff --git a/src/dynamics/fixed_points/basic.lean b/src/dynamics/fixed_points/basic.lean
index 2520af1f44024..d5eda405f92dc 100644
--- a/src/dynamics/fixed_points/basic.lean
+++ b/src/dynamics/fixed_points/basic.lean
@@ -87,7 +87,7 @@ h.to_left_inverse e.left_inverse_symm
 protected lemma perm_inv (h : is_fixed_pt e x) : is_fixed_pt ⇑(e⁻¹) x := h.equiv_symm
 
 protected lemma perm_pow (h : is_fixed_pt e x) (n : ℕ) : is_fixed_pt ⇑(e ^ n) x :=
-by { rw ←equiv.perm.iterate_eq_pow, exact h.iterate _ }
+by { rw equiv.perm.coe_pow, exact h.iterate _ }
 
 protected lemma perm_zpow (h : is_fixed_pt e x) : ∀ n : ℤ, is_fixed_pt ⇑(e ^ n) x
 | (int.of_nat n) := h.perm_pow _
diff --git a/src/group_theory/perm/basic.lean b/src/group_theory/perm/basic.lean
index 7ae9350c243e3..0f6b7a4f8c9ab 100644
--- a/src/group_theory/perm/basic.lean
+++ b/src/group_theory/perm/basic.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 import algebra.group.pi
 import algebra.group.prod
 import algebra.hom.iterate
+import logic.equiv.set
 
 /-!
 # The group of permutations (self-equivalences) of a type `α`
@@ -67,9 +68,9 @@ lemma inv_def (f : perm α) : f⁻¹ = f.symm := rfl
 
 @[simp, norm_cast] lemma coe_one : ⇑(1 : perm α) = id := rfl
 @[simp, norm_cast] lemma coe_mul (f g : perm α) : ⇑(f * g) = f ∘ g := rfl
-
 @[norm_cast] lemma coe_pow (f : perm α) (n : ℕ) : ⇑(f ^ n) = (f^[n]) :=
 hom_coe_pow _ rfl (λ _ _, rfl) _ _
+@[simp] lemma iterate_eq_pow (f : perm α) (n : ℕ) : (f^[n]) = ⇑(f ^ n) := (coe_pow _ _).symm
 
 lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y := f.eq_symm_apply
 
@@ -79,9 +80,9 @@ lemma zpow_apply_comm {α : Type*} (σ : perm α) (m n : ℤ) {x : α} :
   (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x) :=
 by rw [←equiv.perm.mul_apply, ←equiv.perm.mul_apply, zpow_mul_comm]
 
-@[simp] lemma iterate_eq_pow (f : perm α) : ∀ n, f^[n] = ⇑(f ^ n)
-| 0       := rfl
-| (n + 1) := by { rw [function.iterate_succ, pow_add, iterate_eq_pow], refl }
+@[simp] lemma image_inv (f : perm α) (s : set α) : ⇑f⁻¹ '' s = f ⁻¹' s := f⁻¹.image_eq_preimage _
+@[simp] lemma preimage_inv (f : perm α) (s : set α) : ⇑f⁻¹ ⁻¹' s = f '' s :=
+(f.image_eq_preimage _).symm
 
 /-! Lemmas about mixing `perm` with `equiv`. Because we have multiple ways to express
 `equiv.refl`, `equiv.symm`, and `equiv.trans`, we want simp lemmas for every combination.
@@ -494,3 +495,25 @@ lemma zpow_mul_right : ∀ n : ℤ, equiv.mul_right a ^ n = equiv.mul_right (a ^
 
 end group
 end equiv
+
+open equiv function
+
+namespace set
+variables {α : Type*} {f : perm α} {s t : set α}
+
+@[simp] lemma bij_on_perm_inv : bij_on ⇑f⁻¹ t s ↔ bij_on f s t := equiv.bij_on_symm
+
+alias bij_on_perm_inv ↔ bij_on.of_perm_inv bij_on.perm_inv
+
+lemma maps_to.perm_pow : maps_to f s s → ∀ n : ℕ, maps_to ⇑(f ^ n) s s :=
+by { simp_rw equiv.perm.coe_pow, exact maps_to.iterate }
+lemma surj_on.perm_pow : surj_on f s s → ∀ n : ℕ, surj_on ⇑(f ^ n) s s :=
+by { simp_rw equiv.perm.coe_pow, exact surj_on.iterate }
+lemma bij_on.perm_pow : bij_on f s s → ∀ n : ℕ, bij_on ⇑(f ^ n) s s :=
+by { simp_rw equiv.perm.coe_pow, exact bij_on.iterate }
+
+lemma bij_on.perm_zpow (hf : bij_on f s s) : ∀ n : ℤ, bij_on ⇑(f ^ n) s s
+| (int.of_nat n) := hf.perm_pow _
+| (int.neg_succ_of_nat n) := by { rw zpow_neg_succ_of_nat, exact (hf.perm_pow _).perm_inv }
+
+end set
diff --git a/src/group_theory/perm/cycle/basic.lean b/src/group_theory/perm/cycle/basic.lean
index c0860c622aa6d..caa1530b9dcef 100644
--- a/src/group_theory/perm/cycle/basic.lean
+++ b/src/group_theory/perm/cycle/basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes
+Authors: Chris Hughes, Yaël Dillies
 -/
 import data.finset.noncomm_prod
 import data.fintype.perm
@@ -11,13 +11,17 @@ import logic.equiv.fintype
 /-!
 # Cyclic permutations
 
+This file develops the theory of cycles in permutations.
+
 ## Main definitions
 
 In the following, `f : equiv.perm β`.
 
 * `equiv.perm.same_cycle`: `f.same_cycle x y` when `x` and `y` are in the same cycle of `f`.
-* `equiv.perm.is_cycle`: `f.is_cycle` when two nonfixed points of `β`
-  are related by repeated application of `f`.
+* `equiv.perm.is_cycle`: `f` is a cycle if any two nonfixed points of `f` are related by repeated
+  applications of `f`, and `f` is not the identity.
+* `equiv.perm.is_cycle_on`: `f` is a cycle on a set `s` when any two points of `s` are related by
+  repeated applications of `f`.
 
 The following two definitions require that `β` is a `fintype`:
 
@@ -36,6 +40,12 @@ The following two definitions require that `β` is a `fintype`:
   - `closure_prime_cycle_swap` : The symmetric group is generated by
     a prime cycle and a transposition
 
+## Notes
+
+`equiv.perm.is_cycle` and `equiv.perm.is_cycle_on` are different in three ways:
+* `is_cycle` is about the entire type while `is_cycle_on` is restricted to a set.
+* `is_cycle` forbids the identity while `is_cycle_on` allows it (if `s` is a subsingleton).
+* `is_cycle_on` forbids fixed points on `s` (if `s` is nontrivial), while `is_cycle` allows them.
 -/
 
 open equiv function finset
@@ -100,22 +110,26 @@ by rw [←same_cycle_apply_left, apply_inv_self]
 @[simp] lemma same_cycle_inv_apply_right : same_cycle f x (f⁻¹ y) ↔ same_cycle f x y :=
 by rw [←same_cycle_apply_right, apply_inv_self]
 
-@[simp] lemma same_cycle_zpow_left_iff {n : ℤ} : same_cycle f ((f ^ n) x) y ↔ same_cycle f x y :=
+@[simp] lemma same_cycle_zpow_left {n : ℤ} : same_cycle f ((f ^ n) x) y ↔ same_cycle f x y :=
 (equiv.add_right (n : ℤ)).exists_congr_left.trans $ by simp [same_cycle, zpow_add]
 
-@[simp] lemma same_cycle_zpow_right_iff {n : ℤ} : same_cycle f x ((f ^ n) y) ↔ same_cycle f x y :=
-by rw [same_cycle_comm, same_cycle_zpow_left_iff, same_cycle_comm]
+@[simp] lemma same_cycle_zpow_right {n : ℤ} : same_cycle f x ((f ^ n) y) ↔ same_cycle f x y :=
+by rw [same_cycle_comm, same_cycle_zpow_left, same_cycle_comm]
 
-@[simp] lemma same_cycle_pow_left_iff {n : ℕ} : same_cycle f ((f ^ n) x) y ↔ same_cycle f x y :=
-by rw [←zpow_coe_nat, same_cycle_zpow_left_iff]
+@[simp] lemma same_cycle_pow_left {n : ℕ} : same_cycle f ((f ^ n) x) y ↔ same_cycle f x y :=
+by rw [←zpow_coe_nat, same_cycle_zpow_left]
 
-@[simp] lemma same_cycle_pow_right_iff {n : ℕ} : same_cycle f x ((f ^ n) y) ↔ same_cycle f x y :=
-by rw [←zpow_coe_nat, same_cycle_zpow_right_iff]
+@[simp] lemma same_cycle_pow_right {n : ℕ} : same_cycle f x ((f ^ n) y) ↔ same_cycle f x y :=
+by rw [←zpow_coe_nat, same_cycle_zpow_right]
 
-alias same_cycle_pow_left_iff ↔ _ same_cycle.pow_left
-alias same_cycle_pow_right_iff ↔ _ same_cycle.pow_right
-alias same_cycle_zpow_left_iff ↔ _ same_cycle.zpow_left
-alias same_cycle_zpow_right_iff ↔ _ same_cycle.zpow_right
+alias same_cycle_apply_left ↔ same_cycle.of_apply_left same_cycle.apply_left
+alias same_cycle_apply_right ↔ same_cycle.of_apply_right same_cycle.apply_right
+alias same_cycle_inv_apply_left ↔ same_cycle.of_inv_apply_left same_cycle.inv_apply_left
+alias same_cycle_inv_apply_right ↔ same_cycle.of_inv_apply_right same_cycle.inv_apply_right
+alias same_cycle_pow_left ↔ same_cycle.of_pow_left same_cycle.pow_left
+alias same_cycle_pow_right ↔ same_cycle.of_pow_right same_cycle.pow_right
+alias same_cycle_zpow_left ↔ same_cycle.of_zpow_left same_cycle.zpow_left
+alias same_cycle_zpow_right ↔ same_cycle.of_zpow_right same_cycle.zpow_right
 
 lemma same_cycle.of_pow {n : ℕ} : same_cycle (f ^ n) x y → same_cycle f x y :=
 λ ⟨m, h⟩, ⟨n * m, by simp [zpow_mul, h]⟩
@@ -136,7 +150,7 @@ exists_congr $ λ n, by rw [←extend_domain_zpow, extend_domain_apply_image, su
 
 alias same_cycle_extend_domain ↔ _ same_cycle.extend_domain
 
-lemma same_cycle.nat' [finite α] : same_cycle f x y → ∃ i < order_of f, (f ^ i) x = y :=
+lemma same_cycle.exists_pow_eq' [finite α] : same_cycle f x y → ∃ i < order_of f, (f ^ i) x = y :=
 begin
   classical,
   rintro ⟨k, rfl⟩,
@@ -149,11 +163,11 @@ begin
   exact int.mod_lt_of_pos _ h₀,
 end
 
-lemma same_cycle.nat'' [finite α] (h : same_cycle f x y) :
+lemma same_cycle.exists_pow_eq'' [finite α] (h : same_cycle f x y) :
   ∃ (i : ℕ) (hpos : 0 < i) (h : i ≤ order_of f), (f ^ i) x = y :=
 begin
   classical,
-  obtain ⟨_|i, hi, rfl⟩ := h.nat',
+  obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq',
   { refine ⟨order_of f, order_of_pos f, le_rfl, _⟩,
     rw [pow_order_of_eq_one, pow_zero] },
   { exact ⟨i.succ, i.zero_lt_succ, hi.le, rfl⟩ }
@@ -605,6 +619,177 @@ end
 
 end is_cycle
 
+/-! ### `is_cycle_on` -/
+
+section is_cycle_on
+variables {f g : perm α} {s t : set α} {a b x y : α}
+
+/-- A permutation is a cycle on `s` when any two points of `s` are related by repeated application
+of the permutation. Note that this means the identity is a cycle of subsingleton sets. -/
+def is_cycle_on (f : perm α) (s : set α) : Prop :=
+set.bij_on f s s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → f.same_cycle x y
+
+@[simp] lemma is_cycle_on_empty : f.is_cycle_on ∅ := by simp [is_cycle_on]
+
+@[simp] lemma is_cycle_on_one : (1 : perm α).is_cycle_on s ↔ s.subsingleton :=
+by simp [is_cycle_on, set.bij_on_id, set.subsingleton]
+
+alias is_cycle_on_one ↔ is_cycle_on.subsingleton _root_.set.subsingleton.is_cycle_on_one
+
+@[simp] lemma is_cycle_on_singleton : f.is_cycle_on {a} ↔ f a = a :=
+by simp [is_cycle_on, same_cycle.rfl]
+
+lemma is_cycle_on_of_subsingleton [subsingleton α] (f : perm α) (s : set α) : f.is_cycle_on s :=
+⟨s.bij_on_of_subsingleton _, λ x _ y _, (subsingleton.elim x y).same_cycle _⟩
+
+@[simp] lemma is_cycle_on_inv : f⁻¹.is_cycle_on s ↔ f.is_cycle_on s :=
+by simp [is_cycle_on, set.bij_on_perm_inv]
+
+alias is_cycle_on_inv ↔ is_cycle_on.of_inv is_cycle_on.inv
+
+lemma is_cycle_on.conj (h : f.is_cycle_on s) : (g * f * g⁻¹).is_cycle_on ((g : perm α) '' s) :=
+⟨(g.bij_on_image.comp h.1).comp g.bij_on_symm_image,
+  λ x hx y hy, by { rw ←preimage_inv at hx hy, convert (h.2 hx hy).conj; rw apply_inv_self }⟩
+
+lemma is_cycle_on_swap [decidable_eq α] (hab : a ≠ b) : (swap a b).is_cycle_on {a, b} :=
+⟨bij_on_swap (by simp) (by simp), λ x hx y hy, begin
+  rw [set.mem_insert_iff, set.mem_singleton_iff] at hx hy,
+  obtain rfl | rfl := hx; obtain rfl | rfl := hy,
+  { exact ⟨0, by rw [zpow_zero, coe_one, id.def]⟩ },
+  { exact ⟨1, by rw [zpow_one, swap_apply_left]⟩ },
+  { exact ⟨1, by rw [zpow_one, swap_apply_right]⟩ },
+  { exact ⟨0, by rw [zpow_zero, coe_one, id.def]⟩ }
+end⟩
+
+protected lemma is_cycle_on.apply_ne (hf : f.is_cycle_on s) (hs : s.nontrivial) (ha : a ∈ s) :
+  f a ≠ a :=
+begin
+  obtain ⟨b, hb, hba⟩ := hs.exists_ne a,
+  obtain ⟨n, rfl⟩ := hf.2 ha hb,
+  exact λ h, hba (is_fixed_pt.perm_zpow h n),
+end
+
+protected lemma is_cycle.is_cycle_on (hf : f.is_cycle) : f.is_cycle_on {x | f x ≠ x} :=
+⟨f.bij_on $ λ x, f.apply_eq_iff_eq.not, λ a ha b, hf.same_cycle ha⟩
+
+/-- This lemma demonstrates the relation between `equiv.perm.is_cycle` and `equiv.perm.is_cycle_on`
+in non-degenerate cases. -/
+lemma is_cycle_iff_exists_is_cycle_on :
+  f.is_cycle ↔ ∃ s : set α, s.nontrivial ∧ f.is_cycle_on s ∧ ∀ ⦃x⦄, ¬ is_fixed_pt f x → x ∈ s :=
+begin
+  refine ⟨λ hf, ⟨{x | f x ≠ x}, _, hf.is_cycle_on, λ _, id⟩, _⟩,
+  { obtain ⟨a, ha⟩ := hf,
+    exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩ },
+  { rintro ⟨s, hs, hf, hsf⟩,
+   obtain ⟨a, ha⟩ := hs.nonempty,
+   exact ⟨a, hf.apply_ne hs ha, λ b hb, hf.2 ha $ hsf hb⟩ }
+end
+
+lemma is_cycle_on.apply_mem_iff (hf : f.is_cycle_on s) : f x ∈ s ↔ x ∈ s :=
+⟨λ hx, by { convert hf.1.perm_inv.1 hx, rw inv_apply_self }, λ hx, hf.1.maps_to hx⟩
+
+/-- Note that the identity satisfies `is_cycle_on` for any subsingleton set, but not `is_cycle`. -/
+lemma is_cycle_on.is_cycle_subtype_perm (hf : f.is_cycle_on s) (hs : s.nontrivial) :
+  (f.subtype_perm $ λ _, hf.apply_mem_iff.symm : perm s).is_cycle :=
+begin
+  obtain ⟨a, ha⟩ := hs.nonempty,
+  exact ⟨⟨a, ha⟩, ne_of_apply_ne (coe : s → α) (hf.apply_ne hs ha),
+    λ b hb, (hf.2 (⟨a, ha⟩ : s).prop b.prop).subtype_perm⟩,
+end
+
+/-- Note that the identity is a cycle on any subsingleton set, but not a cycle. -/
+protected lemma is_cycle_on.subtype_perm (hf : f.is_cycle_on s) :
+  (f.subtype_perm $ λ _, hf.apply_mem_iff.symm : perm s).is_cycle_on set.univ :=
+begin
+  obtain hs | hs := s.subsingleton_or_nontrivial,
+  { haveI := hs.coe_sort,
+    exact is_cycle_on_of_subsingleton _ _ },
+  convert (hf.is_cycle_subtype_perm hs).is_cycle_on,
+  rw [eq_comm, set.eq_univ_iff_forall],
+  exact λ x, ne_of_apply_ne (coe : s → α) (hf.apply_ne hs x.prop),
+end
+
+-- TODO: Theory of order of an element under an action
+lemma is_cycle_on.pow_apply_eq {s : finset α} (hf : f.is_cycle_on s) (ha : a ∈ s) {n : ℕ} :
+  (f ^ n) a = a ↔ s.card ∣ n :=
+begin
+  obtain rfl | hs := finset.eq_singleton_or_nontrivial ha,
+  { rw [coe_singleton, is_cycle_on_singleton] at hf,
+    simpa using is_fixed_pt.iterate hf n },
+  classical,
+  have h : ∀ x ∈ s.attach, ¬ f ↑x = ↑x := λ x hx, hf.apply_ne hs x.prop,
+  have := (hf.is_cycle_subtype_perm hs).order_of,
+  simp only [filter_true_of_mem h, support_subtype_perm, card_attach] at this,
+  rw [←this, order_of_dvd_iff_pow_eq_one, (hf.is_cycle_subtype_perm hs).pow_eq_one_iff'
+    (ne_of_apply_ne (coe : s → α) $ hf.apply_ne hs (⟨a, ha⟩ : s).prop)],
+  simp only [subtype.coe_mk, subtype_perm_pow, subtype_perm_apply],
+end
+
+lemma is_cycle_on.zpow_apply_eq {s : finset α} (hf : f.is_cycle_on s) (ha : a ∈ s) :
+  ∀ {n : ℤ}, (f ^ n) a = a ↔ (s.card : ℤ) ∣ n
+| (int.of_nat n) := (hf.pow_apply_eq ha).trans int.coe_nat_dvd.symm
+| (int.neg_succ_of_nat n) := by { rw [zpow_neg_succ_of_nat, ←inv_pow],
+    exact (hf.inv.pow_apply_eq ha).trans ((dvd_neg _ _).trans int.coe_nat_dvd).symm }
+
+lemma is_cycle_on.pow_apply_eq_pow_apply {s : finset α} (hf : f.is_cycle_on s) (ha : a ∈ s)
+  {m n : ℕ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD s.card] :=
+begin
+  rw [nat.modeq_iff_dvd, ←hf.zpow_apply_eq ha],
+  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm],
+end
+
+lemma is_cycle_on.zpow_apply_eq_zpow_apply {s : finset α} (hf : f.is_cycle_on s) (ha : a ∈ s)
+  {m n : ℤ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD s.card] :=
+begin
+  rw [int.modeq_iff_dvd, ←hf.zpow_apply_eq ha],
+  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm],
+end
+
+lemma is_cycle_on.pow_card_apply {s : finset α} (hf : f.is_cycle_on s) (ha : a ∈ s) :
+  (f ^ s.card) a = a :=
+(hf.pow_apply_eq ha).2 dvd_rfl
+
+lemma is_cycle_on.exists_pow_eq {s : finset α} (hf : f.is_cycle_on s) (ha : a ∈ s) (hb : b ∈ s) :
+  ∃ n < s.card, (f ^ n) a = b :=
+begin
+  classical,
+  obtain ⟨n, rfl⟩ := hf.2 ha hb,
+  obtain ⟨k, hk⟩ := (int.mod_modeq n s.card).symm.dvd,
+  refine ⟨n.nat_mod s.card, int.nat_mod_lt (nonempty.card_pos ⟨a, ha⟩).ne', _⟩,
+  rw [←zpow_coe_nat, int.nat_mod, int.to_nat_of_nonneg (int.mod_nonneg _ $ nat.cast_ne_zero.2
+    (nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul],
+  simp only [zpow_coe_nat, coe_mul, embedding_like.apply_eq_iff_eq],
+  exact is_fixed_pt.perm_zpow (hf.pow_card_apply ha) _,
+end
+
+lemma is_cycle_on.exists_pow_eq' (hs : s.finite) (hf : f.is_cycle_on s) (ha : a ∈ s) (hb : b ∈ s) :
+  ∃ n : ℕ, (f ^ n) a = b :=
+by { lift s to finset α using id hs, obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb, exact ⟨n, hn⟩ }
+
+lemma is_cycle_on.range_pow (hs : s.finite) (h : f.is_cycle_on s) (ha : a ∈ s) :
+  set.range (λ n, (f ^ n) a : ℕ → α) = s :=
+set.subset.antisymm (set.range_subset_iff.2 $ λ n, h.1.maps_to.perm_pow _ ha) $
+  λ x, h.exists_pow_eq' hs ha
+
+lemma is_cycle_on.range_zpow (h : f.is_cycle_on s) (ha : a ∈ s) :
+  set.range (λ n, (f ^ n) a : ℤ → α) = s :=
+set.subset.antisymm (set.range_subset_iff.2 $ λ n, (h.1.perm_zpow _).maps_to ha) $ h.2 ha
+
+lemma is_cycle_on.of_pow {n : ℕ} (hf : (f ^ n).is_cycle_on s) (h : set.bij_on f s s) :
+  f.is_cycle_on s :=
+⟨h, λ x hx y hy, (hf.2 hx hy).of_pow⟩
+
+lemma is_cycle_on.of_zpow {n : ℤ} (hf : (f ^ n).is_cycle_on s) (h : set.bij_on f s s) :
+  f.is_cycle_on s :=
+⟨h, λ x hx y hy, (hf.2 hx hy).of_zpow⟩
+
+lemma is_cycle_on.extend_domain {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p)
+  (h : g.is_cycle_on s) :
+  (g.extend_domain f).is_cycle_on (coe ∘ f '' s) :=
+⟨h.1.extend_domain, by { rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩, exact (h.2 ha hb).extend_domain }⟩
+
+end is_cycle_on
+
 /-!
 ### `cycle_of`
 -/
@@ -802,14 +987,45 @@ begin
       ←pow_eq_mod_order_of] }
 end
 
-/-- x is in the support of f iff cycle_of f x is a cycle.-/
-lemma is_cycle_cycle_of_iff (f : perm α) : is_cycle (cycle_of f x) ↔ (f x ≠ x) :=
+/-- `x` is in the support of `f` iff `equiv.perm.cycle_of f x` is a cycle. -/
+lemma is_cycle_cycle_of_iff (f : perm α) : is_cycle (cycle_of f x) ↔ f x ≠ x :=
 begin
-  split,
-  { intro hx, rw ne.def, rw ← cycle_of_eq_one_iff f,
-    exact equiv.perm.is_cycle.ne_one hx, },
-  { intro hx,
-    apply equiv.perm.is_cycle_cycle_of, exact hx }
+  refine ⟨λ hx, _, f.is_cycle_cycle_of⟩,
+  rw [ne.def, ←cycle_of_eq_one_iff f],
+  exact hx.ne_one,
+end
+
+lemma is_cycle_on_support_cycle_of (f : perm α) (x : α) : f.is_cycle_on (f.cycle_of x).support :=
+⟨f.bij_on $ by simp [mem_support_cycle_of_iff], λ a ha b hb,
+  by { rw [mem_coe, mem_support_cycle_of_iff] at ha hb, exact ha.1.symm.trans hb.1 }⟩
+
+lemma same_cycle.exists_pow_eq_of_mem_support (h : same_cycle f x y) (hx : x ∈ f.support) :
+  ∃ (i : ℕ) (hi' : i < (f.cycle_of x).support.card), (f ^ i) x = y :=
+begin
+  rw mem_support at hx,
+  refine (f.is_cycle_on_support_cycle_of _).exists_pow_eq _ _;
+    rwa mem_support_cycle_of_iff' hx,
+end
+
+lemma same_cycle.exists_pow_eq (f : perm α) (h : same_cycle f x y) :
+  ∃ (i : ℕ) (hi : 0 < i) (hi' : i ≤ (f.cycle_of x).support.card + 1), (f ^ i) x = y :=
+begin
+  by_cases hx : x ∈ f.support,
+  { obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx,
+    cases k,
+    { refine ⟨(f.cycle_of x).support.card, _, self_le_add_right _ _, _⟩,
+      { refine zero_lt_one.trans (one_lt_card_support_of_ne_one _),
+        simpa using hx },
+      { simp only [perm.coe_one, id.def, pow_zero] at hk',
+        subst hk',
+        rw [←(is_cycle_cycle_of _ $ mem_support.1 hx).order_of,
+            ←cycle_of_pow_apply_self, pow_order_of_eq_one, one_apply] } },
+    { exact ⟨k + 1, by simp, nat.le_succ_of_le hk.le, hk'⟩ } },
+  { refine ⟨1, zero_lt_one, by simp, _⟩,
+    obtain ⟨k, rfl⟩ := h,
+    rw [not_mem_support] at hx,
+    rw [pow_apply_eq_self_of_apply_eq_self hx,
+        zpow_apply_eq_self_of_apply_eq_self hx] }
 end
 
 end cycle_of
@@ -1171,72 +1387,6 @@ begin
       { exact λ H, hd.disjoint_cycle_factors_finset.le_bot (mem_inter_of_mem H hf) } } }
 end
 
-lemma same_cycle.nat_of_mem_support [fintype α] (f : perm α) {x y : α} (h : same_cycle f x y)
-  (hx : x ∈ f.support) :
-  ∃ (i : ℕ) (hi' : i < (f.cycle_of x).support.card), (f ^ i) x = y :=
-begin
-  revert f,
-  intro f,
-  apply cycle_induction_on _ f,
-  { simp },
-  { intros g hg H hx,
-    rw mem_support at hx,
-    rw [hg.cycle_of_eq hx, ←hg.order_of],
-    exact H.nat' },
-  { rintros g h hd hg IH IH' ⟨m, rfl⟩ hx,
-    cases (disjoint_iff_eq_or_eq.mp hd) x with hgx hhx,
-    { have hpow : ∀ (k : ℤ), ((g * h) ^ k) x = (h ^ k) x,
-      { intro k,
-        suffices : (g ^ k) x = x,
-        { simpa [hd.commute.eq, hd.commute.symm.mul_zpow] },
-        rw zpow_apply_eq_self_of_apply_eq_self,
-        simpa using hgx },
-      obtain ⟨k, hk, hk'⟩ := IH' _ _,
-      { refine ⟨k, _, _⟩,
-        { rw [←cycle_of_eq_one_iff] at hgx,
-          rwa [hd.cycle_of_mul_distrib, hgx, one_mul] },
-        { simpa [←zpow_coe_nat, hpow] using hk' } },
-      { use m,
-        simp [hpow] },
-      { rw [mem_support, hd.commute.eq] at hx,
-        simpa [hgx] using hx } },
-    { have hpow : ∀ (k : ℤ), ((g * h) ^ k) x = (g ^ k) x,
-      { intro k,
-        suffices : (h ^ k) x = x,
-        { simpa [hd.commute.mul_zpow] },
-        rw zpow_apply_eq_self_of_apply_eq_self,
-        simpa using hhx },
-      obtain ⟨k, hk, hk'⟩ := IH _ _,
-      { refine ⟨k, _, _⟩,
-        { rw [←cycle_of_eq_one_iff] at hhx,
-          rwa [hd.cycle_of_mul_distrib, hhx, mul_one] },
-        { simpa [←zpow_coe_nat, hpow] using hk' } },
-      { use m,
-        simp [hpow] },
-      { simpa [hhx] using hx } } }
-end
-
-lemma same_cycle.nat [fintype α] (f : perm α) {x y : α} (h : same_cycle f x y) :
-  ∃ (i : ℕ) (hi : 0 < i) (hi' : i ≤ (f.cycle_of x).support.card + 1), (f ^ i) x = y :=
-begin
-  by_cases hx : x ∈ f.support,
-  { obtain ⟨k, hk, hk'⟩ := same_cycle.nat_of_mem_support f h hx,
-    cases k,
-    { refine ⟨(f.cycle_of x).support.card, _, self_le_add_right _ _, _⟩,
-      { refine zero_lt_one.trans (one_lt_card_support_of_ne_one _),
-        simpa using hx },
-      { simp only [perm.coe_one, id.def, pow_zero] at hk',
-        subst hk',
-        rw [←(is_cycle_cycle_of _ $ mem_support.1 hx).order_of,
-            ←cycle_of_pow_apply_self, pow_order_of_eq_one, one_apply] } },
-    { exact ⟨k + 1, by simp, nat.le_succ_of_le hk.le, hk'⟩ } },
-  { refine ⟨1, zero_lt_one, by simp, _⟩,
-    obtain ⟨k, rfl⟩ := h,
-    rw [not_mem_support] at hx,
-    rw [pow_apply_eq_self_of_apply_eq_self hx,
-        zpow_apply_eq_self_of_apply_eq_self hx] }
-end
-
 section generation
 
 variables [finite β]
diff --git a/src/group_theory/perm/cycle/concrete.lean b/src/group_theory/perm/cycle/concrete.lean
index 1bc2a9449fa59..03a7eb22a2180 100644
--- a/src/group_theory/perm/cycle/concrete.lean
+++ b/src/group_theory/perm/cycle/concrete.lean
@@ -262,7 +262,7 @@ begin
     rw ←support_cycle_of_eq_nil_iff at hx,
     simp [hx] },
   { rintro ⟨h, hx⟩,
-    simpa using same_cycle.nat_of_mem_support _ h hx }
+    simpa using h.exists_pow_eq_of_mem_support hx }
 end
 
 lemma nodup_to_list (p : perm α) (x : α) :
@@ -305,7 +305,7 @@ lemma next_to_list_eq_apply (p : perm α) (x y : α) (hy : y ∈ to_list p x) :
   next (to_list p x) y hy = p y :=
 begin
   rw mem_to_list_iff at hy,
-  obtain ⟨k, hk, hk'⟩ := hy.left.nat_of_mem_support _ hy.right,
+  obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right,
   rw ←nth_le_to_list p x k (by simpa using hk) at hk',
   simp_rw ←hk',
   rw [next_nth_le _ (nodup_to_list _ _), nth_le_to_list, nth_le_to_list, ←mul_apply, ←pow_succ,
@@ -317,7 +317,7 @@ lemma to_list_pow_apply_eq_rotate (p : perm α) (x : α) (k : ℕ) :
   p.to_list ((p ^ k) x) = (p.to_list x).rotate k :=
 begin
   apply ext_le,
-  { simp },
+  { simp only [length_to_list, cycle_of_self_apply_pow, length_rotate]},
   { intros n hn hn',
     rw [nth_le_to_list, nth_le_rotate, nth_le_to_list, length_to_list,
         pow_mod_card_support_cycle_of_self_apply, pow_add, mul_apply] }
@@ -327,7 +327,7 @@ lemma same_cycle.to_list_is_rotated {f : perm α} {x y : α} (h : same_cycle f x
   to_list f x ~r to_list f y :=
 begin
   by_cases hx : x ∈ f.support,
-  { obtain ⟨_ | k, hk, hy⟩ := h.nat_of_mem_support _ hx,
+  { obtain ⟨_ | k, hk, hy⟩ := h.exists_pow_eq_of_mem_support hx,
     { simp only [coe_one, id.def, pow_zero] at hy,
       simp [hy] },
     use k.succ,
@@ -341,7 +341,7 @@ lemma pow_apply_mem_to_list_iff_mem_support {n : ℕ} :
 begin
   rw [mem_to_list_iff, and_iff_right_iff_imp],
   refine λ _, same_cycle.symm _,
-  rw same_cycle_pow_left_iff
+  rw same_cycle_pow_left
 end
 
 lemma to_list_form_perm_nil (x : α) :
@@ -389,7 +389,7 @@ begin
         form_perm_nil] },
   ext y,
   by_cases hy : same_cycle f x y,
-  { obtain ⟨k, hk, rfl⟩ := hy.nat_of_mem_support _ (mem_support.mpr hx),
+  { obtain ⟨k, hk, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx),
     rw [cycle_of_apply_apply_pow_self, list.form_perm_apply_mem_eq_next (nodup_to_list f x),
         next_to_list_eq_apply, pow_succ, mul_apply],
     rw mem_to_list_iff,
diff --git a/src/group_theory/perm/support.lean b/src/group_theory/perm/support.lean
index b779f3197931f..f8aac0b2bf1e7 100644
--- a/src/group_theory/perm/support.lean
+++ b/src/group_theory/perm/support.lean
@@ -615,4 +615,8 @@ end card
 
 end support
 
+@[simp] lemma support_subtype_perm [decidable_eq α] {s : finset α} (f : perm α) (h) :
+  (f.subtype_perm h : perm {x // x ∈ s}).support = s.attach.filter (λ x, f x ≠ x) :=
+by { ext, simp [subtype.ext_iff] }
+
 end equiv.perm