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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ subtypePerm g ⋯ = subtypePermOfSupport c
Tactic:
ext ⟨x, hx⟩
State after:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm g ⋯) { val := x, property := hx }) = ↑((subtypePermOfSupport c) { val := x, property := hx })

State before:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm g ⋯) { val := x, property := hx }) = ↑((subtypePermOfSupport c) { val := x, property := hx })
Tactic:
simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]
State after:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ g x = c x

State before:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ g x = c x
Tactic:
exact ((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm
State after:
no goals