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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Nat.card ↥(MonoidHom.range (φ g)) = Fintype.card ↑{k | fsc ∘ ⇑k = fsc}
Tactic:
simp_rw [← hφ_range', Nat.card_eq_fintype_card]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) = Fintype.card ↑↑(MonoidHom.range (φ g))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) = Fintype.card ↑↑(MonoidHom.range (φ g))
Tactic:
rfl
State after:
no goals