Theorem: Equiv.Perm.IsCycle.commute_iff' (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ Commute g c ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ Commute g c →
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

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

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ Commute g c →
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
intro hgc
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
let hgc' := Equiv.Perm.mem_support_of_commute hgc
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
use hgc'
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
obtain ⟨a, ha⟩ := Equiv.Perm.IsCycle.nonempty_support hc
State after:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

State before:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
suffices c.SameCycle a (g a) by
  simp only [Equiv.Perm.SameCycle] at this
  obtain ⟨i, hi⟩ := this; use i
  ext ⟨x, hx⟩
  simp only [Equiv.Perm.subtypePermOfSupport, Subtype.coe_mk, Equiv.Perm.subtypePerm_apply]
  rw [Equiv.Perm.subtypePerm_apply_zpow_of_mem]
  suffices c.SameCycle a x by
    obtain ⟨j, rfl⟩ := this
    simp only [← Equiv.Perm.mul_apply, Commute.eq (Commute.zpow_right hgc j)]
    rw [← zpow_add, add_comm i j, zpow_add]
    simp only [Equiv.Perm.mul_apply]
    simp only [EmbeddingLike.apply_eq_iff_eq]
    exact hi
  exact hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)
State after:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ SameCycle c a (g a)

State before:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ SameCycle c a (g a)
Tactic:
apply hc.sameCycle (mem_support.mp ha) (mem_support.mp ((hgc' a).mp ha))
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
this : SameCycle c a (g a)
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
simp only [Equiv.Perm.SameCycle] at this
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
this : ∃ i, (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
this : ∃ i, (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
obtain ⟨i, hi⟩ := this
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
use i
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hgc'

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hgc'
Tactic:
ext ⟨x, hx⟩
State after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑(((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx }) =
    ↑((subtypePerm g hgc') { val := x, property := hx })

State before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑(((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx }) =
    ↑((subtypePerm g hgc') { val := x, property := hx })
Tactic:
simp only [Equiv.Perm.subtypePermOfSupport, Subtype.coe_mk, Equiv.Perm.subtypePerm_apply]
State after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = g x

State before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = g x
Tactic:
rw [Equiv.Perm.subtypePerm_apply_zpow_of_mem]
State after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ (c ^ i) x = g x

State before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ (c ^ i) x = g x
Tactic:
suffices c.SameCycle a x by
  obtain ⟨j, rfl⟩ := this
  simp only [← Equiv.Perm.mul_apply, Commute.eq (Commute.zpow_right hgc j)]
  rw [← zpow_add, add_comm i j, zpow_add]
  simp only [Equiv.Perm.mul_apply]
  simp only [EmbeddingLike.apply_eq_iff_eq]
  exact hi
State after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ SameCycle c a x

State before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ SameCycle c a x
Tactic:
exact hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
this : SameCycle c a x
⊢ (c ^ i) x = g x
Tactic:
obtain ⟨j, rfl⟩ := this
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) ((c ^ j) a) = g ((c ^ j) a)

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) ((c ^ j) a) = g ((c ^ j) a)
Tactic:
simp only [← Equiv.Perm.mul_apply, Commute.eq (Commute.zpow_right hgc j)]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i * c ^ j) a = (c ^ j * g) a

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i * c ^ j) a = (c ^ j * g) a
Tactic:
rw [← zpow_add, add_comm i j, zpow_add]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a
Tactic:
simp only [Equiv.Perm.mul_apply]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j) ((c ^ i) a) = (c ^ j) (g a)

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j) ((c ^ i) a) = (c ^ j) (g a)
Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) a = g a

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) a = g a
Tactic:
exact hi
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
      subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) →
    Commute g c
Tactic:
rintro ⟨hc', h⟩
State after:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
h : subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
⊢ Commute g c

State before:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
h : subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
⊢ Commute g c
Tactic:
obtain ⟨i, hi⟩ := h
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
⊢ Commute g c

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
⊢ ∀ x ∈ support c, g x = (c ^ i) x
Tactic:
intro x hx
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
⊢ g x = (c ^ i) x

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
⊢ g x = (c ^ i) x
Tactic:
let hix := Equiv.Perm.congr_fun hi ⟨x, hx⟩
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx } =
  (subtypePerm g hc') { val := x, property := hx } :=
  Perm.congr_fun hi { val := x, property := hx }
⊢ g x = (c ^ i) x

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx } =
  (subtypePerm g hc') { val := x, property := hx } :=
  Perm.congr_fun hi { val := x, property := hx }
⊢ g x = (c ^ i) x
Tactic:
simp only [← Subtype.coe_inj, Equiv.Perm.subtypePermOfSupport] at hix
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = ↑((subtypePerm g hc') { val := x, property := hx })
⊢ g x = (c ^ i) x

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = ↑((subtypePerm g hc') { val := x, property := hx })
⊢ g x = (c ^ i) x
Tactic:
simp only [Subtype.coe_mk, Equiv.Perm.subtypePerm_apply,
  Equiv.Perm.subtypePerm_apply_zpow_of_mem] at hix
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : (c ^ i) x = g x
⊢ g x = (c ^ i) x

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : (c ^ i) x = g x
⊢ g x = (c ^ i) x
Tactic:
exact hix.symm
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
⊢ Commute g c
Tactic:
ext x
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ (g * c) x = (c * g) x

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ (g * c) x = (c * g) x
Tactic:
simp only [Equiv.Perm.coe_mul, Function.comp_apply]
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ g (c x) = c (g x)

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ g (c x) = c (g x)
Tactic:
by_cases hx : x ∈ c.support
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c (g x)

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

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c (g x)
Tactic:
rw [hi' x hx]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c ((c ^ i) x)

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c ((c ^ i) x)
Tactic:
rw [hi' (c x) (apply_mem_support.mpr hx)]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ i) (c x) = c ((c ^ i) x)

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ i) (c x) = c ((c ^ i) x)
Tactic:
simp only [← Equiv.Perm.mul_apply, ← zpow_add_one, ← zpow_one_add]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ (i + 1)) x = (c ^ (1 + i)) x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ (i + 1)) x = (c ^ (1 + i)) x
Tactic:
rw [Int.add_comm 1 i]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g (c x) = c (g x)
Tactic:
rw [not_mem_support.mp hx]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g x = c (g x)

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

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ c (g x) = g x
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g x ∉ support c

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

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

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
hx' : g x ∈ support c
⊢ x ∈ support c
Tactic:
exact (hc' x).mpr hx'
State after:
no goals