ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : IsCycle (f ^ n)
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
⊢ IsCycle f
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : IsCycle (f ^ n)
h2 : support f ⊆ support (f ^ n)
⊢ IsCycle f
have key : ∀ x : α, (f ^ n) x ≠ x ↔ f x ≠ x := by
  simp_rw [← mem_support, ← Finset.ext_iff]
  exact (support_pow_le _ n).antisymm h2
case intro.intro
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
x : α
hx1 : ↑(f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, ↑(f ^ n) y ≠ y → SameCycle (f ^ n) x y
⊢ IsCycle f
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : IsCycle (f ^ n)
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
⊢ IsCycle f
obtain ⟨x, hx1, hx2⟩ := h1
case intro.intro
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
x : α
hx1 : ↑(f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, ↑(f ^ n) y ≠ y → SameCycle (f ^ n) x y
y : α
hy : ↑f y ≠ y
⊢ SameCycle f x y
case intro.intro
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
x : α
hx1 : ↑(f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, ↑(f ^ n) y ≠ y → SameCycle (f ^ n) x y
⊢ IsCycle f
refine' ⟨x, (key x).mp hx1, fun y hy => _⟩
case intro.intro.intro
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
x : α
hx1 : ↑(f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, ↑(f ^ n) y ≠ y → SameCycle (f ^ n) x y
y : α
hy : ↑f y ≠ y
i : ℤ
h✝ : ↑((f ^ n) ^ i) x = y
⊢ SameCycle f x y
case intro.intro
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
x : α
hx1 : ↑(f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, ↑(f ^ n) y ≠ y → SameCycle (f ^ n) x y
y : α
hy : ↑f y ≠ y
⊢ SameCycle f x y
cases' hx2 ((key y).mpr hy) with i _
no goals
case intro.intro.intro
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
x : α
hx1 : ↑(f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, ↑(f ^ n) y ≠ y → SameCycle (f ^ n) x y
y : α
hy : ↑f y ≠ y
i : ℤ
h✝ : ↑((f ^ n) ^ i) x = y
⊢ SameCycle f x y
exact ⟨n * i, by rwa [zpow_mul]⟩
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : IsCycle (f ^ n)
h2 : support f ⊆ support (f ^ n)
⊢ support (f ^ n) = support f
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : IsCycle (f ^ n)
h2 : support f ⊆ support (f ^ n)
⊢ ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
simp_rw [← mem_support, ← Finset.ext_iff]
no goals
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : IsCycle (f ^ n)
h2 : support f ⊆ support (f ^ n)
⊢ support (f ^ n) = support f
exact (support_pow_le _ n).antisymm h2
no goals
ι : Type ?u.1024464
α : Type u_1
β : Type ?u.1024470
f g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : support f ⊆ support (f ^ n)
key : ∀ (x : α), ↑(f ^ n) x ≠ x ↔ ↑f x ≠ x
x : α
hx1 : ↑(f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, ↑(f ^ n) y ≠ y → SameCycle (f ^ n) x y
y : α
hy : ↑f y ≠ y
i : ℤ
h✝ : ↑((f ^ n) ^ i) x = y
⊢ ↑(f ^ (↑n * i)) x = y
rwa [zpow_mul]