awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
⊢ LE.le (α := ℕ) 3 5

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
⊢ 3 ≤ Nat.card α

Tactic:
simpa using le_trans (by norm_num) hα

Premises used: le_trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
f : Perm α
hf : f.IsThreeCycle
⊢ IsSimpleGroup.{u_1} ↥(alternatingGroup α)

Tactic:
have : IsSimpleGroup (alternatingGroup α) := isSimpleGroup h5
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
f : Perm α
hf : f.IsThreeCycle
this : IsSimpleGroup.{u_1} ↥(alternatingGroup α)
apply :
  ¬Eq (α := Subgroup ↥(alternatingGroup α))
      (normalClosure {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) f ⋯}) ⊥
⊢ Eq (α := Subgroup ↥(alternatingGroup α))
    (normalClosure {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) f ⋯}) ⊤

Tactic:
apply normalClosure_normal.eq_bot_or_eq_top.resolve_left

Premises used: Or.resolve_left, Subgroup.normalClosure_normal, Subgroup.Normal.eq_bot_or_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
f : Perm α
hf : f.IsThreeCycle
this : IsSimpleGroup.{u_1} ↥(alternatingGroup α)
⊢ ¬Eq (α := Subgroup ↥(alternatingGroup α))
      (normalClosure {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) f ⋯}) ⊥

Tactic:
simp [hf.ne_one]

Premises used: Equiv.Perm.IsThreeCycle.ne_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
⊢ 5 ≤ Nat.card (Fin 5)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
⊢ IsSimpleGroup ↥(alternatingGroup (Fin 5))

Tactic:
have : IsSimpleGroup (alternatingGroup (Fin 5)) := isSimpleGroup (by simp)
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
apply :
  ¬Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
      (normalClosure
        (singleton (α := ↥(alternatingGroup (Fin 5)))
          (Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
              Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x) (finRotate 5) ⋯ :
            ↥(alternatingGroup (Fin 5)))))
      ⊥
⊢ Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      (singleton (α := ↥(alternatingGroup (Fin 5)))
        (Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
            Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x) (finRotate 5) ⋯ :
          ↥(alternatingGroup (Fin 5)))))
    ⊤

Tactic:
apply normalClosure_normal.eq_bot_or_eq_top.resolve_left

Premises used: Or.resolve_left, Subgroup.normalClosure_normal, Subgroup.Normal.eq_bot_or_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
⊢ ¬Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
      (normalClosure
        (singleton (α := ↥(alternatingGroup (Fin 5)))
          (Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
              Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x) (finRotate 5) ⋯ :
            ↥(alternatingGroup (Fin 5)))))
      ⊥

Tactic:
simp +decide

Premises used: Decidable.decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq (α := ℤˣ) ((sign : (a : Perm (Fin 5)) → ℤˣ) (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) : ℤˣ) (1 : ℤˣ)

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
apply :
  ¬Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
      (normalClosure
        {Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
            Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x)
            (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) ⋯})
      ⊥
⊢ Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      {Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
          Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x)
          (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) ⋯})
    ⊤

Tactic:
apply normalClosure_normal.eq_bot_or_eq_top.resolve_left

Premises used: Or.resolve_left, Subgroup.normalClosure_normal, Subgroup.Normal.eq_bot_or_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
⊢ ¬Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
      (normalClosure
        {Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
            Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x)
            (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) ⋯})
      ⊥

Tactic:
simp +decide

Premises used: Decidable.decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ 5 ≤ Nat.card (Fin 5)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
⊢ Ne (α := ℤˣ) (-1) 1

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ alternatingGroup α = MonoidHom.ker sign

Tactic:
rfl

Premises used: alternatingGroup, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
⊢ f ∈ alternatingGroup α ↔ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)

Tactic:
sign.mem_ker

Premises used: Set.Mem, MonoidHom.mem_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g g' : Perm α
hg : g.IsSwap
hg' : g'.IsSwap
⊢ g * g' ∈ alternatingGroup α

