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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ ↑c = Equiv.Perm.cycleOf g x ↔ Equiv.Perm.SameCycle g y x
Tactic:
rw [Equiv.Perm.cycle_is_cycleOf hy c.prop]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x ↔ Equiv.Perm.SameCycle g y x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x ↔ Equiv.Perm.SameCycle g y x
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x → Equiv.Perm.SameCycle g y x

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.SameCycle g y x → Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x → Equiv.Perm.SameCycle g y x
Tactic:
intro hx'
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x
Tactic:
apply And.left
State after:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x ∧ ?mp.b

case mp.b
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Prop

State before:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Equiv.Perm.SameCycle g y x ∧ ?mp.b

case mp.b
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ Prop
Tactic:
rw [← Equiv.Perm.mem_support_cycleOf_iff]
State after:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g y)

State before:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support (Equiv.Perm.cycleOf g y)
Tactic:
rw [hx', Equiv.Perm.mem_support, Equiv.Perm.cycleOf_apply_self, ← Equiv.Perm.mem_support]
State after:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support g

State before:
case mp.self
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hx' : Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
⊢ x ∈ Equiv.Perm.support g
Tactic:
exact hx
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
⊢ Equiv.Perm.SameCycle g y x → Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
Tactic:
intro hxy
State after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hxy : Equiv.Perm.SameCycle g y x
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : x ∈ Equiv.Perm.support g
hy : y ∈ Equiv.Perm.support ↑c
hxy : Equiv.Perm.SameCycle g y x
⊢ Equiv.Perm.cycleOf g y = Equiv.Perm.cycleOf g x
Tactic:
rw [Equiv.Perm.SameCycle.cycleOf_eq hxy]
State after:
no goals