Theorem: Equiv.Perm.IsCycle.forall_commute_iff (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ (∀ c ∈ cycleFactorsFinset g, Commute z c) ↔
    ∀ c ∈ cycleFactorsFinset g,
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Tactic:
apply forall_congr'
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ ∀ (a : Perm α),
    a ∈ cycleFactorsFinset g → Commute z a ↔
      a ∈ cycleFactorsFinset g →
        ∃ (hc : ∀ (x : α), x ∈ support a ↔ z x ∈ support a), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers a

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ ∀ (a : Perm α),
    a ∈ cycleFactorsFinset g → Commute z a ↔
      a ∈ cycleFactorsFinset g →
        ∃ (hc : ∀ (x : α), x ∈ support a ↔ z x ∈ support a), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers a
Tactic:
intro c
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g → Commute z c ↔
    c ∈ cycleFactorsFinset g →
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g → Commute z c ↔
    c ∈ cycleFactorsFinset g →
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Tactic:
apply imp_congr_right
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c)

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c)
Tactic:
intro hc
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Tactic:
exact Equiv.Perm.IsCycle.commute_iff (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).1
State after:
no goals