awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)
⊢ Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
have rw₁ : Nat.card.{u_1} ↥(kleinFour α) ≠ 0
Tactic: rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)) *
      Nat.card.{u_1} ↥(kleinFour α) =
    3 * Nat.card.{u_1} ↥(kleinFour α)
have rw : Nat.card.{u_1} ↥(alternatingGroup α) = 3 * Nat.card.{u_1} ↥(kleinFour α)
Tactic: rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Nat.card.{u_1} ↥(alternatingGroup α) = 3 * Nat.card.{u_1} ↥(kleinFour α)
have rw : 12 = 3 * Nat.card.{u_1} ↥(kleinFour α)
Tactic: rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)
⊢ Nat.card.{u_1} ↥(alternatingGroup α) = 3 * Nat.card.{u_1} ↥(kleinFour α)
have rw₁ : 12 = HMul.hMul (α := ℕ) 3 4
Tactic: rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Nat.card.{u_1} ↥(kleinFour α) ≠ 0
have rw : Ne (α := ℕ) 4 0
Tactic: rw [kleinFour_card_of_card_eq_four hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
have this : 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)
have rw : IsMulCommutative.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α))
Tactic: rw [← Subgroup.Normal.quotient_commutative_iff_commutator_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
have comm_le : 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)) ⊥
have rw : ¬Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) ⊥ ⊤
Tactic: rw [ne_eq, commutator_eq_bot_iff_center_eq_top,
      center_eq_bot (le_of_eq hα4.symm)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)
⊢ ¬Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) ⊥ ⊤
have apply : Nontrivial.{u_1} (Subgroup ↥(alternatingGroup α))
Tactic: apply @bot_ne_top _ _ _ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)
⊢ Nontrivial.{u_1} (Subgroup ↥(alternatingGroup α))
have rw : LT.lt (α := ℕ) 1 12
Tactic: rw [Subgroup.nontrivial_iff, ← Finite.one_lt_card_iff_nontrivial,
      card_of_card_eq_four hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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 α)
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
have comm_ne_bot : 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)) ⊥
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
have obtain : ∀ (k : ↥(alternatingGroup α))
  (hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k) (hk' : k ≠ 1),
  Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
Tactic: obtain ⟨k, hk, hk'⟩ := Or.resolve_left (Subgroup.bot_or_exists_ne_one _) comm_ne_bot
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α))
have refine : LE.le (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
Tactic: refine le_antisymm ?_ comm_le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have hg₁ : 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
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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}
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have inl : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) 1
Tactic: rcases hg with ⟨rfl⟩ | hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have inr : ∀ (hg : (↑g : Perm α).cycleType = {2, 2}),
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
Tactic: rcases hg with ⟨rfl⟩ | hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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}
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have hk22₁ : ∃ (c : Perm α), c * (↑k : Perm α) * c⁻¹ = (↑g : Perm α)
Tactic: rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
Cleared hypotheses: hk22, hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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}
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have inr : ∀ (c : Perm α) (hc : c * (↑k : Perm α) * c⁻¹ = (↑g : Perm α)),
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
Tactic: obtain ⟨c, hc⟩ := hk22
Cleared hypotheses: hk22
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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 α)
hg : (↑g : Perm α).cycleType = {2, 2}
c : Perm α
hc : c * (↑k : Perm α) * c⁻¹ = (↑g : Perm α)
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have hc₁ : (((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
      (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
    k =
  g
Tactic: rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)
hg : (↑g : Perm α).cycleType = {2, 2}
c : Perm α
hc :
  (((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
        (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
      k =
    g
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have inr : Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
  (Bracket.bracket (L := Subgroup ↥(alternatingGroup α)) ⊤ ⊤)
  ((((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
        (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
      k :
    ↥(alternatingGroup α))
Tactic: simp only [commutator, ← hc]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this_1 :
  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 α)
hg : (↑g : Perm α).cycleType = {2, 2}
c : Perm α
hc :
  (((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
        (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
      k =
    g
fc : MulAut ↥(alternatingGroup α) := (MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c
this : ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
⊢ Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
    (Bracket.bracket (L := Subgroup ↥(alternatingGroup α)) ⊤ ⊤)
    ((((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
          (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
        k :
      ↥(alternatingGroup α))
have rw : Membership.mem (α := ↥(alternatingGroup α))
  (Subgroup.map (MulEquiv.toMonoidHom fc) (Bracket.bracket (L := Subgroup ↥(alternatingGroup α)) ⊤ ⊤))
  ((((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
        (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
      k :
    ↥(alternatingGroup α))
Tactic: rw [this, ← Subgroup.map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α)
hg : (↑g : Perm α).cycleType = {2, 2}
c : Perm α
hc :
  (((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
        (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
      k =
    g
fc : MulAut ↥(alternatingGroup α) := (MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c
⊢ Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
    (Bracket.bracket (L := Subgroup ↥(alternatingGroup α)) ⊤ ⊤)
    ((((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
          (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
        k :
      ↥(alternatingGroup α))
have inr : ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
Tactic: suffices (⊤ : Subgroup (alternatingGroup α)) =
        Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
        rw [this, ← Subgroup.map_commutator]
        refine Subgroup.mem_map_of_mem _ hk
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
have suffices : (↑k : Perm α).cycleType = {2, 2}
Tactic: suffices hk22 : (k : Equiv.Perm α).cycleType = {2, 2} by
    refine le_antisymm ?_ comm_le
    intro g hg
    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
    rcases hg with ⟨rfl⟩ | hg
    · exact Subgroup.one_mem _
    · rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
      obtain ⟨c, hc⟩ := hk22
      rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
      simp only [commutator, ← hc]
      let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c
      suffices (⊤ : Subgroup (alternatingGroup α)) =
        Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
        rw [this, ← Subgroup.map_commutator]
        refine Subgroup.mem_map_of_mem _ hk
      simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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
⊢ (↑k : Perm α).cycleType = {2, 2}
have hk2 : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α) k
Tactic: have hk2 := comm_le hk