awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ x ≠ y

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g • f = f ↔ f ∘ (⇑((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) g : Perm α) : (a : α) → α) = f

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
i : ι
h : f a = i
subst :
  stabilizerEquiv_invFun g a =
    (↑((g (f a) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a) a ⋯)) :
      α)
⊢ stabilizerEquiv_invFun g a =
    (↑((g i : (a : { a : α // f a = i }) → { a : α // f a = i }) (Subtype.mk (p := fun (a : α) ↦ f a = i) a h)) : α)

Tactic:
subst h
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ stabilizerEquiv_invFun g a =
    (↑((g (f a) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a) a ⋯)) :
      α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ f (stabilizerEquiv_invFun g a) = f a

Tactic:
(g (f a) ⟨a, rfl⟩).prop

Premises used: DomMulAct.stabilizerEquiv_invFun, Subtype.mk, Subtype.prop, DFunLike.coe, rfl
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
rw :
  (↑((Equiv.symm (g (f a)) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a) (stabilizerEquiv_invFun g a) ⋯)) :
      α) =
    a
⊢ stabilizerEquiv_invFun (f := f) (fun (i : ι) ↦ Equiv.symm (g i)) (stabilizerEquiv_invFun g a) = a

Tactic:
rw [stabilizerEquiv_invFun_eq _ (comp_stabilizerEquiv_invFun g a)]

Premises used: DomMulAct.comp_stabilizerEquiv_invFun, DomMulAct.stabilizerEquiv_invFun_eq
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ (↑((Equiv.symm (g (f a)) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a) (stabilizerEquiv_invFun g a) ⋯)) :
      α) =
    a

Tactic:
congr_arg Subtype.val ((g <| f a).left_inv _)

Premises used: DomMulAct.stabilizerEquiv_invFun, congr_arg, Subtype.val, Equiv.left_inv
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ (↑((Equiv.symm (g (f a)) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a) (stabilizerEquiv_invFun g a) ⋯)) :
      α) =
    a

Tactic:
exact congr_arg Subtype.val ((g <| f a).left_inv _)

Premises used: congr_arg, Subtype.val, Equiv.left_inv
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
rw :
  (↑((g (f a) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a)
            (stabilizerEquiv_invFun (f := f) (fun (i : ι) ↦ Equiv.symm (g i)) a) ⋯)) :
      α) =
    a
⊢ stabilizerEquiv_invFun g (stabilizerEquiv_invFun (f := f) (fun (i : ι) ↦ Equiv.symm (g i)) a) = a

Tactic:
rw [stabilizerEquiv_invFun_eq _ (comp_stabilizerEquiv_invFun _ a)]

Premises used: DomMulAct.comp_stabilizerEquiv_invFun, DomMulAct.stabilizerEquiv_invFun_eq
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ (↑((g (f a) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a)
            (stabilizerEquiv_invFun (f := f) (fun (i : ι) ↦ Equiv.symm (g i)) a) ⋯)) :
      α) =
    a

Tactic:
congr_arg Subtype.val ((g <| f a).right_inv _)

Premises used: Equiv.right_inv, DomMulAct.stabilizerEquiv_invFun, congr_arg, Subtype.val
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ (↑((g (f a) : (a_1 : { a_1 : α // f a_1 = f a }) → { a_2 : α // f a_2 = f a })
          (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a)
            (stabilizerEquiv_invFun (f := f) (fun (i : ι) ↦ Equiv.symm (g i)) a) ⋯)) :
      α) =
    a

Tactic:
exact congr_arg Subtype.val ((g <| f a).right_inv _)

Premises used: Equiv.right_inv, congr_arg, Subtype.val
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ
i : ι
a : α
rw :
  (f ∘ (⇑((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ) : Perm α) : (a : α) → α))
        a =
      i ↔
    f a = i
rw₁ rw₂ : f a = i ↔ f a = i
⊢ f ((((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ) : Perm α) : (a : α) → α) a) =
      i ↔
    f a = i

Tactic:
rw [← Function.comp_apply (f := f), mem_stabilizer_iff.mp g.unop.prop]

Premises used: DomMulAct.mem_stabilizer_iff, Subtype.prop, Iff.mp, MulOpposite.unop, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
h :
  ∀ (a : α),
    HSMul.hSMul (α := (Perm α)ᵈᵐᵃ) ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g) : (Perm α)ᵈᵐᵃ) f
        a =
      f a
