case intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ f ^ n = 1 ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
⊢ f ^ n = 1 ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
cases nonempty_fintype β
case intro.mp
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ f ^ n = 1 → ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x

case intro.mpr
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ (∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x) → f ^ n = 1
case intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ f ^ n = 1 ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
constructor
case intro.mp
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
case intro.mp
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ f ^ n = 1 → ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
intro h
case intro.mp.intro.intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
x : β
hx : ↑f x ≠ x
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
case intro.mp
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
obtain ⟨x, hx, -⟩ := id hf
no goals
case intro.mp.intro.intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
x : β
hx : ↑f x ≠ x
⊢ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x
exact ⟨x, hx, by simp [h]⟩
no goals
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
x : β
hx : ↑f x ≠ x
⊢ ↑(f ^ n) x = x
simp [h]
case intro.mpr.intro.intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
⊢ f ^ n = 1
case intro.mpr
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ (∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x) → f ^ n = 1
rintro ⟨x, hx, hx'⟩
case pos
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
h : support (f ^ n) = support f
⊢ f ^ n = 1

case neg
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
h : ¬support (f ^ n) = support f
⊢ f ^ n = 1
case intro.mpr.intro.intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
⊢ f ^ n = 1
by_cases h : support (f ^ n) = support f
case pos
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx✝ : ↑f x ≠ x
hx : ↑(f ^ n) x ≠ x
hx' : ↑(f ^ n) x = x
h : support (f ^ n) = support f
⊢ f ^ n = 1
case pos
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
h : support (f ^ n) = support f
⊢ f ^ n = 1
rw [← mem_support, ← h, mem_support] at hx
no goals
case pos
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx✝ : ↑f x ≠ x
hx : ↑(f ^ n) x ≠ x
hx' : ↑(f ^ n) x = x
h : support (f ^ n) = support f
⊢ f ^ n = 1
contradiction
case neg
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
h : orderOf f ∣ n
⊢ f ^ n = 1
case neg
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
h : ¬support (f ^ n) = support f
⊢ f ^ n = 1
rw [hf.support_pow_eq_iff, Classical.not_not] at h
case neg.intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
k : ℕ
hx' : ↑(f ^ (orderOf f * k)) x = x
⊢ f ^ (orderOf f * k) = 1
case neg
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
hx' : ↑(f ^ n) x = x
h : orderOf f ∣ n
⊢ f ^ n = 1
obtain ⟨k, rfl⟩ := h
no goals
case neg.intro
ι : Type ?u.1228455
α : Type ?u.1228458
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
x : β
hx : ↑f x ≠ x
k : ℕ
hx' : ↑(f ^ (orderOf f * k)) x = x
⊢ f ^ (orderOf f * k) = 1
rw [pow_mul, pow_orderOf_eq_one, one_pow]