Theorem: OnCycleFactors.Equiv.Perm.card_fixedBy (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.fixedBy α g) = Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Tactic:
rw [Equiv.Perm.sum_cycleType, ← Finset.card_compl]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.fixedBy α g) = (Equiv.Perm.support g)ᶜ.card

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.fixedBy α g) = (Equiv.Perm.support g)ᶜ.card
Tactic:
simp only [Fintype.card_ofFinset, Set.mem_compl_iff, Finset.mem_coe,
  Equiv.Perm.mem_support, Classical.not_not]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ).card = (Equiv.Perm.support g)ᶜ.card

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ).card = (Equiv.Perm.support g)ᶜ.card
Tactic:
apply congr_arg
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ = (Equiv.Perm.support g)ᶜ

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ = (Equiv.Perm.support g)ᶜ
Tactic:
ext x
State after:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x : α
⊢ x ∈ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ ↔ x ∈ (Equiv.Perm.support g)ᶜ

State before:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x : α
⊢ x ∈ Finset.filter (fun x => x ∈ MulAction.fixedBy α g) Finset.univ ↔ x ∈ (Equiv.Perm.support g)ᶜ
Tactic:
simp only [MulAction.mem_fixedBy, Equiv.Perm.smul_def, Finset.mem_filter, Finset.mem_univ,
  true_and_iff, Finset.mem_compl, Equiv.Perm.mem_support, Classical.not_not]
State after:
no goals