-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem commute_iff_of_mem_cycleFactorsFinset [DecidableEq α] [Fintype α]{g k c : Equiv.Perm α}
    (hc : c ∈ g.cycleFactorsFinset) :
    Commute k c ↔
      ∃ hc' : ∀ x : α, x ∈ c.support ↔ k x ∈ c.support,
        k.subtypePerm hc' ∈ Subgroup.zpowers
          (g.subtypePerm (mem_cycleFactorsFinset_support hc))

Proof state:
case h.h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support
⊢ ∀ (a : ℤ), c.subtypePermOfSupport ^ a = k.subtypePerm hc' ↔ g.subtypePerm ⋯ ^ a = k.subtypePerm hc'

Tactic:
intro n

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

Proof state:
case h.h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support
n : ℤ
⊢ c.subtypePermOfSupport ^ n = k.subtypePerm hc' ↔ g.subtypePerm ⋯ ^ n = k.subtypePerm hc'

Tactic:
rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Tactic:
rw [IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ (∃ (hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport) ↔
    ∃ (hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Proof state:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support
⊢ (∃ k_1, c.subtypePermOfSupport ^ k_1 = k.subtypePerm hc') ↔ ∃ k_1, g.subtypePerm ⋯ ^ k_1 = k.subtypePerm hc'

Tactic:
apply exists_congr

Result:
case h.h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support
⊢ ∀ (a : ℤ), c.subtypePermOfSupport ^ a = k.subtypePerm hc' ↔ g.subtypePerm ⋯ ^ a = k.subtypePerm hc'

Proof state:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ ∀ (a : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support),
    k.subtypePerm a ∈ Subgroup.zpowers c.subtypePermOfSupport ↔ k.subtypePerm a ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Tactic:
intro hc'

Result:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support
⊢ k.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport ↔ k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ (∃ (hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport) ↔
    ∃ (hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Tactic:
apply exists_congr

Result:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ ∀ (a : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support),
    k.subtypePerm a ∈ Subgroup.zpowers c.subtypePermOfSupport ↔ k.subtypePerm a ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Proof state:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support
⊢ k.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport ↔ k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Tactic:
simp only [Subgroup.mem_zpowers_iff]

Result:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), x ∈ c.support ↔ k x ∈ c.support
⊢ (∃ k_1, c.subtypePermOfSupport ^ k_1 = k.subtypePerm hc') ↔ ∃ k_1, g.subtypePerm ⋯ ^ k_1 = k.subtypePerm hc'