Tactic:
simp [mem_alternatingGroup, map_mul, hg.sign_eq, hg'.sign_eq]

Premises used: Equiv.Perm.mem_alternatingGroup, map_mul, Equiv.Perm.IsSwap.sign_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
rw : Ne (α := ℤˣ) (-1) 1
⊢ l.prod ∈ alternatingGroup α ↔ Even l.length

Tactic:
rw [mem_alternatingGroup, sign_prod_list_swap hl, neg_one_pow_eq_one_iff_even]

Premises used: neg_one_pow_eq_one_iff_even, Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_prod_list_swap
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ Ne (α := ℤˣ) (-1) 1

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
h : f.IsThreeCycle
⊢ f ∈ alternatingGroup α

Tactic:
Perm.mem_alternatingGroup.mpr h.sign

Premises used: Iff.mpr, Equiv.Perm.mem_alternatingGroup, Equiv.Perm.IsThreeCycle.sign
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
n : ℕ
⊢ Membership.mem (γ := Subgroup (Perm (Fin (2 * n + 1)))) (alternatingGroup (Fin (2 * n + 1))) (finRotate (2 * n + 1))

Tactic:
simp [mem_alternatingGroup]

Premises used: Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
rw : Nat.card ↥⊤ = 2
⊢ (alternatingGroup α).index = 2

Tactic:
rw [alternatingGroup, index_ker, MonoidHom.range_eq_top.mpr (sign_surjective α)]

Premises used: Iff.mpr, Subgroup.index_ker, MonoidHom.range_eq_top, alternatingGroup, Equiv.Perm.sign_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
simp_rw : Nat.card { x : ℤˣ // True } = 2
simp_rw₁ : card { x : ℤˣ // True } = 2
simp_rw₂ : card ℤˣ = 2
⊢ Nat.card ↥⊤ = 2

Tactic:
simp_rw [mem_top, Nat.card_eq_fintype_card, card_subtype_true, card_units_int]

Premises used: Fintype.card_subtype_true, Fintype.card_units_int, Subgroup.mem_top, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Subsingleton α
rw : alternatingGroup α = ⊤
⊢ (alternatingGroup α).index = 1

Tactic:
rw [Subgroup.index_eq_one]

Premises used: Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Subsingleton α
⊢ alternatingGroup α = ⊤

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
e : α ≃ β
⊢ map (↑e.permCongrHom : Perm α →* Perm β) (alternatingGroup α) = alternatingGroup β

Tactic:
simp [Subgroup.ext_iff, Subgroup.map_equiv_eq_comap_symm]

Premises used: Subgroup.ext_iff, Subgroup.map_equiv_eq_comap_symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
⊢ 2 * Nat.card.{u_1} ↥(alternatingGroup α) = Nat.card.{u_1} (Perm α)

Tactic:
simp only [← alternatingGroup.index_eq_two (α := α), index_mul_card]

Premises used: Subgroup.index_mul_card, alternatingGroup.index_eq_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
⊢ 2 * card.{u_1} ↥(alternatingGroup α) = card.{u_1} (Perm α)

Tactic:
simp only [← Nat.card_eq_fintype_card, two_mul_nat_card_alternatingGroup]

Premises used: two_mul_nat_card_alternatingGroup, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
⊢ card.{u_1} ↥(alternatingGroup α) = (card α).factorial / 2

Tactic:
Nat.eq_div_of_mul_eq_right two_ne_zero (two_mul_card_alternatingGroup.trans card_perm)

Premises used: Nat.eq_div_of_mul_eq_right, Fintype.card_perm, two_ne_zero, two_mul_card_alternatingGroup, Eq.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
⊢ Nat.card.{u_1} ↥(alternatingGroup α) = (Nat.card α).factorial / 2

Tactic:
simp only [Nat.card_eq_fintype_card, card_alternatingGroup]

Premises used: card_alternatingGroup, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
inl : Subsingleton α → IsCyclic.{u_1} ↥(alternatingGroup α)
inr : Nontrivial α → IsCyclic.{u_1} ↥(alternatingGroup α)
⊢ IsCyclic.{u_1} ↥(alternatingGroup α)

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Subsingleton α
⊢ IsCyclic.{u_1} ↥(alternatingGroup α)

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

Tactic:
have : 1 < Nat.card α := Finite.one_lt_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
this : 1 < Nat.card α
inr : Nat.card.{u_1} ↥(alternatingGroup α) ∣ 3
⊢ IsCyclic.{u_1} ↥(alternatingGroup α)

Tactic:
apply isCyclic_of_card_dvd_prime (p := 3)

Premises used: isCyclic_of_card_dvd_prime
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
this : 1 < Nat.card α
inr : (Nat.card α).factorial / 2 ∣ 3
⊢ Nat.card.{u_1} ↥(alternatingGroup α) ∣ 3

Tactic:
rw [nat_card_alternatingGroup]

Premises used: nat_card_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
this : 1 < Nat.card α
inr : ∀ (hα : LE.le (α := ℕ) 2 3) (this : LT.lt (α := ℕ) 1 2), Nat.factorial 2 / 2 ∣ 3
inr₁ : ∀ (hα : LE.le (α := ℕ) 3 3) (this : LT.lt (α := ℕ) 1 3), Nat.factorial 3 / 2 ∣ 3
⊢ (Nat.card α).factorial / 2 ∣ 3

Tactic:
interval_cases (Nat.card α)

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : Nontrivial α
hα : LE.le (α := ℕ) 2 3
this : LT.lt (α := ℕ) 1 2
⊢ Nat.factorial 2 / 2 ∣ 3

Tactic:
simp [Nat.factorial_succ]

Premises used: Nat.factorial_succ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : Nontrivial α
hα : LE.le (α := ℕ) 3 3
this : LT.lt (α := ℕ) 1 3
⊢ Nat.factorial 3 / 2 ∣ 3

Tactic:
simp [Nat.factorial_succ]

Premises used: Nat.factorial_succ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
⊢ IsMulCommutative.{u_1} ↥(alternatingGroup α)

Tactic:
(isCyclic_of_card_le_three hα).isMulCommutative

Premises used: Set.Mem, IsCyclic.isMulCommutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ (alternatingGroup α).Normal

Tactic:
sign.normal_ker

Premises used: Equiv.Perm.sign, MonoidHom.normal_ker, alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : ↥(alternatingGroup α)
hc : IsConj (↑σ : Perm α) (↑τ : Perm α)
hσ : (↑σ : Perm α).support.card + 2 ≤ card α
obtain :
  ∀ (σ : Perm α) (hσ : σ ∈ alternatingGroup α)
    (hc : IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ) : Perm α) (↑τ : Perm α))
    (hσ_1 : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ) : Perm α).support.card + 2 ≤ card α),
    IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ) τ
