awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {1} (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
h : g = 1
⊢ HPow.hPow (β := ℕ) g 2 = 1

Tactic:
convert! one_pow _

Premises used: one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {1} (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
⊢ g = 1

Tactic:
simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'

Premises used: Set.mem_singleton_iff, Subgroup.mk_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
⊢ g ^ orderOf g = 1

Tactic:
pow_orderOf_eq_one g

Premises used: pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
h : 2 = orderOf g
⊢ HPow.hPow (β := ℕ) g 2 = 1

Tactic:
convert! pow_orderOf_eq_one g

Premises used: pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
h : Eq (α := ℕ) 2 (Multiset.lcm {2, 2})
⊢ 2 = orderOf g

Tactic:
rw [← Equiv.Perm.lcm_cycleType, hg']

Premises used: Equiv.Perm.lcm_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
⊢ Eq (α := ℕ) 2 (Multiset.lcm {2, 2})

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) ∣ 2

Tactic:
have : Monoid.exponent (kleinFour α) ∣ 2 := by
    rw [Monoid.exponent_dvd]
    rintro ⟨⟨g, hg⟩, hg'⟩
    simp only [Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one]
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4] at hg'
    rcases hg' with hg' | hg'
    · convert! one_pow _
      simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'
    · convert! pow_orderOf_eq_one g
      rw [← Equiv.Perm.lcm_cycleType, hg']
      simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent.{u_1} ↥(kleinFour α) ∣ 2
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) = 1 ∨ Monoid.exponent.{u_1} ↥(kleinFour α) = 2

Tactic:
rw [Nat.dvd_prime Nat.prime_two] at this

Premises used: Nat.dvd_prime, Nat.prime_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent.{u_1} ↥(kleinFour α) = 1 ∨ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
apply : ¬Monoid.exponent.{u_1} ↥(kleinFour α) = 1
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) = 2

Tactic:
apply Or.resolve_left this

Premises used: Or.resolve_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent.{u_1} ↥(kleinFour α) = 1 ∨ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
rw : ¬LE.le (α := ℕ) 4 1
⊢ ¬Monoid.exponent.{u_1} ↥(kleinFour α) = 1

Tactic:
rw [Monoid.exp_eq_one_iff, ← Finite.card_le_one_iff_subsingleton,
    kleinFour_card_of_card_eq_four hα4]

Premises used: alternatingGroup.kleinFour_card_of_card_eq_four, Finite.card_le_one_iff_subsingleton, Monoid.exp_eq_one_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent.{u_1} ↥(kleinFour α) = 1 ∨ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
⊢ ¬LE.le (α := ℕ) 4 1

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)

Tactic:
have _ : (kleinFour α).Normal := normal_kleinFour hα4
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
rw :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) *
      Nat.card.{u_1} ↥(kleinFour α) =
    3 * Nat.card.{u_1} ↥(kleinFour α)
rw₁ : Nat.card.{u_1} ↥(kleinFour α) ≠ 0
⊢ Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3

Tactic:
rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]

Premises used: Nat.mul_left_inj
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
rw : Nat.card.{u_1} ↥(alternatingGroup α) = 3 * Nat.card.{u_1} ↥(kleinFour α)
⊢ Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) *
      Nat.card.{u_1} ↥(kleinFour α) =
    3 * Nat.card.{u_1} ↥(kleinFour α)

Tactic:
rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
rw : 12 = 3 * Nat.card.{u_1} ↥(kleinFour α)
rw₁ rw₂ : 12 = HMul.hMul (α := ℕ) 3 4
⊢ Nat.card.{u_1} ↥(alternatingGroup α) = 3 * Nat.card.{u_1} ↥(kleinFour α)

Tactic:
rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]

Premises used: alternatingGroup.kleinFour_card_of_card_eq_four, alternatingGroup.card_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
rw : Ne (α := ℕ) 4 0
⊢ Nat.card.{u_1} ↥(kleinFour α) ≠ 0

Tactic:
rw [kleinFour_card_of_card_eq_four hα4]

Premises used: alternatingGroup.kleinFour_card_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Ne (α := ℕ) 4 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3

Tactic:
have : Nat.card (alternatingGroup α ⧸ kleinFour α) = 3 := by
    rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]
    · rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]
      rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]
    rw [kleinFour_card_of_card_eq_four hα4]; simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
rw :
  IsMulCommutative.{u_1}
    (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α))
⊢ LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)

Tactic:
rw [← Subgroup.Normal.quotient_commutative_iff_commutator_le]

