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), ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Tactic:
rw [Equiv.Perm.IsCycle.commute_iff' hc]
State after:
α : 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)) ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c

State before:
α : 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)) ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Tactic:
apply exists_congr
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ ∀ (a : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
    subtypePerm g a ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g a) ∈ Subgroup.zpowers c

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ ∀ (a : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
    subtypePerm g a ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g a) ∈ Subgroup.zpowers c
Tactic:
intro hc'
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
⊢ subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c

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
⊢ subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c
Tactic:
simp only [Subgroup.mem_zpowers_iff]
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
⊢ (∃ k, subtypePermOfSupport c ^ k = subtypePerm g hc') ↔ ∃ k, c ^ k = ofSubtype (subtypePerm g hc')

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
⊢ (∃ k, subtypePermOfSupport c ^ k = subtypePerm g hc') ↔ ∃ k, c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
apply exists_congr
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm g hc' ↔ c ^ a = ofSubtype (subtypePerm g hc')

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm g hc' ↔ c ^ a = ofSubtype (subtypePerm g hc')
Tactic:
intro k
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePermOfSupport c ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePermOfSupport c ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
unfold subtypePermOfSupport
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm c ⋯ ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm c ⋯ ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
rw [Equiv.Perm.subtypePerm_zpow]
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm (c ^ k) ⋯ = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm (c ^ k) ⋯ = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ (∀ a ∈ support c, (c ^ k) a = g a) ↔ ∀ (x : α), (c ^ k) x = (ofSubtype (subtypePerm g hc')) x

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ (∀ a ∈ support c, (c ^ k) a = g a) ↔ ∀ (x : α), (c ^ k) x = (ofSubtype (subtypePerm g hc')) x
Tactic:
apply forall_congr'
State after:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ ∀ (a : α), a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

State before:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ ∀ (a : α), a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
intro a
State after:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

State before:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
by_cases ha : a ∈ 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
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

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

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
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
rw [imp_iff_right ha]
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
k : ℤ
a : α
ha : a ∈ support c
⊢ (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

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
k : ℤ
a : α
ha : a ∈ support c
⊢ (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
apply Eq.congr rfl
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
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = (ofSubtype (subtypePerm g hc')) a

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
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = (ofSubtype (subtypePerm g hc')) a
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem]
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
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = ↑((subtypePerm g hc') { val := a, property := ?pos.ha✝ })

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

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
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = ↑((subtypePerm g hc') { val := a, property := ?pos.ha✝ })

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c
Tactic:
rfl
State after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c

State before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c
Tactic:
exact ha
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
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
rw [iff_true_left _]
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
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

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
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem]
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
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = a

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

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
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = a

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
rw [←Equiv.Perm.not_mem_support]
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
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support (c ^ k)

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

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
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support (c ^ k)

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
intro ha'
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
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ False

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

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
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ False

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
apply ha
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
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support c

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

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
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support c

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
apply Equiv.Perm.support_zpow_le
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
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support (c ^ ?neg.n✝)

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

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

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
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support (c ^ ?neg.n✝)

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

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
exact ha'
State after:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
exact ha
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
exact fun b => False.elim (ha b)
State after:
no goals