awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ x ≠ 1

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
refine : ∀ (n : ℕ), Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
⊢ ¬IsSolvable (Perm (Fin 5))

Tactic:
refine not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_

Premises used: not_solvable_of_mem_derivedSeries
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) 0) x

Tactic:
mem_top x

Premises used: Set.Mem, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) 0) x

Tactic:
exact mem_top x

Premises used: Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
succ : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) ⁅x, y * x * y⁻¹⁆
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) x

Tactic:
rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]

Premises used: Subgroup.Normal.mem_comm_iff, inv_mul_cancel_left, derivedSeries_normal
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) ⁅x, y * x * y⁻¹⁆

Tactic:
commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)

Premises used: Set.Mem, Subgroup.commutator_mem_commutator, derivedSeries_normal, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) ⁅x, y * x * y⁻¹⁆

Tactic:
exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)

Premises used: Subgroup.commutator_mem_commutator, derivedSeries_normal, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
zero : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) 0) x
succ :
  ∀ (n : ℕ) (ih : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x),
    Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) x
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x

Tactic:
induction n with
  | zero => exact mem_top x
  | succ n ih =>
    rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
    exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)

Premises used: Subgroup.Normal.mem_comm_iff, inv_mul_cancel_left, Subgroup.mem_top, derivedSeries_normal
-- Module: Mathlib.GroupTheory.Solvable
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
rwa : Cardinal.lift.{u_3, 0} (Cardinal.mk (Fin 5)) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
rwa₁ : Cardinal.lift.{u_3, 0} (↑5 : Cardinal.{0}) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
rwa₂ : (↑5 : Cardinal.{u_3}) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
rwa₃ rwa₄ rwa₅ rwa₆ : (↑5 : Cardinal.{u_3}) ≤ Cardinal.mk X
⊢ Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)

Tactic:
rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]

Premises used: Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id
-- Module: Mathlib.GroupTheory.Solvable
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
⊢ Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)

Tactic:
have key : Nonempty (Fin 5 ↪ X) := by
    rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
-- Module: Mathlib.GroupTheory.Solvable
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
key : Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)
⊢ False

Tactic:
Equiv.Perm.fin_5_not_solvable
      (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))

Premises used: Nonempty.some, solvable_of_solvable_injective, Equiv.Perm.fin_5_not_solvable, Equiv.Perm.viaEmbeddingHom_injective
-- Module: Mathlib.GroupTheory.Solvable
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
key : Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)
⊢ False

Tactic:
exact
    Equiv.Perm.fin_5_not_solvable
      (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))

Premises used: Nonempty.some, solvable_of_solvable_injective, Equiv.Perm.fin_5_not_solvable, Equiv.Perm.viaEmbeddingHom_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
i : ℕ
hi : i ∈ g.cycleType
⊢ ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = i

Tactic:
rw [cycleType_def g, Multiset.mem_map] at hi

Premises used: Multiset.mem_map, Equiv.Perm.cycleType_def
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
i : ℕ
hi : ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = i
obtain : ∀ (c : Perm α) (hc : c ∈ g.cycleFactorsFinset.val), Odd ((card ∘ support) c)
⊢ Odd i

Tactic:
obtain ⟨c, hc, rfl⟩ := hi

Premises used: rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset.val
⊢ c ∈ g.cycleFactorsFinset

Tactic:
rw [← Finset.mem_def] at hc

Premises used: Finset.mem_def
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
rw : ∀ (this : HPow.hPow (α := ℤˣ) (-1) #c.support ≠ 1), Odd ((card ∘ support) c)
rw₁ : c.IsCycle
⊢ Odd ((card ∘ support) c)

Tactic:
rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this

Premises used: neg_eq_iff_eq_neg, Equiv.Perm.IsCycle.sign, Int.units_ne_iff_eq_neg
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : HPow.hPow (α := ℤˣ) (-1) #c.support ≠ 1
rw : ¬Even #c.support
⊢ Odd ((card ∘ support) c)

Tactic:
rw [← Nat.not_even_iff_odd, comp_apply]

Premises used: Nat.not_even_iff_odd, Function.comp_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : HPow.hPow (α := ℤˣ) (-1) #c.support ≠ 1
⊢ ¬Even #c.support

Tactic:
fun h ↦ this h.neg_one_pow

Premises used: Even.neg_one_pow, Not
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : HPow.hPow (α := ℤˣ) (-1) #c.support ≠ 1
⊢ ¬Even #c.support

Tactic:
exact fun h ↦ this h.neg_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
⊢ c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
rw [mem_cycleFactorsFinset_iff] at hc

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
hc₁ : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)

Tactic:
rw [mem_cycleFactorsFinset_iff] at hc

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
⊢ c.IsCycle

Tactic:
hc.left

Premises used: And.left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
⊢ c.IsCycle

Tactic:
exact hc.left

