ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
⊢ support (f ^ n) = support f ↔ ¬f ^ n = 1
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
⊢ support (f ^ n) = support f ↔ ¬orderOf f ∣ n
rw [orderOf_dvd_iff_pow_eq_one]
case mp
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
⊢ support (f ^ n) = support f → ¬f ^ n = 1

case mpr
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
⊢ ¬f ^ n = 1 → support (f ^ n) = support f
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
⊢ support (f ^ n) = support f ↔ ¬f ^ n = 1
constructor
case mp
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
h : support (f ^ n) = support f
H : f ^ n = 1
⊢ False
case mp
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
⊢ support (f ^ n) = support f → ¬f ^ n = 1
intro h H
case mp
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
h : support (f ^ n) = support f
H : f ^ n = 1
⊢ f = 1
case mp
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
h : support (f ^ n) = support f
H : f ^ n = 1
⊢ False
refine' hf.ne_one _
no goals
case mp
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
h : support (f ^ n) = support f
H : f ^ n = 1
⊢ f = 1
rw [← support_eq_empty_iff, ← h, H, support_one]
case mpr
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
H : ¬f ^ n = 1
⊢ support (f ^ n) = support f
case mpr
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
⊢ ¬f ^ n = 1 → support (f ^ n) = support f
intro H
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
H : ¬f ^ n = 1
⊢ support f ≤ support (f ^ n)
case mpr
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
H : ¬f ^ n = 1
⊢ support (f ^ n) = support f
apply le_antisymm (support_pow_le _ n) _
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
H : ¬f ^ n = 1
x : α
hx : x ∈ support f
⊢ x ∈ support (f ^ n)
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
H : ¬f ^ n = 1
⊢ support f ≤ support (f ^ n)
intro x hx
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
⊢ f ^ n = 1
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
H : ¬f ^ n = 1
x : α
hx : x ∈ support f
⊢ x ∈ support (f ^ n)
contrapose! H
case H
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
z : α
⊢ ↑(f ^ n) z = ↑1 z
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
⊢ f ^ n = 1
ext z
case pos
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
z : α
hz : ↑f z = z
⊢ ↑(f ^ n) z = ↑1 z

case neg
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
z : α
hz : ¬↑f z = z
⊢ ↑(f ^ n) z = ↑1 z
case H
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
z : α
⊢ ↑(f ^ n) z = ↑1 z
by_cases hz : f z = z
no goals
case pos
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
z : α
hz : ↑f z = z
⊢ ↑(f ^ n) z = ↑1 z
rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]
case neg.intro
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
z : α
hz : ¬↑f z = z
k : ℕ
hx : ↑(f ^ k) z ∈ support f
H : ¬↑(f ^ k) z ∈ support (f ^ n)
⊢ ↑(f ^ n) z = ↑1 z
case neg
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x✝ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
x : α
hx : x ∈ support f
H : ¬x ∈ support (f ^ n)
z : α
hz : ¬↑f z = z
⊢ ↑(f ^ n) z = ↑1 z
obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)
case neg.intro.a
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
z : α
hz : ¬↑f z = z
k : ℕ
hx : ↑(f ^ k) z ∈ support f
H : ¬↑(f ^ k) z ∈ support (f ^ n)
⊢ ↑(f ^ k) (↑(f ^ n) z) = ↑(f ^ k) (↑1 z)
case neg.intro
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
z : α
hz : ¬↑f z = z
k : ℕ
hx : ↑(f ^ k) z ∈ support f
H : ¬↑(f ^ k) z ∈ support (f ^ n)
⊢ ↑(f ^ n) z = ↑1 z
apply (f ^ k).injective
case neg.intro.a
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
z : α
hz : ¬↑f z = z
k : ℕ
hx : ↑(f ^ k) z ∈ support f
H : ¬↑(f ^ k) z ∈ support (f ^ n)
⊢ ↑(f ^ n) (↑(f ^ k) z) = ↑(f ^ k) (↑1 z)
case neg.intro.a
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
z : α
hz : ¬↑f z = z
k : ℕ
hx : ↑(f ^ k) z ∈ support f
H : ¬↑(f ^ k) z ∈ support (f ^ n)
⊢ ↑(f ^ k) (↑(f ^ n) z) = ↑(f ^ k) (↑1 z)
rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]
no goals
case neg.intro.a
ι : Type ?u.1128878
α : Type u_1
β : Type ?u.1128884
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
n : ℕ
z : α
hz : ¬↑f z = z
k : ℕ
hx : ↑(f ^ k) z ∈ support f
H : ¬↑(f ^ k) z ∈ support (f ^ n)
⊢ ↑(f ^ n) (↑(f ^ k) z) = ↑(f ^ k) (↑1 z)
simpa using H