awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
this : Eq (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
⊢ ∀ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) g

Tactic:
simp [this]
-- 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ᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
suffices : ∃ (g : ↥(alternatingGroup α)), g ∉ stabilizer (↥(alternatingGroup α)) s
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤

Tactic:
suffices ∃ g, g ∉ stabilizer (alternatingGroup α) s by contrapose! this; simp [this]
-- 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ᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ swap a b * swap a c ∈ alternatingGroup α

Tactic:
aesop
-- 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ᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
h :
  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap a c) ⋯ ∉
    stabilizer (↥(alternatingGroup α)) s
⊢ ∃ (g : ↥(alternatingGroup α)), g ∉ stabilizer (↥(alternatingGroup α)) s

Tactic:
use ⟨Equiv.swap a b * Equiv.swap a c, by aesop⟩
-- 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ᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
h : ¬∀ (b_1 : α), Membership.mem (α := α) s ((swap a b : (a : α) → α) ((swap a c : (a : α) → α) b_1 : α) : α) ↔ b_1 ∈ s
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap a c) ⋯ ∉
    stabilizer (↥(alternatingGroup α)) s

Tactic:
simp_rw [mem_stabilizer_set, Subgroup.mk_smul, mul_smul, Perm.smul_def]

Premises used: Equiv.Perm.smul_def, MulAction.mem_stabilizer_set, SemigroupAction.mul_smul, Subgroup.mk_smul
-- 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ᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ ¬∀ (b_1 : α), Membership.mem (α := α) s ((swap a b : (a : α) → α) ((swap a c : (a : α) → α) b_1 : α) : α) ↔ b_1 ∈ s

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
pos :
  ∀ (hab : a = b),
    ∃ (g : ↥(alternatingGroup α)),
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
neg :
  ∀ (hab : ¬a = b),
    ∃ (g : ↥(alternatingGroup α)),
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b

Tactic:
by_cases hab : a = b
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a = b
h :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) 1 ∧
    HSMul.hSMul (α := ↥(alternatingGroup α)) 1 a = b
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b

Tactic:
use 1
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a = b
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) 1 ∧
    HSMul.hSMul (α := ↥(alternatingGroup α)) 1 a = b

Tactic:
simpa
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
pos :
  ∀ (ht : 2 < t.ncard),
    ∃ (g : ↥(alternatingGroup α)),
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
neg :
  ∀ (ht : ¬2 < t.ncard),
    ∃ (g : ↥(alternatingGroup α)),
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b

Tactic:
by_cases ht : 2 < t.ncard

Premises used: Set.ncard
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : 2 < t.ncard
⊢ ncard (α := α) {a, b} < t.ncard

Tactic:
rw [← Set.ncard_pair hab] at ht

Premises used: Set.ncard_pair
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ncard (α := α) {a, b} < t.ncard
⊢ (t \ {a, b}).Nonempty

Tactic:
replace ht := Set.diff_nonempty_of_ncard_lt_ncard ht
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : (t \ {a, b}).Nonempty
pos :
  ∀ (c : α) (hct : c ∈ t) (hc : c ∉ {a, b}),
    ∃ (g : ↥(alternatingGroup α)),
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b

Tactic:
obtain ⟨c, hct, hc⟩ := ht
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : c ∉ {a, b}
⊢ ¬c = a ∧ c ∉ {b}

Tactic:
simp only [mem_insert_iff, not_or] at hc

Premises used: not_or, Set.mem_insert_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ swap c a * swap a b ∈ alternatingGroup α

Tactic:
simp [hab, hc.1]

Premises used: And.left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
pos :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) ⋯)
pos₁ :
  HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) ⋯) a =
    b
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b

Tactic:
refine ⟨⟨swap c a * swap a b, by simp [hab, hc.1]⟩, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
pos : ∀ ⦃b_1 : α⦄, b_1 ∈ t → Function.comp (β := α) (⇑(swap c a) : (a : α) → α) (⇑(swap a b) : (a : α) → α) b_1 ∈ t
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) ⋯)

Tactic:
simp only [mem_stabilizer_set' t.toFinite, Subgroup.mk_smul, Perm.smul_def, coe_mul]

Premises used: Equiv.Perm.smul_def, Equiv.Perm.coe_mul, MulAction.mem_stabilizer_set', Set.toFinite, Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ t → Function.comp (β := α) (⇑(swap c a) : (a : α) → α) (⇑(swap a b) : (a : α) → α) b_1 ∈ t

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
pos : Function.comp (β := α) (⇑(swap c a) : (a : α) → α) (⇑(swap a b) : (a : α) → α) a = b
⊢ HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) ⋯) a =
    b

Tactic:
simp only [Subgroup.mk_smul, Perm.smul_def, coe_mul]

Premises used: Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ Function.comp (β := α) (⇑(swap c a) : (a : α) → α) (⇑(swap a b) : (a : α) → α) a = b

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
⊢ t.ncard + tᶜ.ncard = Nat.card α

Tactic:
have := ncard_add_ncard_compl t
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
⊢ 1 < tᶜ.ncard

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
neg :
  ∀ (c d : α) (hc : c ∈ tᶜ) (hd : d ∈ tᶜ) (hcd : c ≠ d),
    ∃ (g : ↥(alternatingGroup α)),
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b

Tactic:
obtain ⟨c, d, hc, hd, hcd⟩ := (one_lt_ncard_iff tᶜ.toFinite).mp (by grind)

