Theorem: Equiv.Perm.existsBasis (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nonempty (Equiv.Perm.Basis g)
Tactic:
suffices hsupp_ne :
  ∀ c : g.cycleFactorsFinset, (c : Equiv.Perm α).support.Nonempty by
  exact ⟨fun c ↦ (hsupp_ne c).choose, fun c ↦ (hsupp_ne c).choose_spec⟩
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑c).Nonempty

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑c).Nonempty
Tactic:
intro c
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑c).Nonempty

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑c).Nonempty
Tactic:
exact Equiv.Perm.IsCycle.nonempty_support (Equiv.Perm.mem_cycleFactorsFinset_iff.mp c.prop).1
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
hsupp_ne : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑c).Nonempty
⊢ Nonempty (Equiv.Perm.Basis g)
Tactic:
exact ⟨fun c ↦ (hsupp_ne c).choose, fun c ↦ (hsupp_ne c).choose_spec⟩
State after:
no goals