awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) a : α) :
          α) :
      α)
have pos : Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
  ((swap a ((g : (a : α) → α) a) : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) : α)
Tactic: rw [swap_apply_left, swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
pos :
  Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) a : α) :
          α) :
      α)
have pos₁ : Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
Tactic: rw [swap_apply_left, swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) :
          α) :
      α)
have pos : (g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) = a
Tactic: simp only [swap_apply_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ (g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) = a
have pos : (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a
Tactic: suffices (g ^ 3) a = a by simpa
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have neg : Eq (α := α) ((g : (a : α) → α) x : α) ((swap a ((g : (a : α) → α) a) : (a : α) → α) x : α)
Tactic: rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
⊢ Eq (α := α) ((g : (a : α) → α) x : α) ((swap a ((g : (a : α) → α) a) : (a : α) → α) x : α)
have neg : (g : (a : α) → α) x = x
Tactic: rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
have pos : ∀ (bc : b = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
Tactic: by_cases bc : b = c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
pos :
  ∀ (bc : b = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
have neg : ∀ (bc : ¬b = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
Tactic: by_cases bc : b = c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b = c
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
have pos : ∀ (ac : a ≠ b), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a b)
Tactic: subst bc
Cleared hypotheses: c, ac, bc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsSwap
hτ : τ.IsSwap
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (σ * τ)
have obtain : ∀ (a b : α) (ab : a ≠ b), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * τ)
Tactic: obtain ⟨a, b, ab, rfl⟩ := hσ
Cleared hypotheses: σ, hσ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : Perm α
hτ : τ.IsSwap
a b : α
ab : a ≠ b
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * τ)
have obtain : ∀ (c d : α) (cd : c ≠ d),
  Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
Tactic: obtain ⟨c, d, cd, rfl⟩ := hτ
Cleared hypotheses: τ, hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
have pos : ∀ (ac : a = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
Tactic: by_cases ac : a = c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
pos :
  ∀ (ac : a = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
have neg : ∀ (ac : ¬a = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
Tactic: by_cases ac : a = c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : a = c
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
have pos : ∀ (cd : a ≠ d), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a d)
Tactic: subst ac
Cleared hypotheses: c, cd, ac
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
Tactic: have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d) := by
    simp [swap_comm c a, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
have neg : Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle})
  (swap a b * swap a c * (swap c a * swap c d))
Tactic: rw [h']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y * swap z t).cycleType = {2, 2}
have rw : (swap x y).cycleType + (swap z t).cycleType = {2, 2}
Tactic: rw [(disjoint_swap_swap h).cycleType_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).cycleType + (swap z t).cycleType = {2, 2}
have rw : HAdd.hAdd (α := Multiset ℕ) {2} {2} = {2, 2}
Tactic: rw [isSwap_iff_cycleType.mp ?_, isSwap_iff_cycleType.mp ?_]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
rw : HAdd.hAdd (α := Multiset ℕ) {2} {2} = {2, 2}
⊢ (swap x y).cycleType + (swap z t).cycleType = {2, 2}
have rw₁ : (swap z t).IsSwap
Tactic: rw [isSwap_iff_cycleType.mp ?_, isSwap_iff_cycleType.mp ?_]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
rw : HAdd.hAdd (α := Multiset ℕ) {2} {2} = {2, 2}
rw₁ : (swap z t).IsSwap
⊢ (swap x y).cycleType + (swap z t).cycleType = {2, 2}
have rw₂ : (swap x y).IsSwap
Tactic: rw [isSwap_iff_cycleType.mp ?_, isSwap_iff_cycleType.mp ?_]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap z t).IsSwap
have rw : z ≠ t
Tactic: rw [swap_isSwap_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).IsSwap
have rw : x ≠ y
Tactic: rw [swap_isSwap_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
i : ι
h : f a = i
⊢ 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)) : α)
have 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 sorry)) :
    α)
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ stabilizerEquiv_invFun (f := f) (fun (i : ι) ↦ Equiv.symm (g i)) (stabilizerEquiv_invFun g a) = a
have 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) sorry)) :
    α) =
  a
