Theorem: OnCycleFactors.mem_Iφ_iff (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g ↔
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
simp only [Iφ]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈
      {
        toSubmonoid :=
          {
            toSubsemigroup :=
              {
                carrier :=
                  {τ |
                    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
                      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card},
                mul_mem' := ⋯ },
            one_mem' := ⋯ },
        inv_mem' := ⋯ } ↔
    ∀ (c : { x // x ∈ 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 { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈
      {
        toSubmonoid :=
          {
            toSubsemigroup :=
              {
                carrier :=
                  {τ |
                    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
                      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card},
                mul_mem' := ⋯ },
            one_mem' := ⋯ },
        inv_mem' := ⋯ } ↔
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
rfl
State after:
no goals