Premises used: Compl.compl, Set.toFinite, Iff.mp, Set.one_lt_ncard_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ swap a b * swap c d ∈ alternatingGroup α

Tactic:
simp [hab, hcd]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
neg :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) ⋯)
neg₁ :
  HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) ⋯) a =
    b
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b

Tactic:
refine ⟨⟨swap a b * swap c d, by simp [hab, hcd]⟩, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
neg : ∀ ⦃b_1 : α⦄, b_1 ∈ t → Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap c d) : (a : α) → α) b_1 ∈ t
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) ⋯)

Tactic:
simp only [mem_stabilizer_set' t.toFinite, Subgroup.mk_smul, Perm.smul_def, coe_mul]

Premises used: Equiv.Perm.smul_def, Equiv.Perm.coe_mul, MulAction.mem_stabilizer_set', Set.toFinite, Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ t → Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap c d) : (a : α) → α) b_1 ∈ t

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
neg : Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap c d) : (a : α) → α) a = b
⊢ HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) ⋯) a =
    b

Tactic:
simp only [Subgroup.smul_def, Perm.smul_def, Perm.coe_mul]

Premises used: Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Subgroup.smul_def
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap c d) : (a : α) → α) a = b

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
obtain :
  ∀ (g : Perm α) (hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g) (hg3 : g.IsThreeCycle), G = ⊤
⊢ 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 ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
rw : alternatingGroup α ≤ Subgroup.map (alternatingGroup α).subtype G
⊢ G = ⊤

Tactic:
rw [eq_top_iff, ← Subgroup.map_subtype_le_map_subtype,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]

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

Tactic:
apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem _ 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 ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
h :
  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g ⋯ ∈ (↑G : Set ↥(alternatingGroup α)) ∧
    ((alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g ⋯) =
      g
⊢ g ∈ Subgroup.map (alternatingGroup α).subtype G

Tactic:
use ⟨g, hg3.mem_alternatingGroup⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g ⋯ ∈ (↑G : Set ↥(alternatingGroup α)) ∧
    ((alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g ⋯) =
      g

Tactic:
simpa only [SetLike.mem_coe, Subgroup.subtype_apply, and_true] using hG hg

Premises used: and_true, Subgroup.subtype_apply, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
φ : ↥G →* ↥(Subgroup.map (alternatingGroup α).subtype G) := (alternatingGroup α).subtype.subgroupMap G
f : MulActionHom (M := ↥G) (N := ↥(Subgroup.map (alternatingGroup α).subtype G))
  (⇑φ : (a : ↥G) → ↥(Subgroup.map (alternatingGroup α).subtype G)) α α :=
  { toFun := id, map_smul' := ⋯ }
rwa rwa₁ rwa₂ rwa₃ : IsPreprimitive (↥G) α
⊢ IsPreprimitive (↥(Subgroup.map (alternatingGroup α).subtype G)) α

Tactic:
rwa [← isPreprimitive_congr (f := f) ((alternatingGroup α).subtype.subgroupMap_surjective G)
      Function.bijective_id]

Premises used: Function.bijective_id, Subgroup.subtype, alternatingGroup, MonoidHom.subgroupMap_surjective, MulAction.isPreprimitive_congr
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
apply : Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥G) sᶜ)) (β := Perm (↑sᶜ : Type u_1)) toPerm
⊢ B.Subsingleton

Tactic:
apply hB.subsingleton_of_ssubset_of_stabilizer_le hB_ss_sc

Premises used: MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
g : Perm (↑sᶜ : Type u_1)
rwa rwa₁ rwa₂ rwa₃ : s.Nontrivial
⊢ sᶜᶜ.Nontrivial

Tactic:
rwa [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
g : Perm (↑sᶜ : Type u_1)
obtain :
  ∀ (k : ↥(alternatingGroup α))
    (hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ) k),
    ∃ (a : ↥(stabilizer (↥G) sᶜ)),
      Eq (α := Perm (↑sᶜ : Type u_1)) (toPerm a)
        (toPerm
          (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
            Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ) x) k hk))
⊢ ∃ (a : ↥(stabilizer (↥G) sᶜ)), toPerm a = g

Tactic:
obtain ⟨⟨k, hk⟩, rfl⟩ := alternatingGroup.stabilizer.surjective_toPerm (by rwa [compl_compl]) g

Premises used: alternatingGroup.stabilizer.surjective_toPerm, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ) k
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) k

Tactic:
rw [stabilizer_compl] at hk

Premises used: stabilizer_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
k : ↥(alternatingGroup α)
hk_1 : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ) k
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) k
⊢ Membership.mem (γ := Subgroup ↥G) (stabilizer (↥G) sᶜ) (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦ x ∈ G) k ⋯)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
k : ↥(alternatingGroup α)
hk_1 : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ) k
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) k
⊢ ∃ (a : ↥(stabilizer (↥G) sᶜ)),
    Eq (α := Perm (↑sᶜ : Type u_1)) (toPerm a)
      (toPerm
        (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
          Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ) x) k hk_1))

Tactic:
exact ⟨⟨⟨k, hG hk⟩, by aesop⟩, rfl⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < 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 α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
rw : 1 < sᶜ.ncard
⊢ sᶜ.Nontrivial

Tactic:
rw [← one_lt_ncard_iff_nontrivial]

Premises used: Set.one_lt_ncard_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ 1 < sᶜ.ncard

Tactic:
lt_of_le_of_lt h0.nonempty.ncard_pos hs

Premises used: lt_of_le_of_lt, Set.Nontrivial.nonempty, Set.Nonempty.ncard_pos