Tactic: rw [stabilizerEquiv_invFun_eq _ (comp_stabilizerEquiv_invFun g a)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ stabilizerEquiv_invFun g (stabilizerEquiv_invFun (f := f) (fun (i : ι) ↦ Equiv.symm (g i)) a) = a
have 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) sorry)) :
    α) =
  a
Tactic: rw [stabilizerEquiv_invFun_eq _ (comp_stabilizerEquiv_invFun _ a)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ
i : ι
a : α
⊢ f ((((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ) : Perm α) : (a : α) → α) a) =
      i ↔
    f a = i
have rw : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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
⊢ f ((((Equiv.symm mk : (a : (Perm α)ᵈᵐᵃ) → Perm α) (↑(MulOpposite.unop g) : (Perm α)ᵈᵐᵃ) : Perm α) : (a : α) → α) a) =
      i ↔
    f a = i
have rw₁ : f a = i ↔ f a = i
Tactic: rw [← Function.comp_apply (f := f), mem_stabilizer_iff.mp g.unop.prop]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
⊢ Membership.mem (α := (Perm α)ᵈᵐᵃ) (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f)
    ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g) : (Perm α)ᵈᵐᵃ)
have h : ∀ (a : α),
  HSMul.hSMul (α := (Perm α)ᵈᵐᵃ) ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g) : (Perm α)ᵈᵐᵃ) f a =
    f a
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
a : α
⊢ HSMul.hSMul (α := (Perm α)ᵈᵐᵃ) ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) (stabilizerEquiv_invFun_aux g) : (Perm α)ᵈᵐᵃ) f a =
    f a
have h : f ((stabilizerEquiv_invFun_aux g : (a : α) → α) a) = f a
Tactic: rw [smul_apply, symm_apply_apply, Perm.smul_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a : α // f a = i }
⊢ (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
have 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 α)ᵈᵐᵃ)) sorry :
                  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)) sorry } :
                    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: ext i a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
inst_3 : Fintype ι
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ i : ι, (Fintype.card.{u_1} { a : α // f a = i })!
have rw : Eq (α := ℕ) (∏ a : ι, Nat.card.{u_1} (Perm { a_1 : α // f a_1 = a }))
  (∏ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 })!)
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ i : ι, (Fintype.card.{u_1} { a : α // f a = i })!
have rw₁ : ∀ (x : Perm α),
  f ∘ (⇑x : (a : α) → α) = f ↔
    Membership.mem (α := (Perm α)ᵈᵐᵃ) (γ := Subgroup (Perm α)ᵈᵐᵃ) (stabilizer (Perm α)ᵈᵐᵃ f)
      ((mk : (a : Perm α) → (Perm α)ᵈᵐᵃ) x : (Perm α)ᵈᵐᵃ)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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
⊢ Nat.card.{u_1} (Perm { a : α // f a = i }) = (Fintype.card.{u_1} { a : α // f a = i })!
have rw : Fintype.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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 })!
⊢ Nat.card.{u_1} (Perm { a : α // f a = i }) = (Fintype.card.{u_1} { a : α // f a = i })!
have rw₁ : (Fintype.card.{u_1} { a : α // f a = i })! = (Fintype.card.{u_1} { a : α // f a = i })!
Tactic: rw [Nat.card_eq_fintype_card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
⊢ Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
    ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!
have intro : ∀ (val : Fintype α),
  Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
    ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
val : Fintype α
⊢ Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
    ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!
have intro : Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ x : ι, (Fintype.card.{u_1} { a : α // f a = x })!
Tactic: simp only [← Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Finite α
inst_1 : Fintype ι
⊢ Set.ncard.{u_1} (α := Perm α) {g : Perm α | f ∘ (⇑g : (a : α) → α) = f} =
    ∏ i : ι, (Set.ncard.{u_1} (α := α) {a : α | f a = i})!
have intro : ∀ (val : Fintype α),
  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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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})!
have intro₁ : ∀ (val : Fintype α),
  Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } = ∏ x : ι, (Fintype.card.{u_1} { a : α // f a = x })!
Tactic: classical
  cases nonempty_fintype α
  simp only [← Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]
  exact stabilizer_card f
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 : α) → α) = φ
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } =
    ∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!
have 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 })!)
Tactic: simp only [this, stabilizer_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 : α) → α) = φ
⊢ 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 })!)
have 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
Tactic: apply Finset.prod_bij (fun g _ => g.val)