Theorem: Equiv.Perm.sameCycle_of_mem_support (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∃ c, ∀ y ∈ Equiv.Perm.support ↑c, Equiv.Perm.SameCycle g y x
Tactic:
use ⟨g.cycleOf x, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff.mpr hx⟩
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∀ y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }, Equiv.Perm.SameCycle g y x

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∀ y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }, Equiv.Perm.SameCycle g y x
Tactic:
intro y hy
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
y : α
hy : y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }
⊢ Equiv.Perm.SameCycle g y x

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
x : α
hx : x ∈ Equiv.Perm.support g
y : α
hy : y ∈ Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := ⋯ }
⊢ Equiv.Perm.SameCycle g y x
Tactic:
rw [← Equiv.Perm.eq_cycleOf_iff_sameCycle hx hy]
State after:
no goals