-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem nat_card_range_toPermHom :
    Nat.card (toPermHom g).range =
      ∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)!

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
n : ℕ
⊢ (∃ a ∈ g.cycleFactorsFinset, a.support.card = n) ↔ n ∈ g.cycleType

Tactic:
simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ i ∈ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach,
      (Fintype.card { a // (↑a).support.card = i })! =
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
simp_rw [← CycleType.count_def]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ x ∈ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach, (Multiset.count x g.cycleType)! =
    ∏ x ∈ g.cycleType.toFinset, (Multiset.count x g.cycleType)!

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ x ∈ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach, (Multiset.count x g.cycleType)! =
    ∏ x ∈ g.cycleType.toFinset, (Multiset.count x g.cycleType)!

Tactic:
apply Finset.prod_congr _ (fun _ _ => rfl)

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach = g.cycleType.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
classical
set sc := fun (c : g.cycleFactorsFinset) ↦ c.val.support.card with hsc
suffices Fintype.card (toPermHom g).range =
  Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
  simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
    Finset.univ_eq_attach]
  simp_rw [← CycleType.count_def]
  apply Finset.prod_congr _ (fun _ _ => rfl)
  ext n
  simp only [Finset.univ_eq_attach, Finset.mem_image, Finset.mem_attach,
      hsc, true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
  simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
simp only [← SetLike.coe_sort_coe, Fintype.card_eq_nat_card]
congr
ext
rw [SetLike.mem_coe, mem_range_toPermHom_iff', Set.mem_setOf_eq, ← beq_eq_beq]

Result:
no goals

Proof state:
case e_α.e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
x✝ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ x✝ ∈ ↑(toPermHom g).range ↔ x✝ ∈ {k | sc ∘ ⇑k = sc}

Tactic:
rw [SetLike.mem_coe, mem_range_toPermHom_iff', Set.mem_setOf_eq, ← beq_eq_beq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}

Tactic:
simp only [← SetLike.coe_sort_coe, Fintype.card_eq_nat_card]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ Nat.card ↑↑(toPermHom g).range = Nat.card ↑{k | sc ∘ ⇑k = sc}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach = g.cycleType.toFinset

Tactic:
ext n

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
n : ℕ
⊢ n ∈ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach ↔ n ∈ g.cycleType.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
set sc := fun (c : g.cycleFactorsFinset) ↦ c.val.support.card with hsc

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
n : ℕ
⊢ n ∈ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach ↔ n ∈ g.cycleType.toFinset

Tactic:
simp only [Finset.univ_eq_attach, Finset.mem_image, Finset.mem_attach,
    hsc, true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
n : ℕ
⊢ (∃ a ∈ g.cycleFactorsFinset, a.support.card = n) ↔ n ∈ g.cycleType

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
  Finset.univ_eq_attach]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ i ∈ Finset.image (fun c => (↑c).support.card) g.cycleFactorsFinset.attach,
      (Fintype.card { a // (↑a).support.card = i })! =
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!