Theorem: OnCycleFactors.hφ_eq_card_of_mem_range (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
hτ : τ ∈ MonoidHom.range (φ g)
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
obtain ⟨⟨k, hk⟩, rfl⟩ := hτ
State after:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Equiv.Perm.support ↑(((φ g) { val := k, property := hk }) c)).card = (Equiv.Perm.support ↑c).card

State before:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Equiv.Perm.support ↑(((φ g) { val := k, property := hk }) c)).card = (Equiv.Perm.support ↑c).card
Tactic:
rw [φ_eq, ConjAct.smul_def, Equiv.Perm.support_conj]
State after:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Finset.map (Equiv.toEmbedding (ConjAct.ofConjAct k)) (Equiv.Perm.support ↑c)).card = (Equiv.Perm.support ↑c).card

State before:
case intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : ↑↑(Equiv.Perm.cycleFactorsFinset g)
k : ConjAct (Equiv.Perm α)
hk : k ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
⊢ (Finset.map (Equiv.toEmbedding (ConjAct.ofConjAct k)) (Equiv.Perm.support ↑c)).card = (Equiv.Perm.support ↑c).card
Tactic:
apply Finset.card_map
State after:
no goals