⊢ Membership.mem (α := (Perm α)ᵈᵐᵃ) (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f)
    ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g) : (Perm α)ᵈᵐᵃ)

Tactic:
ext a
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
h : f ((stabilizerEquiv_invFun_aux g : (a : α) → α) a) = f a
⊢ HSMul.hSMul (α := (Perm α)ᵈᵐᵃ) ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g) : (Perm α)ᵈᵐᵃ) f a =
    f a

Tactic:
rw [smul_apply, symm_apply_apply, Perm.smul_def]

Premises used: Equiv.Perm.smul_def, Equiv.symm_apply_apply, DomMulAct.smul_apply
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ f ((stabilizerEquiv_invFun_aux g : (a : α) → α) a) = f a

Tactic:
apply comp_stabilizerEquiv_invFun

Premises used: DomMulAct.comp_stabilizerEquiv_invFun
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
h :
  ∀ (i : ι) (a : { x : α // f x = i }),
    Eq.{u_1 + 1} (α := α)
      (↑(((fun (g : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ) (i : ι) ↦
                  (Perm.subtypePerm (p := fun (a : α) ↦ f a = i)
                      ((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ)) ⋯ :
                    Perm { x : α // f x = i }))
                ((fun (g : (i : ι) → Perm { a : α // f a = i }) ↦
                    ({
                        unop' :=
                          Subtype.mk (p := fun (x : (Perm α)ᵈᵐᵃ) ↦
                            Membership.mem (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f) x)
                            ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g)) ⋯ } :
                      PreOpposite ↥(stabilizer (Perm α)ᵈᵐᵃ f)))
                  g)
                i :
              (a : { x : α // f x = i }) → { x : α // f x = i })
            a) :
        α)
      (↑((g i : (a : { x : α // f x = i }) → { x : α // f x = i }) a) : α)
⊢ (fun (g : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ) (i : ι) ↦
        (Perm.subtypePerm (p := fun (a : α) ↦ f a = i)
            ((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ)) ⋯ :
          Perm { x : α // f x = i }))
      ((fun (g : (i : ι) → Perm { a : α // f a = i }) ↦
          ({
              unop' :=
                Subtype.mk (p := fun (x : (Perm α)ᵈᵐᵃ) ↦
                  Membership.mem (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f) x)
                  ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g)) ⋯ } :
            PreOpposite ↥(stabilizer (Perm α)ᵈᵐᵃ f)))
        g) =
    g

Tactic:
ext i a
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
i : ι
a : { x : α // f x = i }
⊢ Eq.{u_1 + 1} (α := α)
    (↑(((fun (g : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ) (i : ι) ↦
                (Perm.subtypePerm (p := fun (a : α) ↦ f a = i)
                    ((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ)) ⋯ :
                  Perm { x : α // f x = i }))
              ((fun (g : (i : ι) → Perm { a : α // f a = i }) ↦
                  ({
                      unop' :=
                        Subtype.mk (p := fun (x : (Perm α)ᵈᵐᵃ) ↦
                          Membership.mem (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f) x)
                          ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g)) ⋯ } :
                    PreOpposite ↥(stabilizer (Perm α)ᵈᵐᵃ f)))
                g)
              i :
            (a : { x : α // f x = i }) → { x : α // f x = i })
          a) :
      α)
    (↑((g i : (a : { x : α // f x = i }) → { x : α // f x = i }) a) : α)

Tactic:
apply stabilizerEquiv_invFun_eq

Premises used: DomMulAct.stabilizerEquiv_invFun_eq
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ
a : α
i : ι
h : f a = i
⊢ Eq (α := α)
    ((↑((((stabilizerMulEquiv f : (a : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ) → (i : ι) → Perm { a : α // f a = i }) g i :
                Perm { a : α // f a = i }) :
              (a : { a : α // f a = i }) → { a : α // f a = i })
            (Subtype.mk (p := fun (a : α) ↦ f a = i) a h)) :
        α) :
      α)
    ((((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ) : Perm α) : (a : α) → α) a :
      α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
inst_3 : Fintype ι
rw :
  Eq (α := ℕ) (∏ a : ι, Nat.card.{u_1} (Perm { a_1 : α // f a_1 = a }))
    (∏ i : ι, (Fintype.card.{u_1} { a : α // f a = i })!)
rw₁ :
  ∀ (x : Perm α),
    f ∘ (⇑x : (a : α) → α) = f ↔
      Membership.mem (α := (Perm α)ᵈᵐᵃ) (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f)
        ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) x : (Perm α)ᵈᵐᵃ)
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ i : ι, (Fintype.card.{u_1} { a : α // f a = i })!

Tactic:
rw [← Nat.card_eq_fintype_card,
    Nat.card_congr (subtypeEquiv mk fun _ ↦ ?_),
    Nat.card_congr MulOpposite.opEquiv,
    Nat.card_congr (DomMulAct.stabilizerMulEquiv f).toEquiv, Nat.card_pi]

Premises used: MulOpposite.opEquiv, Equiv.subtypeEquiv, MulEquiv.toEquiv, DomMulAct.mk, DomMulAct.stabilizerMulEquiv, Nat.card_congr, Nat.card_pi, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
inst_3 : Fintype ι
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
rw : Fintype.card.{u_1} (Perm { a : α // f a = i }) = (Fintype.card.{u_1} { a : α // f a = i })!
rw₁ rw₂ : (Fintype.card.{u_1} { a : α // f a = i })! = (Fintype.card.{u_1} { a : α // f a = i })!
⊢ Nat.card.{u_1} (Perm { a : α // f a = i }) = (Fintype.card.{u_1} { a : α // f a = i })!

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_perm]

Premises used: Fintype.card_perm, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
inst_3 : Fintype ι
⊢ Eq (α := ℕ) (∏ a : ι, Nat.card.{u_1} (Perm { a_1 : α // f a_1 = a }))
    (∏ i : ι, (Fintype.card.{u_1} { a : α // f a = i })!)

Tactic:
exact Finset.prod_congr rfl fun i _ ↦ by rw [Nat.card_eq_fintype_card, Fintype.card_perm]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
inst_3 : Fintype ι
x : Perm α
⊢ f ∘ (⇑x : (a : α) → α) = f ↔
    Membership.mem (α := (Perm α)ᵈᵐᵃ) (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f)
      ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) x : (Perm α)ᵈᵐᵃ)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
intro :
  ∀ (val : Fintype α),
    Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
      ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!
⊢ Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
    ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
val : Fintype α
intro :
  Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ x : ι, (Fintype.card.{u_1} { a : α // f a = x })!
⊢ Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
    ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!

Tactic:
simp only [← Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]

Premises used: Nat.card_coe_set_eq, Set.coe_setOf, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
val : Fintype α
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ x : ι, (Fintype.card.{u_1} { a : α // f a = x })!

Tactic:
stabilizer_card f

Premises used: DomMulAct.stabilizer_card
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
val : Fintype α
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ x : ι, (Fintype.card.{u_1} { a : α // f a = x })!

Tactic:
exact stabilizer_card f

Premises used: DomMulAct.stabilizer_card
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
intro :
  ∀ (val : Fintype α),
    Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
      ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!
intro₁ :
  ∀ (val : Fintype α),
    Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } =
      ∏ x : ι, (Fintype.card.{u_1} { a : α // f a = x })!
⊢ Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
    ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!

Tactic:
classical
  cases nonempty_fintype α
  simp only [← Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]
  exact stabilizer_card f

Premises used: Nat.card_coe_set_eq, nonempty_fintype, Set.coe_setOf, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
a : α
⊢ f a ∈ (↑(Finset.image f Finset.univ) : Set ι)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
simp :
  Eq (α := ℕ) (∏ i : ↥(Finset.image f Finset.univ), (Fintype.card.{u_1} { a : α // φ a = i })!)
    (∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!)
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } =
    ∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!

Tactic:
simp only [this, stabilizer_card]

Premises used: DomMulAct.stabilizer_card
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
hi :
  ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (↑a : ι) ∈ Finset.image f Finset.univ
i_inj :
  ∀ (a₁ : ↥(Finset.image f Finset.univ))
    (ha₁ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₁)
    (a₂ : ↥(Finset.image f Finset.univ))
    (ha₂ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₂), (↑a₁ : ι) = (↑a₂ : ι) → a₁ = a₂
i_surj :
  ∀ b ∈ Finset.image f Finset.univ,
    ∃ (a : ↥(Finset.image f Finset.univ)) (_ :
      Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a), (↑a : ι) = b
h :
  ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (Fintype.card.{u_1} { a_1 : α // φ a_1 = a })! = (Fintype.card.{u_1} { a_1 : α // f a_1 = (↑a : ι) })!
⊢ Eq (α := ℕ) (∏ i : ↥(Finset.image f Finset.univ), (Fintype.card.{u_1} { a : α // φ a = i })!)
    (∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!)

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

Premises used: Finset.prod_bij
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
⊢ ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (↑a : ι) ∈ Finset.image f Finset.univ

Tactic:
fun g _ => Finset.coe_mem g

Premises used: Set.Mem, Finset.coe_mem, setOf
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
⊢ ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (↑a : ι) ∈ Finset.image f Finset.univ

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

Premises used: Finset.coe_mem
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
⊢ ∀ (a₁ : ↥(Finset.image f Finset.univ))
    (ha₁ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₁)
    (a₂ : ↥(Finset.image f Finset.univ))
    (ha₂ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₂), (↑a₁ : ι) = (↑a₂ : ι) → a₁ = a₂

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

Premises used: SetCoe.ext
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
⊢ ∀ (a₁ : ↥(Finset.image f Finset.univ))
    (ha₁ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₁)
    (a₂ : ↥(Finset.image f Finset.univ))
    (ha₂ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₂), (↑a₁ : ι) = (↑a₂ : ι) → a₁ = a₂

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

Premises used: SetCoe.ext
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
⊢ ∀ b ∈ Finset.image f Finset.univ,
    ∃ (a : ↥(Finset.image f Finset.univ)) (_ :
      Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a), (↑a : ι) = b

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
i : ↥(Finset.image f Finset.univ)
h :
  Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ i →
    (Fintype.card.{u_1} { a : α // φ a = i })! = (Fintype.card.{u_1} { a : α // f a = (↑i : ι) })!
⊢ ∀ (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ i),
    (Fintype.card.{u_1} { a : α // φ a = i })! = (Fintype.card.{u_1} { a : α // f a = (↑i : ι) })!

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
i : ↥(Finset.image f Finset.univ)
ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ i
h : Fintype.card.{u_1} { a : α // φ a = i } = Fintype.card.{u_1} { a : α // f a = (↑i : ι) }
⊢ (Fintype.card.{u_1} { a : α // φ a = i })! = (Fintype.card.{u_1} { a : α // f a = (↑i : ι) })!

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
i : ↥(Finset.image f Finset.univ)
ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ i
h : { a : α // φ a = i } ≃ { a : α // f a = (↑i : ι) }
⊢ Fintype.card.{u_1} { a : α // φ a = i } = Fintype.card.{u_1} { a : α // f a = (↑i : ι) }

Tactic:
apply Fintype.card_congr

Premises used: Fintype.card_congr
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
i : ↥(Finset.image f Finset.univ)
ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ i
h : ∀ (a : α), φ a = i ↔ f ((Equiv.refl α : (a : α) → α) a) = (↑i : ι)
⊢ { a : α // φ a = i } ≃ { a : α // f a = (↑i : ι) }

Tactic:
apply Equiv.subtypeEquiv (Equiv.refl α)

Premises used: Equiv.subtypeEquiv, Equiv.refl
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
i : ↥(Finset.image f Finset.univ)
ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ i
a : α
h : (↑(φ a) : ι) = (↑i : ι) ↔ f a = (↑i : ι)
⊢ φ a = i ↔ f ((Equiv.refl α : (a : α) → α) a) = (↑i : ι)

Tactic:
rw [refl_apply, ← Subtype.coe_inj]

Premises used: Equiv.refl_apply, Subtype.coe_inj