Premises used: Subgroup.Normal.quotient_commutative_iff_commutator_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
⊢ IsMulCommutative.{u_1}
    (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α))

Tactic:
(isCyclic_of_prime_card this).isMulCommutative

Premises used: IsCyclic.isMulCommutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
⊢ IsMulCommutative.{u_1}
    (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α))

Tactic:
exact (isCyclic_of_prime_card this).isMulCommutative

Premises used: IsCyclic.isMulCommutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
⊢ LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)

Tactic:
have comm_le : commutator (alternatingGroup α) ≤ kleinFour α := by
    rw [← Subgroup.Normal.quotient_commutative_iff_commutator_le]
    exact (isCyclic_of_prime_card this).isMulCommutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
rw : ¬Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) ⊥ ⊤
⊢ Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥

Tactic:
rw [ne_eq, commutator_eq_bot_iff_center_eq_top,
      center_eq_bot (le_of_eq hα4.symm)]

Premises used: alternatingGroup.center_eq_bot, ne_eq, le_of_eq, Eq.symm, commutator_eq_bot_iff_center_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
apply : Nontrivial.{u_1} (Subgroup ↥(alternatingGroup α))
⊢ ¬Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) ⊥ ⊤

Tactic:
apply @bot_ne_top _ _ _ ?_

Premises used: bot_ne_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
rw : LT.lt (α := ℕ) 1 12
⊢ Nontrivial.{u_1} (Subgroup ↥(alternatingGroup α))

Tactic:
rw [Subgroup.nontrivial_iff, ← Finite.one_lt_card_iff_nontrivial,
      card_of_card_eq_four hα4]

Premises used: Subgroup.nontrivial_iff, alternatingGroup.card_of_card_eq_four, Finite.one_lt_card_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
⊢ LT.lt (α := ℕ) 1 12

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
⊢ Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥

Tactic:
have comm_ne_bot : commutator (alternatingGroup α) ≠ ⊥ := by
    rw [ne_eq, commutator_eq_bot_iff_center_eq_top,
      center_eq_bot (le_of_eq hα4.symm)]
    apply @bot_ne_top _ _ _ ?_
    rw [Subgroup.nontrivial_iff, ← Finite.one_lt_card_iff_nontrivial,
      card_of_card_eq_four hα4]
    simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
obtain :
  ∀ (k : ↥(alternatingGroup α))
    (hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k) (hk' : k ≠ 1),
    Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))

Tactic:
obtain ⟨k, hk, hk'⟩ := Or.resolve_left (Subgroup.bot_or_exists_ne_one _) comm_ne_bot

Premises used: Or.resolve_left, Subgroup.bot_or_exists_ne_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))

Tactic:
le_antisymm ?_ comm_le

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
refine : LE.le (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))

Tactic:
refine le_antisymm ?_ comm_le

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α) g
⊢ g = 1 ∨ (↑g : Perm α).cycleType = {2, 2}

Tactic:
rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4,
      Set.mem_union, Set.mem_singleton_iff, Set.mem_setOf_eq] at hg

Premises used: Set.mem_union, alternatingGroup.coe_kleinFour_of_card_eq_four, Set.mem_setOf_eq, Set.mem_singleton_iff, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : g = 1 ∨ (↑g : Perm α).cycleType = {2, 2}
inl : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) 1
inr :
  ∀ (hg : (↑g : Perm α).cycleType = {2, 2}),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g

Tactic:
rcases hg with ⟨rfl⟩ | hg

Premises used: rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) 1

Tactic:
Subgroup.one_mem _

Premises used: Set.Mem, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) 1

Tactic:
exact Subgroup.one_mem _

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
⊢ ∃ (c : Perm α), c * (↑k : Perm α) * c⁻¹ = (↑g : Perm α)

Tactic:
rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22

Premises used: isConj_iff, Equiv.Perm.isConj_iff_cycleType_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk22 : (↑k : Perm α).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
hk22₁ : ∃ (c : Perm α), c * (↑k : Perm α) * c⁻¹ = (↑g : Perm α)
⊢ (↑g : Perm α).cycleType = {2, 2}

Tactic:
rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22

Premises used: isConj_iff, Equiv.Perm.isConj_iff_cycleType_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hk22 : ∃ (c : Perm α), c * (↑k : Perm α) * c⁻¹ = (↑g : Perm α)
hg : (↑g : Perm α).cycleType = {2, 2}
inr :
  ∀ (c : Perm α) (hc : c * (↑k : Perm α) * c⁻¹ = (↑g : Perm α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g

Tactic:
obtain ⟨c, hc⟩ := hk22