α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, cycleType σ = {a}) ↔ IsCycle σ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ ↑card (cycleType σ) = 1 ↔ IsCycle σ
rw [card_eq_one]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ IsCycle σ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, cycleType σ = {a}) ↔ IsCycle σ
simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
  cycleFactorsFinset_eq_singleton_iff]
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) → IsCycle σ

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ IsCycle σ → ∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ IsCycle σ
constructor
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
w✝¹ : ℕ
w✝ : Perm α
h : IsCycle σ
⊢ IsCycle σ
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) → IsCycle σ
rintro ⟨_, _, ⟨h, -⟩, -⟩
no goals
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
w✝¹ : ℕ
w✝ : Perm α
h : IsCycle σ
⊢ IsCycle σ
exact h
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsCycle σ
⊢ ∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ IsCycle σ → ∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a
intro h
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsCycle σ
⊢ (IsCycle σ ∧ σ = σ) ∧ (Finset.card ∘ support) σ = Finset.card (support σ)
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsCycle σ
⊢ ∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a
use σ.support.card, σ
no goals
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsCycle σ
⊢ (IsCycle σ ∧ σ = σ) ∧ (Finset.card ∘ support) σ = Finset.card (support σ)
simp [h]