awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
rw : (c * c).IsThreeCycle
⊢ (c * (g' * g' * c)).IsThreeCycle

Tactic:
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]

Premises used: pow_two, Iff.mp, orderOf_dvd_iff_pow_eq_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * c).IsThreeCycle

Tactic:
(card_support_eq_three_iff.1 h3).isThreeCycle_sq

Premises used: card_support_eq_three_iff, Equiv.Perm.IsThreeCycle.isThreeCycle_sq, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * c).IsThreeCycle

Tactic:
exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq

Premises used: card_support_eq_three_iff, Equiv.Perm.IsThreeCycle.isThreeCycle_sq, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
suffices : orderOf g' ∣ 2
⊢ (c * (g' * g' * c)).IsThreeCycle

Tactic:
suffices hg' : orderOf g' ∣ 2 by
    rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
    exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
rw : ∀ b ∈ g'.cycleType, b ∣ 2
⊢ orderOf g' ∣ 2

Tactic:
rw [← lcm_cycleType, Multiset.lcm_dvd]

Premises used: Equiv.Perm.lcm_cycleType, Multiset.lcm_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
rw : g'.support.card ≤ 2
⊢ n ∣ 2

Tactic:
rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]

Premises used: Equiv.Perm.le_card_support_of_mem_cycleType, le_antisymm, Equiv.Perm.two_le_of_mem_cycleType, le_trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
bc : c.support.card + g'.support.card ≤ c.support.card + 2
a : ℕ
⊢ g'.support.card ≤ 2

Tactic:
apply le_of_add_le_add_left

Premises used: le_of_add_le_add_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ (c * g').support.card ≤ HAdd.hAdd (α := ℕ) 3 2

Tactic:
(c * g').support.card_le_univ

Premises used: Equiv.Perm.support, HMul.hMul, Fintype.card, Finset.card_le_univ, Finset.card, Multiset.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ (c * g').support.card ≤ HAdd.hAdd (α := ℕ) 3 2

Tactic:
exact (c * g').support.card_le_univ

Premises used: Equiv.Perm.support, HMul.hMul, Finset.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
rw : Nat.card.{u_1} ↥(alternatingGroup α) = 1
rw₁ : 2 * Nat.card.{u_1} ↥(alternatingGroup α) = HMul.hMul (α := ℕ) 2 1
rw₂ : Nat.card.{u_1} (Perm α) = HMul.hMul (α := ℕ) 2 1
rw₃ : Nat.card.{u_1} (Perm α) = 2
rw₄ : (Nat.card α).factorial = 2
rw₅ : Nat.factorial 2 = 2
rw₆ rw₇ : Eq (α := ℕ) 2 2
⊢ alternatingGroup α = ⊥

Tactic:
rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]

Premises used: Nat.card_perm, Subgroup.eq_bot_iff_card, Nat.factorial_two, two_mul_nat_card_alternatingGroup, mul_one, Nat.mul_right_inj
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
suffices : Nat.card α = 2
⊢ alternatingGroup α = ⊥

Tactic:
suffices hα' : Nat.card α = 2 by
    rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
⊢ Nat.card α = 2

Tactic:
h2.antisymm ?_

Premises used: LE.le.antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
refine : 2 ≤ Nat.card α
⊢ Nat.card α = 2

Tactic:
refine h2.antisymm ?_

Premises used: LE.le.antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
⊢ 2 ≤ Nat.card α

Tactic:
simpa [Nat.card_eq_fintype_card] using Fintype.one_lt_card

Premises used: Fintype.one_lt_card, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
rw : 1 < Nat.card α
⊢ Nontrivial α

Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, ← Nat.card_eq_fintype_card]

Premises used: Fintype.one_lt_card_iff_nontrivial, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
⊢ LT.lt (α := ℕ) 1 3

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
⊢ 1 < Nat.card α

Tactic:
refine lt_of_lt_of_le (by decide) h3

Premises used: lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
⊢ Nontrivial α

Tactic:
have : Nontrivial α := by
    rw [← Fintype.one_lt_card_iff_nontrivial, ← Nat.card_eq_fintype_card]
    refine lt_of_lt_of_le (by decide) h3
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
rw : 1 < Nat.card.{u_1} ↥(alternatingGroup α)
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)

Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, ← Nat.card_eq_fintype_card]

Premises used: Fintype.one_lt_card_iff_nontrivial, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ 1 < Nat.card.{u_1} ↥(alternatingGroup α)

