-- 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.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

Tactic:
obtain ⟨i, hi⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp ((hgc' a).mp ha))

Result:
case h.intro.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
⊢ g.subtypePerm hgc' ∈ Subgroup.zpowers c.subtypePermOfSupport

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 : g x ∈ c.support
⊢ x ∈ c.support

Tactic:
exact (hc' x).mpr hx

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 ∈ c.support, g x = (c ^ i) x

Tactic:
intro 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
⊢ 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 x ∉ c.support

Tactic:
contrapose! hx

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 : g x ∈ c.support
⊢ x ∈ c.support

Proof state:
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

Tactic:
have hgc' := mem_support_iff_of_commute hgc

Result:
case mp
α : 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
⊢ ∃ (hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Proof state:
case h.intro.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
⊢ g.subtypePerm hgc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Tactic:
use i

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

Proof state:
case mpr.intro.intro
α : 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'
⊢ Commute g c

Tactic:
ext x

Result:
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

Proof state:
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

Tactic:
rintro ⟨hc', ⟨i, hi⟩⟩

Result:
case mpr.intro.intro
α : 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'
⊢ Commute g c

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
⊢ (c ^ i) x = g x

Tactic:
obtain ⟨j, rfl⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)

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) ((c ^ j) a) = g ((c ^ j) 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
⊢ g (c x) = c (g x)

Tactic:
suffices hi' : ∀ x ∈ c.support, g x = (c ^ i) x by
  rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]
  simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]

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 ∈ c.support, g x = (c ^ i) x

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

Tactic:
ext ⟨x, hx⟩

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
⊢ ↑(((fun x => c.subtypePermOfSupport ^ x) i) ⟨x, hx⟩) = ↑((g.subtypePerm hgc') ⟨x, hx⟩)

Proof state:
case mp
α : 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
⊢ ∃ (hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Tactic:
use hgc'

Result:
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

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
⊢ g (c x) = c (g x)

Tactic:
rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]

Result:
α : 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)