awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
f : Perm α
hf : f.IsThreeCycle
⊢ Eq (α := Subgroup ↥(alternatingGroup α))
    (normalClosure {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) f ⋯}) ⊤
have this : IsSimpleGroup.{u_1} ↥(alternatingGroup α)
Tactic: have : IsSimpleGroup (alternatingGroup α) := isSimpleGroup h5
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
f : Perm α
hf : f.IsThreeCycle
this : IsSimpleGroup.{u_1} ↥(alternatingGroup α)
⊢ Eq (α := Subgroup ↥(alternatingGroup α))
    (normalClosure {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) f ⋯}) ⊤
have apply : ¬Eq (α := Subgroup ↥(alternatingGroup α))
    (normalClosure {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) f sorry}) ⊥
Tactic: apply normalClosure_normal.eq_bot_or_eq_top.resolve_left
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
Goal:
⊢ Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      (singleton (α := ↥(alternatingGroup (Fin 5)))
        (Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
            Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x) (finRotate 5) ⋯ :
          ↥(alternatingGroup (Fin 5)))))
    ⊤
have this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
Tactic: have : IsSimpleGroup (alternatingGroup (Fin 5)) := isSimpleGroup (by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
⊢ Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      (singleton (α := ↥(alternatingGroup (Fin 5)))
        (Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
            Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x) (finRotate 5) ⋯ :
          ↥(alternatingGroup (Fin 5)))))
    ⊤
have apply : ¬Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      (singleton (α := ↥(alternatingGroup (Fin 5)))
        (Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
            Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x) (finRotate 5) sorry :
          ↥(alternatingGroup (Fin 5)))))
    ⊥
Tactic: apply normalClosure_normal.eq_bot_or_eq_top.resolve_left
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
Goal:
⊢ Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      {Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
          Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x)
          (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) ⋯})
    ⊤
have this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
Tactic: have : IsSimpleGroup (alternatingGroup (Fin 5)) := isSimpleGroup (by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
⊢ Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      {Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
          Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x)
          (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) ⋯})
    ⊤
have apply : ¬Eq (α := Subgroup ↥(alternatingGroup (Fin 5)))
    (normalClosure
      {Subtype.mk (p := fun (x : Perm (Fin 5)) ↦
          Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) x)
          (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) sorry})
    ⊥
Tactic: apply normalClosure_normal.eq_bot_or_eq_top.resolve_left
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ l.prod ∈ alternatingGroup α ↔ Even l.length
have rw : Ne (α := ℤˣ) (-1) 1
Tactic: rw [mem_alternatingGroup, sign_prod_list_swap hl, neg_one_pow_eq_one_iff_even]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
⊢ (alternatingGroup α).index = 2
have rw : Nat.card ↥⊤ = 2
Tactic: rw [alternatingGroup, index_ker, MonoidHom.range_eq_top.mpr (sign_surjective α)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
⊢ Nat.card ↥⊤ = 2
have simp_rw : Nat.card { x : ℤˣ // True } = 2
Tactic: simp_rw [mem_top, Nat.card_eq_fintype_card, card_subtype_true, card_units_int]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
simp_rw : Nat.card { x : ℤˣ // True } = 2
⊢ Nat.card ↥⊤ = 2
have simp_rw₁ : card { x : ℤˣ // True } = 2
Tactic: simp_rw [mem_top, Nat.card_eq_fintype_card, card_subtype_true, card_units_int]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nontrivial α
simp_rw : Nat.card { x : ℤˣ // True } = 2
simp_rw₁ : card { x : ℤˣ // True } = 2
⊢ Nat.card ↥⊤ = 2
have simp_rw₂ : card ℤˣ = 2
Tactic: simp_rw [mem_top, Nat.card_eq_fintype_card, card_subtype_true, card_units_int]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Subsingleton α
⊢ (alternatingGroup α).index = 1
have rw : alternatingGroup α = ⊤
Tactic: rw [Subgroup.index_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
⊢ IsCyclic.{u_1} ↥(alternatingGroup α)
have inl : Subsingleton α → IsCyclic.{u_1} ↥(alternatingGroup α)
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
inl : Subsingleton α → IsCyclic.{u_1} ↥(alternatingGroup α)
⊢ IsCyclic.{u_1} ↥(alternatingGroup α)
have inr : Nontrivial α → IsCyclic.{u_1} ↥(alternatingGroup α)
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
⊢ IsCyclic.{u_1} ↥(alternatingGroup α)
have this : 1 < Nat.card α
Tactic: have : 1 < Nat.card α := Finite.one_lt_card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
this : 1 < Nat.card α
⊢ IsCyclic.{u_1} ↥(alternatingGroup α)
have inr : Nat.card.{u_1} ↥(alternatingGroup α) ∣ 3
Tactic: apply isCyclic_of_card_dvd_prime (p := 3)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
this : 1 < Nat.card α
⊢ Nat.card.{u_1} ↥(alternatingGroup α) ∣ 3
have inr : (Nat.card α).factorial / 2 ∣ 3
Tactic: rw [nat_card_alternatingGroup]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
this : 1 < Nat.card α
⊢ (Nat.card α).factorial / 2 ∣ 3
have inr : ∀ (hα : LE.le (α := ℕ) 2 3) (this : LT.lt (α := ℕ) 1 2), Nat.factorial 2 / 2 ∣ 3
Tactic: interval_cases (Nat.card α)
Cleared hypotheses: hα, this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : Nat.card α ≤ 3
h : Nontrivial α
this : 1 < Nat.card α
inr : ∀ (hα : LE.le (α := ℕ) 2 3) (this : LT.lt (α := ℕ) 1 2), Nat.factorial 2 / 2 ∣ 3
⊢ (Nat.card α).factorial / 2 ∣ 3
have inr₁ : ∀ (hα : LE.le (α := ℕ) 3 3) (this : LT.lt (α := ℕ) 1 3), Nat.factorial 3 / 2 ∣ 3
Tactic: interval_cases (Nat.card α)
Cleared hypotheses: hα, this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : ↥(alternatingGroup α)
hc : IsConj (↑σ : Perm α) (↑τ : Perm α)
hσ : (↑σ : Perm α).support.card + 2 ≤ card α
⊢ IsConj σ τ
have obtain : ∀ (σ : Perm α) (hσ : σ ∈ alternatingGroup α)
  (hc : IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ) : Perm α) (↑τ : Perm α))
  (hσ_1 : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ) : Perm α).support.card + 2 ≤ card α),
  IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ) τ
Tactic: obtain ⟨σ, hσ⟩ := σ
Cleared hypotheses: σ, hc, hσ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : ↥(alternatingGroup α)
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hc : IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α) (↑τ : Perm α)
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) τ
have obtain : ∀ (τ : Perm α) (hτ : τ ∈ alternatingGroup α)
  (hc :
    IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)),
  IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
