case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Finset.card (support σ) < 2 * orderOf σ
n : ℕ
hn : cycleType σ = replicate (n + 1) (orderOf σ)
⊢ IsCycle σ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Finset.card (support σ) < 2 * orderOf σ
⊢ IsCycle σ
obtain ⟨n, hn⟩ := cycleType_prime_order h1
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : cycleType σ = replicate (n + 1) (orderOf σ)
⊢ IsCycle σ
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Finset.card (support σ) < 2 * orderOf σ
n : ℕ
hn : cycleType σ = replicate (n + 1) (orderOf σ)
⊢ IsCycle σ
rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id,
  mul_lt_mul_right (orderOf_pos σ), Nat.succ_lt_succ_iff, Nat.lt_succ_iff, le_zero_iff] at h2
no goals
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : cycleType σ = replicate (n + 1) (orderOf σ)
⊢ IsCycle σ
rw [← card_cycleType_eq_one, hn, card_replicate, h2]