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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ↑(MonoidHom.range (φ g)) = {τ | fsc ∘ ⇑τ = fsc}
Tactic:
rw [← Iφ_eq_range]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ↑(Iφ g) = {τ | fsc ∘ ⇑τ = fsc}

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ↑(Iφ g) = {τ | fsc ∘ ⇑τ = fsc}
Tactic:
ext τ
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ τ ∈ {τ | fsc ∘ ⇑τ = fsc}

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ τ ∈ {τ | fsc ∘ ⇑τ = fsc}
Tactic:
simp only [Finset.coe_sort_coe, Set.mem_setOf_eq, Function.funext_iff, Function.comp_apply]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ τ ∈ ↑(Iφ g) ↔ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a
Tactic:
simp only [SetLike.mem_coe, mem_Iφ_iff]
State after:
case h
α : 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) ↔
    ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a

State before:
case h
α : 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) ↔
    ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), fsc (τ a) = fsc a
Tactic:
apply forall_congr'
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(τ a)).card = (Equiv.Perm.support ↑a).card ↔ fsc (τ a) = fsc a

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
τ : Equiv.Perm ↑↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ∀ (a : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(τ a)).card = (Equiv.Perm.support ↑a).card ↔ fsc (τ a) = fsc a
Tactic:
intro c
State after:
case h.h
α : 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 ↔ fsc (τ c) = fsc c

State before:
case h.h
α : 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 ↔ fsc (τ c) = fsc c
Tactic:
simp only [← Function.Injective.eq_iff Fin.val_injective, fsc]
State after:
no goals