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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c), subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)
Tactic:
rw [Equiv.Perm.IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c),
      subtypePerm k hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c), subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)

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

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ ∀ (a : ∀ (x : α), x ∈ support c ↔ k x ∈ support c),
    subtypePerm k a ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ subtypePerm k a ∈ Subgroup.zpowers (subtypePerm g ⋯)
Tactic:
intro hc'
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)
Tactic:
simp only [Subgroup.mem_zpowers_iff]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ (∃ k_1, subtypePermOfSupport c ^ k_1 = subtypePerm k hc') ↔ ∃ k_1, subtypePerm g ⋯ ^ k_1 = subtypePerm k hc'

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ (∃ k_1, subtypePermOfSupport c ^ k_1 = subtypePerm k hc') ↔ ∃ k_1, subtypePerm g ⋯ ^ k_1 = subtypePerm k hc'
Tactic:
apply exists_congr
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ a = subtypePerm k hc'

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ a = subtypePerm k hc'
Tactic:
intro n
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePermOfSupport c ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePermOfSupport c ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'
Tactic:
unfold subtypePermOfSupport
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'
Tactic:
rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePermOfSupport c ^ n = subtypePerm k hc'

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePermOfSupport c ^ n = subtypePerm k hc'
Tactic:
rfl
State after:
no goals