Tactic:
lt_of_mul_lt_mul_left ?_ (le_of_lt Nat.prime_two.pos)

Premises used: lt_of_mul_lt_mul_left, le_of_lt, Nat.Prime.pos, Nat.prime_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
refine : HMul.hMul (α := ℕ) 2 1 < 2 * Nat.card.{u_1} ↥(alternatingGroup α)
⊢ 1 < Nat.card.{u_1} ↥(alternatingGroup α)

Tactic:
refine lt_of_mul_lt_mul_left ?_ (le_of_lt Nat.prime_two.pos)

Premises used: lt_of_mul_lt_mul_left, le_of_lt, Nat.Prime.pos, Nat.prime_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
rw : (HMul.hMul (α := ℕ) 2 1).succ ≤ (Nat.card α).factorial
⊢ HMul.hMul (α := ℕ) 2 1 < 2 * Nat.card.{u_1} ↥(alternatingGroup α)

Tactic:
rw [two_mul_nat_card_alternatingGroup, Nat.card_perm, ← Nat.succ_le_iff]

Premises used: Nat.card_perm, two_mul_nat_card_alternatingGroup, Nat.succ_le_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ (HMul.hMul (α := ℕ) 2 1).succ ≤ (Nat.card α).factorial

Tactic:
le_trans h3 (Nat.card α).self_le_factorial

Premises used: Nat.card, Nat.self_le_factorial, le_trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ (HMul.hMul (α := ℕ) 2 1).succ ≤ (Nat.card α).factorial

Tactic:
exact le_trans h3 (Nat.card α).self_le_factorial

Premises used: Nat.card, Nat.self_le_factorial, le_trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
⊢ 3 ≤ Nat.card (Fin (n + 3))

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : ∀ n ∈ g.cycleType, n = 2
⊢ g.support.card ≤ card (Fin 5)

Tactic:
have h := g.support.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : ∀ n ∈ g.cycleType, n = 2
h : g.support.card ≤ card (Fin 5)
⊢ g.cycleType = Multiset.replicate g.cycleType.card 2

Tactic:
rw [← Multiset.eq_replicate_card] at h2

Premises used: Multiset.eq_replicate_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : ∀ n ∈ g.cycleType, n = 2
h : g.support.card ≤ card (Fin 5)
h2₁ : g.cycleType = Multiset.replicate g.cycleType.card 2
⊢ g.support.card ≤ card (Fin 5)

Tactic:
rw [← Multiset.eq_replicate_card] at h2

Premises used: Multiset.eq_replicate_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.support.card ≤ card (Fin 5)
⊢ g.cycleType.card * 2 ≤ card (Fin 5)

Tactic:
rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h

Premises used: Multiset.sum_replicate, smul_eq_mul, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ card (Fin 5) ≤ HMul.hMul (α := ℕ) 3 2

Tactic:
norm_num only [card_fin]

Premises used: Fintype.card_fin
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ LT.lt (α := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ g.cycleType.card ≤ 3

Tactic:
have h : Multiset.card g.cycleType ≤ 3 :=
    le_of_mul_le_mul_right (le_trans h (by norm_num only [card_fin])) (by simp)
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
    1

Tactic:
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha₁ :
  HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
    1
⊢ g ≠ 1

Tactic:
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha₁ :
  HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
    1
h1₁ : g ≠ 1
⊢ g.cycleType = Multiset.replicate g.cycleType.card 2

Tactic:
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha₁ :
  HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
    1
h1₁ : g ≠ 1
h2₁ : g.cycleType = Multiset.replicate g.cycleType.card 2
⊢ g.cycleType.card * 2 ≤ card (Fin 5)

Tactic:
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha₁ :
  HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
    1
h1₁ : g ≠ 1
h2₁ : g.cycleType = Multiset.replicate g.cycleType.card 2
h₁ : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ g.cycleType.card ≤ 3

Tactic:
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
ha :
  HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
    1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ HPow.hPow (α := ℤˣ) (-1) (g.cycleType.card * 2 + g.cycleType.card) = 1

Tactic:
simp at ha
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.card * 2 + g.cycleType.card) = 1
rw : ∀ (ha : Even g.cycleType.card), IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
rw₁ : ∀ (ha : HPow.hPow (α := ℤˣ) (-1) g.cycleType.card = 1), Ne (α := ℤˣ) (-1) 1
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g

Tactic:
rw [pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] at ha

