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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
simp : ∀ (x : α), x ∉ g.support
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg = 1

Tactic:
simp only [← Subtype.coe_inj, Subgroup.coe_one, ← support_eq_empty_iff,
    Finset.eq_empty_iff_forall_notMem]

Premises used: Equiv.Perm.support_eq_empty_iff, Subtype.coe_inj, Finset.eq_empty_iff_forall_notMem, Subgroup.coe_one
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha rw : a ∈ g.support
⊢ (g : (a : α) → α) a ≠ a

Tactic:
rw [← mem_support]

Premises used: Equiv.Perm.mem_support
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
⊢ a ∈ g.support

Tactic:
ha
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
⊢ a ∈ g.support

Tactic:
exact ha
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
⊢ (g : (a : α) → α) a ≠ a

Tactic:
have hab : g a ≠ a := by rw [← mem_support]; exact ha
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
rw : Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α))) + 2 ≤ card α
⊢ 2 ≤ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ

Tactic:
rw [← Nat.add_le_add_iff_left, Finset.card_add_card_compl]

Premises used: Finset.card_add_card_compl, Nat.add_le_add_iff_left
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
rw : Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α))) + 2 ≤ Nat.card α
⊢ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α))) + 2 ≤ card α

Tactic:
rw [← Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
rw : HAdd.hAdd (α := ℕ) 2 2 ≤ Nat.card α
⊢ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α))) + 2 ≤ Nat.card α

Tactic:
rw [Finset.card_pair hab.symm]

Premises used: Ne.symm, Finset.card_pair
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
⊢ HAdd.hAdd (α := ℕ) 2 2 ≤ Nat.card α

Tactic:
hα4
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
⊢ HAdd.hAdd (α := ℕ) 2 2 ≤ Nat.card α

Tactic:
exact hα4
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
⊢ 2 ≤ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ

Tactic:
have : 2 ≤ (({a, g a} : Finset α)ᶜ).card := by
    rw [← Nat.add_le_add_iff_left, Finset.card_add_card_compl]
    rw [← Nat.card_eq_fintype_card]
    rw [Finset.card_pair hab.symm]
    exact hα4
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
this : 2 ≤ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ
⊢ ∃ (a_1 : α) (b : α),
    Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ a_1 ∧
      Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ b ∧ a_1 ≠ b

Tactic:
rw [← Nat.lt_iff_add_one_le, Finset.one_lt_card_iff] at this

Premises used: Finset.one_lt_card_iff, Nat.lt_iff_add_one_le
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
this :
  ∃ (a_1 : α) (b : α),
    Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ a_1 ∧
      Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ b ∧ a_1 ≠ b
obtain :
  ∀ (c d : α) (hc : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ c)
    (hd : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ d) (hcd : c ≠ d),
    False
⊢ False

Tactic:
obtain ⟨c, d, hc, hd, hcd⟩ := this
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hc : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ c
hd : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ d
hcd : c ≠ d
⊢ c ≠ a ∧ c ≠ (g : (a : α) → α) a

Tactic:
simp only [Finset.compl_insert, Finset.mem_erase, ← ne_eq, Finset.mem_compl,
    Finset.mem_singleton] at hc hd

Premises used: Finset.mem_singleton, Finset.compl_insert, Finset.mem_compl, ne_eq, Finset.mem_erase
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hc : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ c
hd : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ d
hcd : c ≠ d
hc₁ : c ≠ a ∧ c ≠ (g : (a : α) → α) a
⊢ d ≠ a ∧ d ≠ (g : (a : α) → α) a

Tactic:
simp only [Finset.compl_insert, Finset.mem_erase, ← ne_eq, Finset.mem_compl,
    Finset.mem_singleton] at hc hd

Premises used: Finset.mem_singleton, Finset.compl_insert, Finset.mem_compl, ne_eq, Finset.mem_erase
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 α)
simp :
  ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α)
      (((swap ((g : (a : α) → α) a) c : Perm α) : (a : α) → α) a : α) =
    a
⊢ k • a = a

Tactic:
simp only [Perm.smul_def, coe_mul, Function.comp_apply, k]

Premises used: Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 α)
rw : ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) a = a
⊢ ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α)
      (((swap ((g : (a : α) → α) a) c : Perm α) : (a : α) → α) a : α) =
    a

Tactic:
rw [swap_apply_of_ne_of_ne (x := a) hab.symm hc.1.symm]

Premises used: Ne.symm, Equiv.swap_apply_of_ne_of_ne, And.left
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 α)
rw rw₁ : a = a
⊢ ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) a = a

Tactic:
rw [swap_apply_of_ne_of_ne hab.symm hd.1.symm]

Premises used: Ne.symm, Equiv.swap_apply_of_ne_of_ne, And.left
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 α)
⊢ k • a = a

Tactic:
have hka : k • a = a := by
    simp only [Perm.smul_def, coe_mul, Function.comp_apply, k]
    rw [swap_apply_of_ne_of_ne (x := a) hab.symm hc.1.symm]
    rw [swap_apply_of_ne_of_ne hab.symm hd.1.symm]
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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
simp : ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) c = c
⊢ HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c

Tactic:
simp only [Perm.smul_def, coe_mul, Function.comp_apply, swap_apply_left, k]

Premises used: Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply, Equiv.swap_apply_left
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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
rw rw₁ : c = c
⊢ ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) c = c

Tactic:
rw [swap_apply_of_ne_of_ne hc.2 hcd]

Premises used: Equiv.swap_apply_of_ne_of_ne, And.right
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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
⊢ HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c

Tactic:
have hkga : k • (g a) = c := by
    simp only [Perm.smul_def, coe_mul, Function.comp_apply, swap_apply_left, k]
    rw [swap_apply_of_ne_of_ne hc.2 hcd]
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
apply : k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a = c
⊢ False

Tactic:
apply this
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
⊢ k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a = c

Tactic:
simp [← hkga]
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
⊢ False

Tactic:
suffices k • (⟨g, hg⟩ : alternatingGroup α) • a ≠ c by
    apply this; simp [← hkga]
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
rw : Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
⊢ k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c

Tactic:
rw [this, hka]
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c

Tactic:
hc.right.symm

Premises used: Ne.symm, And.right
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c

Tactic:
exact hc.right.symm

Premises used: Ne.symm, And.right
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
⊢ k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c

Tactic:
suffices k • (⟨g, hg⟩ : alternatingGroup α) • a = (⟨g, hg⟩ : alternatingGroup α) • k • a by
    rw [this, hka]; exact hc.right.symm
-- 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' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
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
rw :
  ∀
    (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),
    let k :=
      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 • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
        Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
⊢ 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:
rw [Subgroup.mem_center_iff] at hg'

Premises used: Subgroup.mem_center_iff