-- 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 ι
φ : α → { x // x ∈ Finset.image f Finset.univ } := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
g : ι
hg : g ∈ Finset.image f Finset.univ
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = g

Tactic:
rw [Finset.mem_image] at hg

Result:
α : 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

Proof state:
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

Tactic:
exact fun g _ => Finset.coe_mem g

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) ⋯
⊢ ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ

Tactic:
intro g

Result:
α : 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) ⋯
g : Perm α
⊢ f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ

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) ⋯
g : Perm α
a : α
⊢ (f ∘ ⇑g) a = f a ↔ (φ ∘ ⇑g) a = φ a

Tactic:
simp only [Function.comp_apply, φ, ← Subtype.coe_inj, Set.val_codRestrict_apply]

Result:
no goals

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:
rw [refl_apply, ← Subtype.coe_inj]

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 a = ↑i

Proof state:
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₂

Tactic:
exact fun g _ g' _ =>  SetCoe.ext

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 = φ
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ i ∈ Finset.image f Finset.univ, (Fintype.card { a // f a = i })!

Tactic:
simp only [this, stabilizer_card]

Result:
α : 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 })!

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) ⋯
g : Perm α
⊢ (∀ (x : α), (f ∘ ⇑g) x = f x) ↔ ∀ (x : α), (φ ∘ ⇑g) x = φ x

Tactic:
apply forall_congr'

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) ⋯
g : Perm α
⊢ ∀ (a : α), (f ∘ ⇑g) a = f a ↔ (φ ∘ ⇑g) a = φ 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 a = ↑i

Tactic:
simp only [φ, Set.val_codRestrict_apply]

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) ⋯
g : Perm α
⊢ ∀ (a : α), (f ∘ ⇑g) a = f a ↔ (φ ∘ ⇑g) a = φ a

Tactic:
intro a

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) ⋯
g : Perm α
a : α
⊢ (f ∘ ⇑g) a = f a ↔ (φ ∘ ⇑g) a = φ 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 ∈ Finset.univ, (Fintype.card { a_1 // φ a_1 = a })! = (Fintype.card { a_1 // f a_1 = ↑a })!

Tactic:
intro i _

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 = φ
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:
α : 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) ⋯
g : Perm α
⊢ f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ

Tactic:
simp only [funext_iff]

Result:
α : 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) ⋯
g : Perm α
⊢ (∀ (x : α), (f ∘ ⇑g) x = f x) ↔ ∀ (x : α), (φ ∘ ⇑g) x = φ x

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ i ∈ Finset.image f Finset.univ, (Fintype.card { a // f a = i })!

Tactic:
set φ : α → Finset.univ.image f :=
  Set.codRestrict f (Finset.univ.image f) (fun a => by simp)

Result:
α : 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) ⋯
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ i ∈ Finset.image f Finset.univ, (Fintype.card { a // f a = i })!