⊢ IsConj σ τ

Tactic:
obtain ⟨σ, hσ⟩ := σ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : ↥(alternatingGroup α)
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hc : IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α) (↑τ : Perm α)
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
obtain :
  ∀ (τ : Perm α) (hτ : τ ∈ alternatingGroup α)
    (hc :
      IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
        (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)),
    IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) τ

Tactic:
obtain ⟨τ, hτ⟩ := τ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
obtain :
  ∀ (π : Perm α)
    (hπ :
      π * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α) * π⁻¹ =
        (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)),
    IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)

Tactic:
obtain ⟨π, hπ⟩ := isConj_iff.1 hc

Premises used: isConj_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ :
  π * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α) * π⁻¹ =
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
⊢ π * σ * π⁻¹ = τ

Tactic:
rw [Subtype.coe_mk, Subtype.coe_mk] at hπ

Premises used: Subtype.coe_mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
inl :
  ∀ (h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)),
    IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
inr :
  ∀ (h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)),
    IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)

Tactic:
rcases Int.units_eq_one_or (Perm.sign π) with h | h

Premises used: Equiv.Perm.sign, Int.units_eq_one_or, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)
inl :
  ∃ (c : ↥(alternatingGroup α)),
    c * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 * c⁻¹ =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)

Tactic:
rw [isConj_iff]

Premises used: isConj_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)
⊢ ∃ (c : ↥(alternatingGroup α)),
    c * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 * c⁻¹ =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ

Tactic:
⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective ?_⟩

Premises used: Subtype.val_injective, Equiv.Perm.mem_alternatingGroup, Subtype.mk, Exists.intro, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)
inl :
  (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) π ⋯ *
            Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 *
          (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) π ⋯)⁻¹) :
      Perm α) =
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
⊢ ∃ (c : ↥(alternatingGroup α)),
    c * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 * c⁻¹ =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ

Tactic:
refine ⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)
⊢ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) π ⋯ *
            Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 *
          (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) π ⋯)⁻¹) :
      Perm α) =
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)

Tactic:
simpa only [Subtype.val, Subgroup.coe_mul, coe_inv, coe_mk] using hπ

Premises used: Subgroup.coe_mk, Equiv.Perm.coe_inv, Subgroup.coe_mul, Subtype.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
rw : σ.support.card + 2 ≤ card α
⊢ 2 ≤ σ.supportᶜ.card

Tactic:
rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]

Premises used: Equiv.Perm.support, Finset.card_compl, le_tsub_iff_left, Finset.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
⊢ σ.support.card + 2 ≤ card α

Tactic:
hσ