-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.commute_iff {g c : Perm α} (hc : c.IsCycle) :
    Commute g c ↔
      ∃ hc' : ∀ x : α, x ∈ c.support ↔ g x ∈ c.support,
        ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c

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

Tactic:
simp only [Perm.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]

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

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

Tactic:
refine exists_congr fun hc' => exists_congr fun k => ?_

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

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

Tactic:
rw [imp_iff_right ha, ofSubtype_subtypePerm_of_mem hc' ha]

Result:
no goals

Proof state:
case neg.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support

Tactic:
exact ha

Result:
no goals

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

Tactic:
by_cases ha : a ∈ c.support

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

case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Proof state:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← not_mem_support]

Result:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ (c ^ k).support

case neg.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support

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

Tactic:
intro a

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

Proof state:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ (c ^ k).support

Tactic:
exact Finset.not_mem_mono (support_zpow_le c k) ha

Result:
no goals

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

Tactic:
simp_rw [hc.commute_iff', Subgroup.mem_zpowers_iff]

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

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

Tactic:
rw [subtypePermOfSupport, subtypePerm_zpow c k]

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

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

Tactic:
apply forall_congr'

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