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
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 α)
⊢ (((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
        (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
      k =
    g

Tactic:
rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc

Premises used: Subtype.coe_inj, MulAut.conjNormal_apply
-- 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 α)
hg : (↑g : Perm α).cycleType = {2, 2}
c : Perm α
hc :
  (((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
        (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
      k =
    g
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 α))
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g

Tactic:
simp only [commutator, ← hc]

Premises used: commutator
-- 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_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) ⊤
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 α))
⊢ 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:
rw [this, ← Subgroup.map_commutator]

Premises used: Subgroup.map_commutator
-- 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_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.map (MulEquiv.toMonoidHom fc) (Bracket.bracket (L := Subgroup ↥(alternatingGroup α)) ⊤ ⊤))
    ((((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
          (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
        k :
      ↥(alternatingGroup α))

Tactic:
Subgroup.mem_map_of_mem _ hk

Premises used: Set.Mem, Subgroup.mem_map_of_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_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.map (MulEquiv.toMonoidHom fc) (Bracket.bracket (L := Subgroup ↥(alternatingGroup α)) ⊤ ⊤))
    ((((MulAut.conjNormal : (a : Perm α) → MulAut ↥(alternatingGroup α)) c : MulAut ↥(alternatingGroup α)) :
          (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
        k :
      ↥(alternatingGroup α))

Tactic:
refine Subgroup.mem_map_of_mem _ hk

Premises used: Subgroup.mem_map_of_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
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
inr : ⊤ = 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 α))

Tactic:
suffices (⊤ : Subgroup (alternatingGroup α)) =
        Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
        rw [this, ← Subgroup.map_commutator]
        refine Subgroup.mem_map_of_mem _ hk
-- 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 α)
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
⊢ ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤

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 α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
suffices : (↑k : Perm α).cycleType = {2, 2}
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))

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
-- 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
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α) k

Tactic:
have hk2 := comm_le hk
-- 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
hk2 : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α) k
⊢ k = 1 ∨ (↑k : 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 hk2

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
hk2 : k = 1 ∨ (↑k : Perm α).cycleType = {2, 2}
⊢ (↑k : Perm α).cycleType = {2, 2}

Tactic:
hk2.resolve_left hk'

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
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
hk2 : k = 1 ∨ (↑k : Perm α).cycleType = {2, 2}
⊢ (↑k : Perm α).cycleType = {2, 2}

Tactic:
exact hk2.resolve_left hk'

Premises used: Or.resolve_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : 2 < s.ncard
⊢ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
rw [two_lt_ncard_iff] at hs

Premises used: Set.two_lt_ncard_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
obtain :
  ∀ (a b c : α) (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c),
    ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle

Tactic:
obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := hs
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle

Tactic:
⟨swap a b * swap a c, ?_, isThreeCycle_swap_mul_swap_same hab hac hbc⟩

Premises used: HMul.hMul, Equiv.swap, And.intro, Exists.intro, Equiv.Perm.isThreeCycle_swap_mul_swap_same
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
refine : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b * swap a c)
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle

Tactic:
refine ⟨swap a b * swap a c, ?_, isThreeCycle_swap_mul_swap_same hab hac hbc⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
rw : (swap a b * swap a c)⁻¹ • s ⊆ s
⊢ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b * swap a c)

Tactic:
rw [mem_stabilizer_set_iff_subset_smul_set s.toFinite, subset_smul_set_iff]

Premises used: Set.subset_smul_set_iff, MulAction.mem_stabilizer_set_iff_subset_smul_set, Set.toFinite
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∈ s
⊢ (fun (x : α) ↦ (swap a b * swap a c)⁻¹ • x) x ∈ s

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
inl :
  ∀ (hs : 2 < s.ncard),
    ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
inr :
  ∀ (hs : 2 ≥ s.ncard),
    ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle

Tactic:
rcases Nat.lt_or_ge 2 (ncard s) with hs | hs

Premises used: Nat.lt_or_ge, Set.ncard, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 < s.ncard
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle

Tactic:
exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard hs

Premises used: Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 < s.ncard
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle

Tactic:
exact exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard hs

Premises used: Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
⊢ s.ncard + sᶜ.ncard = Nat.card α

Tactic:
have := ncard_add_ncard_compl s
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
inr : ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ) g ∧ g.IsThreeCycle
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle

Tactic:
rw [← stabilizer_compl]

Premises used: stabilizer_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ 2 < sᶜ.ncard

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ) g ∧ g.IsThreeCycle

Tactic:
exact exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard (by grind)

Premises used: Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup (Perm α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G
obtain :
  ∀ (g : Perm α) (hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g) (hg3 : g.IsThreeCycle),
    alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
obtain ⟨g, hg, hg3⟩ := exists_mem_stabilizer_isThreeCycle s h4

Premises used: Equiv.Perm.exists_mem_stabilizer_isThreeCycle
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup (Perm α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
apply : g ∈ G
⊢ alternatingGroup α ≤ G

Tactic:
apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem hG' hg3

Premises used: Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup (Perm α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
⊢ g ∈ G

Tactic:
hG ⟨hg, IsThreeCycle.mem_alternatingGroup hg3⟩

Premises used: And.intro, Equiv.Perm.IsThreeCycle.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup (Perm α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
⊢ g ∈ G

Tactic:
exact hG ⟨hg, IsThreeCycle.mem_alternatingGroup hg3⟩

Premises used: And.intro, Equiv.Perm.IsThreeCycle.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
obtain :
  ∀ (a : α) (ha : a ∈ sᶜ) (b : α) (hb : b ∈ sᶜ) (hab : a ≠ b),
    ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
⊢ ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)

Tactic:
obtain ⟨a, ha, b, hb, hab⟩ := hs
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
h : (swap a b).IsSwap ∧ _root_.Disjoint s (↑(swap a b).support : Set α)
⊢ ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)

Tactic:
use Equiv.swap a b

Premises used: Equiv.swap