Premises used: Int.units_pow_two, pow_add, neg_one_pow_eq_one_iff_even, pow_mul, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : HPow.hPow (α := ℤˣ) (-1) g.cycleType.card = 1
⊢ Ne (α := ℤˣ) (-1) 1

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : Even g.cycleType.card
rw : (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate g.cycleType.card 2
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g

Tactic:
rw [isConj_iff_cycleType_eq, h2]

Premises used: Equiv.Perm.isConj_iff_cycleType_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : Even g.cycleType.card
0 :
  ∀ (h_1 : g.cycleType.card = 0) (h2 : g.cycleType = Multiset.replicate 0 2) (h : HMul.hMul (α := ℕ) 0 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 0 3) (ha : Even (α := ℕ) 0),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 0 2
1 :
  ∀ (h_1 : g.cycleType.card = 1) (h2 : g.cycleType = Multiset.replicate 1 2) (h : HMul.hMul (α := ℕ) 1 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 1 3) (ha : Even (α := ℕ) 1),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 1 2
2 :
  ∀ (h_1 : g.cycleType.card = 2) (h2 : g.cycleType = Multiset.replicate 2 2) (h : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 2 3) (ha : Even (α := ℕ) 2),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2
3 :
  ∀ (h_1 : g.cycleType.card = 3) (h2 : g.cycleType = Multiset.replicate 3 2) (h : HMul.hMul (α := ℕ) 3 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 3 3) (ha : Even (α := ℕ) 3),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 3 2
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate g.cycleType.card 2

Tactic:
interval_cases h_1 : Multiset.card g.cycleType

Premises used: Equiv.Perm.cycleType, Multiset.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 0
h2 : g.cycleType = Multiset.replicate 0 2
h_2 : HMul.hMul (α := ℕ) 0 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 0 3
ha : Even (α := ℕ) 0
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 0 2

Tactic:
(h1 (card_cycleType_eq_zero.1 h_1)).elim

Premises used: False.elim, Equiv.Perm.card_cycleType_eq_zero, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 0
h2 : g.cycleType = Multiset.replicate 0 2
h_2 : HMul.hMul (α := ℕ) 0 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 0 3
ha : Even (α := ℕ) 0
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 0 2

Tactic:
exact (h1 (card_cycleType_eq_zero.1 h_1)).elim

Premises used: False.elim, Equiv.Perm.card_cycleType_eq_zero, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 1
h2 : g.cycleType = Multiset.replicate 1 2
h_2 : HMul.hMul (α := ℕ) 1 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 1 3
ha : Even (α := ℕ) 1
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 1 2

Tactic:
simp at ha
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
⊢ Ne (α := Fin 5) 0 4

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
⊢ Ne (α := Fin 5) 0 4

Tactic:
have h04 : (0 : Fin 5) ≠ 4 := by decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
⊢ Ne (α := Fin 5) 1 3

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
⊢ Ne (α := Fin 5) 1 3

Tactic:
have h13 : (1 : Fin 5) ≠ 3 := by decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
h13 : Ne (α := Fin 5) 1 3
2 : HAdd.hAdd (α := Multiset ℕ) {2} {2} = Multiset.replicate 2 2
h_3 : Perm.Disjoint (α := Fin 5) (swap 0 4) (swap 1 3)
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2

Tactic:
rw [Disjoint.cycleType_mul, (isCycle_swap h04).cycleType, (isCycle_swap h13).cycleType,
      card_support_swap h04, card_support_swap h13]

Premises used: Equiv.Perm.IsCycle.cycleType, Equiv.Perm.card_support_swap, Equiv.Perm.isCycle_swap, Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
h13 : Ne (α := Fin 5) 1 3
⊢ HAdd.hAdd (α := Multiset ℕ) {2} {2} = Multiset.replicate 2 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
h13 : Ne (α := Fin 5) 1 3
2 : _root_.Disjoint (α := Finset (Fin 5)) {0, 4} {1, 3}
⊢ Perm.Disjoint (α := Fin 5) (swap 0 4) (swap 1 3)

Tactic:
rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13]

Premises used: Equiv.Perm.support_swap, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
h13 : Ne (α := Fin 5) 1 3
⊢ _root_.Disjoint (α := Finset (Fin 5)) {0, 4} {1, 3}

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 3
h2 : g.cycleType = Multiset.replicate 3 2
h_2 : HMul.hMul (α := ℕ) 3 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 3 3
ha : Even (α := ℕ) 3
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 3 2

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
rw : LE.le.{u_1} (α := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α)) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α)) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff