awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  ∀ (g_1 : ↥(alternatingGroup α)),
    g_1 * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg * g_1
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
this : k ∈ alternatingGroup α
⊢ k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a

Tactic:
simp only [← Subgroup.mk_smul k this, ← mul_smul, hg']

Premises used: SemigroupAction.mul_smul, Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  ∀ (g_1 : ↥(alternatingGroup α)),
    g_1 * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg * g_1
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
suffices : k ∈ alternatingGroup α
⊢ k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a

Tactic:
suffices k ∈ alternatingGroup α by
    simp only [← Subgroup.mk_smul k this, ← mul_smul, hg']
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  ∀ (g_1 : ↥(alternatingGroup α)),
    g_1 * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg * g_1
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
⊢ k ∈ alternatingGroup α

Tactic:
simp [k, hc.2.symm, hd.2.symm]

Premises used: Ne.symm, And.right
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ IsMulCommutative.{u_1} ↥(alternatingGroup α) ↔ Nat.card α ≤ 3

Tactic:
⟨fun H ↦ ?_, fun h ↦ (isCyclic_of_card_le_three h).isMulCommutative⟩

Premises used: IsCyclic.isMulCommutative, Iff.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
refine : ∀ (H : IsMulCommutative.{u_1} ↥(alternatingGroup α)), Nat.card α ≤ 3
⊢ IsMulCommutative.{u_1} ↥(alternatingGroup α) ↔ Nat.card α ≤ 3

Tactic:
refine ⟨fun H ↦ ?_, fun h ↦ (isCyclic_of_card_le_three h).isMulCommutative⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
rw : ¬3 < Nat.card α
⊢ Nat.card α ≤ 3

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
this : Subsingleton.{u_1 + 1} ↥(alternatingGroup α)
⊢ ¬Nontrivial.{u_1} ↥(alternatingGroup α)

Tactic:
rw [← not_nontrivial_iff_subsingleton] at this

Premises used: not_nontrivial_iff_subsingleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
this : ¬Nontrivial.{u_1} ↥(alternatingGroup α)
apply : Nontrivial.{u_1} ↥(alternatingGroup α)
⊢ False

Tactic:
apply this
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
this : ¬Nontrivial.{u_1} ↥(alternatingGroup α)
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)

Tactic:
nontrivial_of_three_le_card h.le

Premises used: LT.lt.le, alternatingGroup.nontrivial_of_three_le_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
this : ¬Nontrivial.{u_1} ↥(alternatingGroup α)
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)

Tactic:
exact nontrivial_of_three_le_card h.le

Premises used: LT.lt.le, alternatingGroup.nontrivial_of_three_le_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
suffices : Subsingleton.{u_1 + 1} ↥(alternatingGroup α)
⊢ False

Tactic:
suffices Subsingleton (alternatingGroup α) by
    rw [← not_nontrivial_iff_subsingleton] at this
    apply this
    exact nontrivial_of_three_le_card h.le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
⊢ Subsingleton.{u_1 + 1} ↥(alternatingGroup α)

Tactic:
simpa [center_eq_top_iff.mpr H, eq_comm, subsingleton_iff_bot_eq_top] using center_eq_bot h

Premises used: Iff.mpr, alternatingGroup.center_eq_bot, eq_comm, Subgroup.center_eq_top_iff, subsingleton_iff_bot_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : IsCyclic.{u_1} ↥(alternatingGroup α)
rw : IsMulCommutative.{u_1} ↥(alternatingGroup α)
⊢ Nat.card α ≤ 3

Tactic:
rw [← isMulCommutative_iff_card_le_three]

Premises used: alternatingGroup.isMulCommutative_iff_card_le_three
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : IsCyclic.{u_1} ↥(alternatingGroup α)
⊢ IsMulCommutative.{u_1} ↥(alternatingGroup α)

Tactic:
IsCyclic.isMulCommutative

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

Tactic:
exact IsCyclic.isMulCommutative

Premises used: IsCyclic.isMulCommutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
x : ↥(alternatingGroup ↥s)
rw :
  Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s)) :
      ℤˣ)
    (1 : ℤˣ)
rw₁ : Eq (α := ℤˣ) (((sign : Perm ↥s →* ℤˣ) : (a : Perm ↥s) → ℤˣ) (↑x : Perm ↥s) : ℤˣ) (1 : ℤˣ)
rw₂ rw₃ : Eq (α := ℤˣ) 1 1
⊢ Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s) : Perm α)

Tactic:
rw [mem_alternatingGroup, sign_ofSubtype, mem_alternatingGroup.mp x.prop]

Premises used: Equiv.Perm.mem_alternatingGroup, Subtype.prop, Iff.mp, Equiv.Perm.sign_ofSubtype
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ Eq (α := ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑1 : Perm ↥s)) ⋯ :
      ↥(alternatingGroup α))
    (1 : ↥(alternatingGroup α))

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ ∀ (x y : ↥(alternatingGroup ↥s)),
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑(x * y) : Perm ↥s)) ⋯ =
      HMul.hMul (α := ↥(alternatingGroup α)) (β := ↥(alternatingGroup α))
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
            ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s)) ⋯ :
          ↥(alternatingGroup α))
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
            ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑y : Perm ↥s)) ⋯ :
          ↥(alternatingGroup α))

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  Function.Injective (α := ↥(alternatingGroup ↥s)) (β := Perm α)
    (Function.comp (β := ↥(alternatingGroup α)) (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
      (⇑(ofSubtype s) : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)))
⊢ Function.Injective (α := ↥(alternatingGroup ↥s)) (β := ↥(alternatingGroup α))
    (⇑(ofSubtype s) : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α))

Tactic:
rw [← Function.Injective.of_comp_iff (alternatingGroup α).subtype_injective]

Premises used: Subgroup.subtype_injective, alternatingGroup, Function.Injective.of_comp_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ Function.Injective (α := ↥(alternatingGroup ↥s)) (β := Perm α)
    (Function.comp (β := ↥(alternatingGroup α)) (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
      (⇑(ofSubtype s) : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)))

Tactic:
Perm.ofSubtype_injective.comp (alternatingGroup s).subtype_injective

Premises used: Equiv.Perm.extendDomain, Subgroup.subtype_injective, Membership.mem, Subtype, Function.Injective.comp, alternatingGroup, Equiv.Perm.ofSubtype_injective, Equiv.Perm.subtypeCongr
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ Function.Injective (α := ↥(alternatingGroup ↥s)) (β := Perm α)
    (Function.comp (β := ↥(alternatingGroup α)) (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
      (⇑(ofSubtype s) : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)))

Tactic:
exact Perm.ofSubtype_injective.comp (alternatingGroup s).subtype_injective

Premises used: Subgroup.subtype_injective, Membership.mem, Subtype, Function.Injective.comp, alternatingGroup, Equiv.Perm.ofSubtype_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
g h : ↥(alternatingGroup ↥s)
⊢ Eq (α := ↥(alternatingGroup α))
      ((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) g : ↥(alternatingGroup α))
      ((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) h : ↥(alternatingGroup α)) ↔
    g = h

Tactic:
ofSubtype_injective.eq_iff

Premises used: Function.Injective.eq_iff, alternatingGroup.ofSubtype_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
k : ↥(alternatingGroup ↥s)
⊢ Eq (α := Perm α) ((↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) k) : Perm α) : Perm α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑k : Perm ↥s) : Perm α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
h :
  ∀ (k : Perm α),
    Membership.mem (γ := Subgroup (Perm α))
        (map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s)) k ↔
      k ∈ MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
⊢ map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
    MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α

Tactic:
ext k
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
k : Perm α
⊢ (∃ (x : Perm ↥s),
      Membership.mem (γ := Subgroup (Perm ↥s)) (alternatingGroup ↥s) x ∧
        (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) x = k) ↔
    (∃ (x : Perm ↥s), (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) x = k) ∧
      k ∈ alternatingGroup α

Tactic:
grind [sign_ofSubtype, mem_alternatingGroup]

Premises used: Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_ofSubtype
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ (alternatingGroup α).subtype.comp (ofSubtype s) =
    MonoidHom.comp (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (Subgroup.subtype (alternatingGroup ↥s))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₁ :
  ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₂ :
  MonoidHom.range (G := ↥(alternatingGroup ↥s))
      (MonoidHom.comp (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₃ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))
      (MonoidHom.range (G := ↥(alternatingGroup ↥s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₄ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₅ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
    MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
rw₆ rw₇ :
  MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α =
    MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)

Tactic:
rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]

Premises used: Subgroup.map_subtype_inj, MonoidHom.range_comp, alternatingGroup.map_ofSubtype, Subgroup.subgroupOf_map_subtype, Subgroup.range_subtype, alternatingGroup.ofSubtype_comp_subtype
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
rw : (↑(↑k : Perm α).support : Set α) ⊆ {x : α | x ∈ s} ↔ (↑k : Perm α).support ⊆ s
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (MonoidHom.range (ofSubtype s)) k ↔ (↑k : Perm α).support ⊆ s

Tactic:
rw [range_ofSubtype, mem_subgroupOf, Perm.mem_range_ofSubtype_iff]

Premises used: Equiv.Perm.mem_range_ofSubtype_iff, alternatingGroup.range_ofSubtype, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ (↑(↑k : Perm α).support : Set α) ⊆ {x : α | x ∈ s} ↔ (↑k : Perm α).support ⊆ s

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
g : ↥(alternatingGroup α)
h :
  ∀ (k : ↥(alternatingGroup α)),
    k ∈
        HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
          ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α)) g : MulAut ↥(alternatingGroup α))
          (MonoidHom.range (ofSubtype s)) ↔
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (MonoidHom.range (ofSubtype (g • s))) k
⊢ HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
      ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α)) g : MulAut ↥(alternatingGroup α))
      (MonoidHom.range (ofSubtype s)) =
    MonoidHom.range (ofSubtype (g • s))

Tactic:
ext k
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
h :
  (HSMul.hSMul (α := ConjAct (Perm α))
          ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) (↑g⁻¹ : Perm α) : ConjAct (Perm α))
          (↑k : Perm α)).support ⊆
      s ↔
    (↑k : Perm α).support ⊆ g • s
⊢ k ∈
      HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
        ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α)) g : MulAut ↥(alternatingGroup α))
        (MonoidHom.range (ofSubtype s)) ↔
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (MonoidHom.range (ofSubtype (g • s))) k

Tactic:
simp_rw [mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff, ← map_inv,
    MulAut.smul_def, ← ConjAct.toConjAct_smul_eq_mulAut_conj, ConjAct.coe_smul]

Premises used: map_inv, MulAut.smul_def, ConjAct.toConjAct_smul_eq_mulAut_conj, alternatingGroup.mem_range_ofSubtype_iff, ConjAct.coe_smul, Subgroup.mem_pointwise_smul_iff_inv_smul_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ (HSMul.hSMul (α := ConjAct (Perm α))
          ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) (↑g⁻¹ : Perm α) : ConjAct (Perm α))
          (↑k : Perm α)).support ⊆
      s ↔
    (↑k : Perm α).support ⊆ g • s

Tactic:
simp [support_conj_eq_smul_support, Finset.subset_smul_finset_iff, Subgroup.smul_def]

Premises used: Finset.subset_smul_finset_iff, Equiv.Perm.support_conj_eq_smul_support, Subgroup.smul_def
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
by_contra! : ∀ (h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G), False
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∉ G

Tactic:
by_contra! h
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
this : G = ⊤
⊢ Eq (α := ℕ) 1 2

Tactic:
rw [this, Subgroup.index_top] at hG

Premises used: Subgroup.index_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
this : G = ⊤
hG₁ : Eq (α := ℕ) 1 2
⊢ Nontrivial α

Tactic:
rw [this, Subgroup.index_top] at hG

Premises used: Subgroup.index_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
this : G = ⊤
hG₁ : Eq (α := ℕ) 1 2
a : Nontrivial α
⊢ ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G

Tactic:
rw [this, Subgroup.index_top] at hG

Premises used: Subgroup.index_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
this : G = ⊤
hG₁ : Eq (α := ℕ) 1 2
a : Nontrivial α
h₁ : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
⊢ G = ⊤

Tactic:
rw [this, Subgroup.index_top] at hG

Premises used: Subgroup.index_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : Eq (α := ℕ) 1 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
this : G = ⊤
⊢ False

Tactic:
cases hG
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
suffices : G = ⊤
⊢ False

Tactic:
suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
rwa : ⊤ ≤ G
rwa₁ : closure {σ : Perm α | σ.IsSwap} ≤ G
rwa₂ rwa₃ rwa₄ rwa₅ : {σ : Perm α | σ.IsSwap} ⊆ (↑G : Set (Perm α))
⊢ G = ⊤

Tactic:
rwa [eq_top_iff, ← closure_isSwap, G.closure_le]

Premises used: Equiv.Perm.closure_isSwap, eq_top_iff, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
obtain : ∀ (a b : α) (hab : a ≠ b) (habG : swap a b ∉ G), G = alternatingGroup α
⊢ G = alternatingGroup α

Tactic:
obtain ⟨_, ⟨a, b, hab, rfl⟩, habG⟩ : ∃ g : Perm α, g.IsSwap ∧ g ∉ G := by
    by_contra! h
    suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG
    rwa [eq_top_iff, ← closure_isSwap, G.closure_le]

Premises used: Equiv.Perm, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
h : ∀ (g : Perm α), g ∈ G ↔ g ∈ alternatingGroup α
⊢ G = alternatingGroup α

Tactic:
ext g
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g : Perm α
⊢ g ∈ G ↔ g ∈ alternatingGroup α

Tactic:
swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_

Premises used: Equiv.Perm.swap_induction_on
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g : Perm α
h :
  ∀ (g : Perm α) (x y : α) (hxy : x ≠ y) (ih : g ∈ G ↔ g ∈ alternatingGroup α),
    swap x y * g ∈ G ↔ swap x y * g ∈ alternatingGroup α
⊢ g ∈ G ↔ g ∈ alternatingGroup α

Tactic:
refine swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_