case intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ IsCycle (f ^ n) ↔ Nat.coprime n (orderOf f)
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
⊢ IsCycle (f ^ n) ↔ Nat.coprime n (orderOf f)
cases nonempty_fintype β
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ IsCycle (f ^ n) → Nat.coprime n (orderOf f)

case intro.mpr
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ Nat.coprime n (orderOf f) → IsCycle (f ^ n)
case intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ IsCycle (f ^ n) ↔ Nat.coprime n (orderOf f)
constructor
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
⊢ Nat.coprime n (orderOf f)
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ IsCycle (f ^ n) → Nat.coprime n (orderOf f)
intro h
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
⊢ Nat.coprime n (orderOf f)
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
⊢ Nat.coprime n (orderOf f)
have hr : support (f ^ n) = support f := by
  rw [hf.support_pow_eq_iff]
  rintro ⟨k, rfl⟩
  refine' h.ne_one _
  simp [pow_mul, pow_orderOf_eq_one]
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
this : orderOf (f ^ n) = orderOf f
⊢ Nat.coprime n (orderOf f)
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
⊢ Nat.coprime n (orderOf f)
have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
this : orderOf f = 0 ∨ Nat.gcd (orderOf f) n = 1
⊢ Nat.coprime n (orderOf f)
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
this : orderOf (f ^ n) = orderOf f
⊢ Nat.coprime n (orderOf f)
rw [orderOf_pow, Nat.div_eq_self] at this
case intro.mp.inl
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h✝ : IsCycle (f ^ n)
hr : support (f ^ n) = support f
h : orderOf f = 0
⊢ Nat.coprime n (orderOf f)

case intro.mp.inr
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
h✝ : Nat.gcd (orderOf f) n = 1
⊢ Nat.coprime n (orderOf f)
case intro.mp
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
this : orderOf f = 0 ∨ Nat.gcd (orderOf f) n = 1
⊢ Nat.coprime n (orderOf f)
cases' this with h
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
⊢ ¬orderOf f ∣ n
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
⊢ support (f ^ n) = support f
rw [hf.support_pow_eq_iff]
case intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
k : ℕ
h : IsCycle (f ^ (orderOf f * k))
⊢ False
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
⊢ ¬orderOf f ∣ n
rintro ⟨k, rfl⟩
case intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
k : ℕ
h : IsCycle (f ^ (orderOf f * k))
⊢ f ^ (orderOf f * k) = 1
case intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
k : ℕ
h : IsCycle (f ^ (orderOf f * k))
⊢ False
refine' h.ne_one _
no goals
case intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
val✝ : Fintype β
k : ℕ
h : IsCycle (f ^ (orderOf f * k))
⊢ f ^ (orderOf f * k) = 1
simp [pow_mul, pow_orderOf_eq_one]
no goals
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
⊢ orderOf (f ^ n) = orderOf f
rw [h.orderOf, hr, hf.orderOf]
no goals
case intro.mp.inl
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h✝ : IsCycle (f ^ n)
hr : support (f ^ n) = support f
h : orderOf f = 0
⊢ Nat.coprime n (orderOf f)
exact absurd h (orderOf_pos _).ne'
no goals
case intro.mp.inr
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : IsCycle (f ^ n)
hr : support (f ^ n) = support f
h✝ : Nat.gcd (orderOf f) n = 1
⊢ Nat.coprime n (orderOf f)
rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
case intro.mpr
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
⊢ IsCycle (f ^ n)
case intro.mpr
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
⊢ Nat.coprime n (orderOf f) → IsCycle (f ^ n)
intro h
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ IsCycle (f ^ n)
case intro.mpr
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
⊢ IsCycle (f ^ n)
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : IsCycle ((f ^ n) ^ m)
⊢ IsCycle (f ^ n)
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ IsCycle (f ^ n)
have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : IsCycle ((f ^ n) ^ m)
x : β
hx : x ∈ support (f ^ n)
⊢ x ∈ support ((f ^ n) ^ m)
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : IsCycle ((f ^ n) ^ m)
⊢ IsCycle (f ^ n)
refine' hf'.of_pow fun x hx => _
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : IsCycle ((f ^ n) ^ m)
x : β
hx : x ∈ support (f ^ n)
⊢ x ∈ support f
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : IsCycle ((f ^ n) ^ m)
x : β
hx : x ∈ support (f ^ n)
⊢ x ∈ support ((f ^ n) ^ m)
rw [hm]
no goals
case intro.mpr.intro
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x✝ y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : IsCycle ((f ^ n) ^ m)
x : β
hx : x ∈ support (f ^ n)
⊢ x ∈ support f
exact support_pow_le _ n hx
no goals
ι : Type ?u.1194880
α : Type ?u.1194883
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
n : ℕ
val✝ : Fintype β
h : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ IsCycle ((f ^ n) ^ m)
rwa [hm]