-- 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,
        subtypePerm g hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Proof state:
case h.H.mk.a.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i * c ^ j) a = (c ^ j * g) a

Tactic:
rw [← zpow_add, add_comm i j, zpow_add]

Result:
case h.H.mk.a.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a

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), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Tactic:
constructor

Result:
case mp
α : 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), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

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

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

Tactic:
obtain ⟨a, ha⟩ := IsCycle.nonempty_support hc

Result:
case h.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
⊢ g.subtypePerm hgc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Proof state:
case mpr.intro.intro.H
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
⊢ g (c x) = c (g x)

Tactic:
by_cases hx : x ∈ 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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
⊢ g (c x) = c (g x)

case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g (c x) = c (g x)

Proof state:
case h.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ ↑(((fun x => c.subtypePermOfSupport ^ x) i) ⟨x, hx⟩) = ↑((g.subtypePerm hgc') ⟨x, hx⟩)

Tactic:
simp only [subtypePermOfSupport, Subtype.coe_mk, subtypePerm_apply]

Result:
case h.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ ↑((c.subtypePerm ⋯ ^ i) ⟨x, hx⟩) = g x

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

Tactic:
simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]

Result:
no goals

Proof state:
case h.H.mk.a.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a

Tactic:
simp only [mul_apply, EmbeddingLike.apply_eq_iff_eq]

Result:
case h.H.mk.a.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i) a = g a

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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x✝ : α
hx✝ : x✝ ∈ c.support
x : α
hx : x ∈ c.support
hix : (c ^ i) x = g x
⊢ g x = (c ^ i) x

Tactic:
exact hix.symm

Result:
no goals

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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x✝ : α
hx✝ : x✝ ∈ c.support
x : α
hx : x ∈ c.support
hix : ((fun x => c.subtypePermOfSupport ^ x) i) ⟨x, hx⟩ = (g.subtypePerm hc') ⟨x, hx⟩
⊢ g x = (c ^ i) x

Tactic:
simp only [← Subtype.coe_inj, subtypePermOfSupport, Subtype.coe_mk, subtypePerm_apply,
  subtypePerm_apply_zpow_of_mem] at hix

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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x✝ : α
hx✝ : x✝ ∈ c.support
x : α
hx : x ∈ c.support
hix : (c ^ i) x = g x
⊢ g x = (c ^ i) x

Proof state:
case mp
α : 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), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Tactic:
intro hgc

Result:
case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
⊢ ∃ (hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x✝ : α
hx✝ : x✝ ∈ c.support
x : α
hx : x ∈ c.support
⊢ g x = (c ^ i) x

Tactic:
have hix := Perm.congr_fun hi ⟨x, hx⟩

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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x✝ : α
hx✝ : x✝ ∈ c.support
x : α
hx : x ∈ c.support
hix : ((fun x => c.subtypePermOfSupport ^ x) i) ⟨x, hx⟩ = (g.subtypePerm hc') ⟨x, hx⟩
⊢ g x = (c ^ i) x

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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g (c x) = c (g x)

Tactic:
rw [not_mem_support.mp hx, eq_comm, ← 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
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g x ∉ c.support