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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ MonoidHom.range (φ g) ↔
    ∀ (c : ↑↑(Equiv.Perm.cycleFactorsFinset g)), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
simp only [← Iφ_eq_range, mem_Iφ_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card) ↔
    ∀ (c : ↑↑(Equiv.Perm.cycleFactorsFinset g)), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ (∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card) ↔
    ∀ (c : ↑↑(Equiv.Perm.cycleFactorsFinset g)), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
rfl
State after:
no goals