Tactic: obtain ⟨τ, hτ⟩ := τ
Cleared hypotheses: τ, hc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have obtain : ∀ (π : Perm α)
  (hπ :
    π * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α) * π⁻¹ =
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)),
  IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
Tactic: obtain ⟨π, hπ⟩ := isConj_iff.1 hc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ :
  π * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α) * π⁻¹ =
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have hπ₁ : π * σ * π⁻¹ = τ
Tactic: rw [Subtype.coe_mk, Subtype.coe_mk] at hπ
Cleared hypotheses: hπ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have inl : ∀ (h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)),
  IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
Tactic: rcases Int.units_eq_one_or (Perm.sign π) with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
inl :
  ∀ (h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)),
    IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have inr : ∀ (h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)),
  IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
Tactic: rcases Int.units_eq_one_or (Perm.sign π) with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have inl : ∃ (c : ↥(alternatingGroup α)),
  c * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 * c⁻¹ =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ
Tactic: rw [isConj_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (1 : ℤˣ)
⊢ ∃ (c : ↥(alternatingGroup α)),
    c * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 * c⁻¹ =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ
have inl : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) π sorry *
          Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 *
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) π sorry)⁻¹) :
    Perm α) =
  (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
Tactic: refine ⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
⊢ 2 ≤ σ.supportᶜ.card
have rw : σ.support.card + 2 ≤ card α
Tactic: rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have h2 : 2 ≤ σ.supportᶜ.card
Tactic: have h2 : 2 ≤ σ.supportᶜ.card := by
      rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
      exact hσ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have inr : ∀ (a : α) (ha : a ∈ σ.supportᶜ) (b : α) (hb : b ∈ σ.supportᶜ) (ab : a ≠ b),
  IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
Tactic: obtain ⟨a, ha, b, hb, ab⟩ := Finset.one_lt_card.1 h2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have inr : π * swap a b ∈ alternatingGroup α
Tactic: refine isConj_iff.2 ⟨⟨π * swap a b, ?_⟩, Subtype.val_injective ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
inr : π * swap a b ∈ alternatingGroup α
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
have inr₁ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) sorry *
          Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 *
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) sorry)⁻¹) :
    Perm α) =
  (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
Tactic: refine isConj_iff.2 ⟨⟨π * swap a b, ?_⟩, Subtype.val_injective ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ π * swap a b ∈ alternatingGroup α
have inr : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (π * swap a b) : ℤˣ) (1 : ℤˣ)
Tactic: rw [mem_alternatingGroup, map_mul, h, sign_swap ab, Int.units_mul_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
inr : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (π * swap a b) : ℤˣ) (1 : ℤˣ)
⊢ π * swap a b ∈ alternatingGroup α
have inr₁ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) =
  1
Tactic: rw [mem_alternatingGroup, map_mul, h, sign_swap ab, Int.units_mul_self]