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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ c = cycleOf g x ↔ x ∈ support c
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ c = cycleOf g x → x ∈ support c

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c → c = cycleOf g x

State before:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ c = cycleOf g x → x ∈ support c
Tactic:
intro hcx
State after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ x ∈ support c

State before:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ x ∈ support c
Tactic:
rw [Equiv.Perm.mem_support, hcx, Equiv.Perm.cycleOf_apply_self,
  Ne.def, ← Equiv.Perm.cycleOf_eq_one_iff, ← hcx]
State after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ ¬c = 1

State before:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ ¬c = 1
Tactic:
exact Equiv.Perm.IsCycle.ne_one (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c → c = cycleOf g x
Tactic:
intro hx
State after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ c = cycleOf g x

State before:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ c = cycleOf g x
Tactic:
exact Equiv.Perm.cycle_is_cycleOf hx hc
State after:
no goals