case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : Nat.coprime n (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ support (σ ^ n) = support σ
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : Nat.coprime n (orderOf σ)
⊢ support (σ ^ n) = support σ
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
no goals
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : Nat.coprime n (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ support (σ ^ n) = support σ
exact
  le_antisymm (support_pow_le σ n)
    (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))