-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem CycleType.count_def {σ : Perm α} (n : ℕ) :
    σ.cycleType.count n =
      Fintype.card {c : σ.cycleFactorsFinset // (c : Perm α).support.card = n }

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ Multiset.count n σ.cycleType = Fintype.card { c // (↑c).support.card = n }

Tactic:
rw [cycleType, Multiset.count_eq_card_filter_eq]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x => n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    Fintype.card { c // (↑c).support.card = n }

Proof state:
case e_a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
d : Perm α
h : d ∈ σ.cycleFactorsFinset.val
⊢ n = d.support.val.card ↔ ∃ (_ : d ∈ σ.cycleFactorsFinset), d.support.val.card = n

Tactic:
simp only [Function.comp_apply, eq_comm, Finset.mem_val.mp h, exists_const]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x => n = x.support.val.card) σ.cycleFactorsFinset.val).card =
    (Multiset.filter (fun x => ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n) σ.cycleFactorsFinset.val).card

Tactic:
congr 1

Result:
case e_a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ Multiset.filter (fun x => n = x.support.val.card) σ.cycleFactorsFinset.val =
    Multiset.filter (fun x => ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n) σ.cycleFactorsFinset.val

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x => n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    (Finset.filter (fun x => ∃ (h : x ∈ σ.cycleFactorsFinset), (↑⟨x, h⟩).support.card = n) σ.cycleFactorsFinset).card

Tactic:
simp only [Function.comp_apply, Finset.card, Finset.filter_val,
  Multiset.filter_map, Multiset.card_map]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x => n = x.support.val.card) σ.cycleFactorsFinset.val).card =
    (Multiset.filter (fun x => ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n) σ.cycleFactorsFinset.val).card

Proof state:
case e_a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ ∀ x ∈ σ.cycleFactorsFinset.val, n = x.support.val.card ↔ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n

Tactic:
intro d h

Result:
case e_a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
d : Perm α
h : d ∈ σ.cycleFactorsFinset.val
⊢ n = d.support.val.card ↔ ∃ (_ : d ∈ σ.cycleFactorsFinset), d.support.val.card = n

Proof state:
case e_a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ Multiset.filter (fun x => n = x.support.val.card) σ.cycleFactorsFinset.val =
    Multiset.filter (fun x => ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n) σ.cycleFactorsFinset.val

Tactic:
apply Multiset.filter_congr

Result:
case e_a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ ∀ x ∈ σ.cycleFactorsFinset.val, n = x.support.val.card ↔ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x => n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    Fintype.card { c // (↑c).support.card = n }

Tactic:
rw [Fintype.subtype_card, Finset.univ_eq_attach, Finset.filter_attach',
  Finset.card_map, Finset.card_attach]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x => n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    (Finset.filter (fun x => ∃ (h : x ∈ σ.cycleFactorsFinset), (↑⟨x, h⟩).support.card = n) σ.cycleFactorsFinset).card