Premises used: And.left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
suffices : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
⊢ Odd ((card ∘ support) c)

Tactic:
suffices sign c = 1 by
    rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this
    · rw [← Nat.not_even_iff_odd, comp_apply]
      exact fun h ↦ this h.neg_one_pow
    · rw [mem_cycleFactorsFinset_iff] at hc
      exact hc.left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) c
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)

Tactic:
apply h
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a : c * g = g * c
⊢ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) c

Tactic:
rw [Subgroup.mem_centralizer_singleton_iff]

Premises used: Subgroup.mem_centralizer_singleton_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ c * g = g * c

Tactic:
Equiv.Perm.self_mem_cycle_factors_commute hc

Premises used: SemiconjBy, Equiv.Perm.self_mem_cycle_factors_commute, Commute
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ c * g = g * c

Tactic:
exact Equiv.Perm.self_mem_cycle_factors_commute hc

Premises used: Equiv.Perm.self_mem_cycle_factors_commute
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
pos :
  ∀ (hm : Even (m.sum + m.card)),
    Eq.{u_1 + 1} (α := Finset (Perm α))
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
      {g : Perm α | g.cycleType = m}
neg :
  ∀ (hm : ¬Even (m.sum + m.card)),
    Eq.{u_1 + 1} (α := Finset (Perm α))
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
      ∅
⊢ Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅)

Tactic:
split_ifs with hm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
pos :
  ∀ (g : Perm α),
    Membership.mem (γ := Finset (Perm α))
        (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
          {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
        g ↔
      Membership.mem (γ := Finset (Perm α)) {g : Perm α | g.cycleType = m} g
⊢ Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    {g : Perm α | g.cycleType = m}

Tactic:
ext g
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
pos : g.cycleType = m → Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ Membership.mem (γ := Finset (Perm α))
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
      g ↔
    Membership.mem (γ := Finset (Perm α)) {g : Perm α | g.cycleType = m} g

Tactic:
simp_rw [Finset.mem_map, Finset.mem_filter_univ, Embedding.coe_subtype, Subtype.exists,
      mem_alternatingGroup, exists_and_left, exists_prop, exists_eq_right_right,
      and_iff_left_iff_imp]

Premises used: exists_eq_right_right, Finset.mem_filter_univ, Function.Embedding.coe_subtype, Subtype.exists, exists_and_left, Equiv.Perm.mem_alternatingGroup, exists_prop, Finset.mem_map, and_iff_left_iff_imp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
pos : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
pos₁ : HPow.hPow (α := ℤˣ) (-1) (m.sum + m.card) = 1
pos₂ pos₃ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)

Tactic:
rw [sign_of_cycleType, hg, Even.neg_one_pow hm]

Premises used: Equiv.Perm.sign_of_cycleType, Even.neg_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
neg :
  ∀ (x : Perm α),
    x ∉
      map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m}
⊢ Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    ∅

Tactic:
rw [Finset.eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg :
  Membership.mem (γ := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    g
⊢ g.cycleType = m ∧ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)

Tactic:
simp_rw [Finset.mem_map, Finset.mem_filter_univ, Embedding.coe_subtype, Subtype.exists,
      mem_alternatingGroup, exists_and_left, exists_prop, exists_eq_right_right] at hg

Premises used: exists_eq_right_right, Finset.mem_filter_univ, Function.Embedding.coe_subtype, Subtype.exists, exists_and_left, Equiv.Perm.mem_alternatingGroup, exists_prop, Finset.mem_map
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m ∧ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ g.cycleType = m

Tactic:
rcases hg with ⟨hg, hs⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m ∧ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
hg₁ : g.cycleType = m
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)

Tactic:
rcases hg with ⟨hg, hs⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : HPow.hPow (α := ℤˣ) (-1) (m.sum + m.card) = 1
⊢ Ne (α := ℤˣ) (-1) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ Even (m.sum + m.card)

Tactic:
rw [g.sign_of_cycleType, hg, neg_one_pow_eq_one_iff_even (by simp)] at hs

Premises used: Equiv.Perm.sign_of_cycleType, neg_one_pow_eq_one_iff_even
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Even (m.sum + m.card)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
rw :
  (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0

Tactic:
rw [← Finset.card_map, map_subtype_of_cycleType, apply_ite Finset.card,
    Finset.card_empty, ite_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, Finset.card_map, apply_ite, Finset.card_empty, ite_mul, Finset.card, AlternatingGroup.map_subtype_of_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
simp :
  (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) ∧ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
⊢ (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0

Tactic:
simp only [and_comm (b := Even _)]

Premises used: and_comm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
rw :
  (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0
rw₁ rw₂ :
  (if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0) =
    if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0
⊢ (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) ∧ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0

Tactic:
rw [ite_and, Equiv.Perm.card_of_cycleType_mul_eq]

Premises used: Equiv.Perm.card_of_cycleType_mul_eq, ite_and