-- Mathlib/GroupTheory/Perm/DomMulAct.lean
theorem stabilizer_card':
    Fintype.card {g : Perm α // f ∘ g = f} =
      ∏ i ∈ Finset.univ.image f, (Fintype.card ({a // f a = i}))!

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
a : α
⊢ f a ∈ ↑(Finset.image f Finset.univ)

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : { x // x ∈ Finset.image f Finset.univ }
ha✝ : i ∈ Finset.univ
⊢ (Fintype.card { a // φ a = i })! = (Fintype.card { a // f a = ↑i })!

Tactic:
apply congr_arg

Result:
case h.h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : { x // x ∈ Finset.image f Finset.univ }
ha✝ : i ∈ Finset.univ
⊢ Fintype.card { a // φ a = i } = Fintype.card { a // f a = ↑i }

Proof state:
case h.h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : { x // x ∈ Finset.image f Finset.univ }
ha✝ : i ∈ Finset.univ
⊢ Fintype.card { a // φ a = i } = Fintype.card { a // f a = ↑i }

Tactic:
apply Fintype.card_congr

Result:
case h.h.f
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : { x // x ∈ Finset.image f Finset.univ }
ha✝ : i ∈ Finset.univ
⊢ { a // φ a = i } ≃ { a // f a = ↑i }

Proof state:
case intro.intro
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
a : α
left✝ : a ∈ Finset.univ
⊢ ∃ a_1, ∃ (_ : a_1 ∈ Finset.univ), ↑a_1 = f a

Tactic:
use ⟨f a, by simp only [Finset.mem_image, Finset.mem_univ, true_and, exists_apply_eq_apply]⟩

Result:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
a : α
left✝ : a ∈ Finset.univ
⊢ ∃ (_ : ⟨f a, ⋯⟩ ∈ Finset.univ), ↑⟨f a, ⋯⟩ = f a

Proof state:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
a : α
left✝ : a ∈ Finset.univ
⊢ ∃ (_ : ⟨f a, ⋯⟩ ∈ Finset.univ), ↑⟨f a, ⋯⟩ = f a

Tactic:
simp only [Finset.univ_eq_attach, Finset.mem_attach, exists_const]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
a : α
left✝ : a ∈ Finset.univ
⊢ f a ∈ Finset.image f Finset.univ

Tactic:
simp only [Finset.mem_image, Finset.mem_univ, true_and, exists_apply_eq_apply]

Result:
no goals

Proof state:
case i_surj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ b ∈ Finset.image f Finset.univ, ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = b

Tactic:
exact fun g hg => by
  rw [Finset.mem_image] at hg
  obtain ⟨a, _, rfl⟩ := hg
  use ⟨f a, by simp only [Finset.mem_image, Finset.mem_univ, true_and, exists_apply_eq_apply]⟩
  simp only [Finset.univ_eq_attach, Finset.mem_attach, exists_const]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∏ i : { x // x ∈ Finset.image f Finset.univ }, (Fintype.card { a // φ a = i })! =
    ∏ i ∈ Finset.image f Finset.univ, (Fintype.card { a // f a = i })!

Tactic:
apply Finset.prod_bij (fun g _ => g.val)

Result:
case hi
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, ↑a ∈ Finset.image f Finset.univ

case i_inj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a₁ ∈ Finset.univ, ∀ a₂ ∈ Finset.univ, ↑a₁ = ↑a₂ → a₁ = a₂

case i_surj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ b ∈ Finset.image f Finset.univ, ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = b

case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, (Fintype.card { a_1 // φ a_1 = a })! = (Fintype.card { a_1 // f a_1 = ↑a })!

Proof state:
case h.h.f
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : { x // x ∈ Finset.image f Finset.univ }
ha✝ : i ∈ Finset.univ
⊢ ∀ (a : α), φ a = i ↔ f ((Equiv.refl α) a) = ↑i

Tactic:
intro a

Result:
case h.h.f
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : { x // x ∈ Finset.image f Finset.univ }
ha✝ : i ∈ Finset.univ
a : α
⊢ φ a = i ↔ f ((Equiv.refl α) a) = ↑i

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
g : ι
hg : ∃ a ∈ Finset.univ, f a = g
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = g

Tactic:
obtain ⟨a, _, rfl⟩ := hg

Result:
case intro.intro
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
a : α
left✝ : a ∈ Finset.univ
⊢ ∃ a_1, ∃ (_ : a_1 ∈ Finset.univ), ↑a_1 = f a