α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : ∃ a, (IsCycle a ∧ ∀ (a_1 : α), a_1 ∈ support a → ↑a a_1 = ↑σ a_1) ∧ Finset.card (support a) = n
⊢ 2 ≤ n
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ cycleType σ
⊢ 2 ≤ n
simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map,
  mem_cycleFactorsFinset_iff] at h
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ w✝ : Perm α
hc : IsCycle w✝
⊢ 2 ≤ Finset.card (support w✝)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : ∃ a, (IsCycle a ∧ ∀ (a_1 : α), a_1 ∈ support a → ↑a a_1 = ↑σ a_1) ∧ Finset.card (support a) = n
⊢ 2 ≤ n
obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h
no goals
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ w✝ : Perm α
hc : IsCycle w✝
⊢ 2 ≤ Finset.card (support w✝)
exact hc.two_le_card_support