awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have pos : ∀ (hab : a = b),
  ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have neg : ∀ (hab : ¬a = b),
  ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have h : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) 1 ∧
  HSMul.hSMul (α := ↥(alternatingGroup α)) 1 a = b
Tactic: use 1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have pos : ∀ (ht : 2 < t.ncard),
  ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
Tactic: by_cases ht : 2 < t.ncard
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have neg : ∀ (ht : ¬2 < t.ncard),
  ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
Tactic: by_cases ht : 2 < t.ncard
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have ht₁ : ncard (α := α) {a, b} < t.ncard
Tactic: rw [← Set.ncard_pair hab] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have ht₁ : (t \ {a, b}).Nonempty
Tactic: replace ht := Set.diff_nonempty_of_ncard_lt_ncard ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have pos : ∀ (c : α) (hct : c ∈ t) (hc : c ∉ {a, b}),
  ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
Tactic: obtain ⟨c, hct, hc⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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}
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have hc₁ : ¬c = a ∧ c ∉ {b}
Tactic: simp only [mem_insert_iff, not_or] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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}
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have pos : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
  (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) sorry)
Tactic: refine ⟨⟨swap c a * swap a b, by simp [hab, hc.1]⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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) ⋯)
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have pos₁ : HSMul.hSMul (α := ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) sorry) a =
  b
Tactic: refine ⟨⟨swap c a * swap a b, by simp [hab, hc.1]⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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}
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) ⋯)
have pos : ∀ ⦃b_1 : α⦄, b_1 ∈ t → Function.comp (β := α) (⇑(swap c a) : (a : α) → α) (⇑(swap a b) : (a : α) → α) b_1 ∈ t
Tactic: simp only [mem_stabilizer_set' t.toFinite, Subgroup.mk_smul, Perm.smul_def, coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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}
⊢ HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap c a * swap a b) ⋯) a =
    b
have pos : Function.comp (β := α) (⇑(swap c a) : (a : α) → α) (⇑(swap a b) : (a : α) → α) a = b
Tactic: simp only [Subgroup.mk_smul, Perm.smul_def, coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have this : t.ncard + tᶜ.ncard = Nat.card α
Tactic: have := ncard_add_ncard_compl t
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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 α
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have 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
Tactic: obtain ⟨c, d, hc, hd, hcd⟩ := (one_lt_ncard_iff tᶜ.toFinite).mp (by grind)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have neg : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
  (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) sorry)
Tactic: refine ⟨⟨swap a b * swap c d, by simp [hab, hcd]⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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) ⋯)
⊢ ∃ (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t) g ∧ g • a = b
have neg₁ : HSMul.hSMul (α := ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) sorry) a =
  b
Tactic: refine ⟨⟨swap a b * swap c d, by simp [hab, hcd]⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) t)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) ⋯)
have neg : ∀ ⦃b_1 : α⦄, b_1 ∈ t → Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap c d) : (a : α) → α) b_1 ∈ t
Tactic: simp only [mem_stabilizer_set' t.toFinite, Subgroup.mk_smul, Perm.smul_def, coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap c d) ⋯) a =
    b
have neg : Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap c d) : (a : α) → α) a = b
Tactic: simp only [Subgroup.smul_def, Perm.smul_def, Perm.coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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 = ⊤
have obtain : ∀ (g : Perm α) (hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g) (hg3 : g.IsThreeCycle), G = ⊤
Tactic: obtain ⟨g, hg, hg3⟩ := exists_mem_stabilizer_isThreeCycle s h4
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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 = ⊤
have rw : alternatingGroup α ≤ Subgroup.map (alternatingGroup α).subtype G
Tactic: rw [eq_top_iff, ← Subgroup.map_subtype_le_map_subtype,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ alternatingGroup α ≤ Subgroup.map (alternatingGroup α).subtype G
have apply : g ∈ Subgroup.map (alternatingGroup α).subtype G
Tactic: apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem _ hg3
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ alternatingGroup α ≤ Subgroup.map (alternatingGroup α).subtype G
have apply₁ : IsPreprimitive (↥(Subgroup.map (alternatingGroup α).subtype G)) α
Tactic: apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem _ hg3
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
have h : Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g sorry ∈ (↑G : Set ↥(alternatingGroup α)) ∧
  ((alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g sorry) =
    g
Tactic: use ⟨g, hg3.mem_alternatingGroup⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ B.Subsingleton
have apply : Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥G) sᶜ)) (β := Perm (↑sᶜ : Type u_1)) toPerm
Tactic: apply hB.subsingleton_of_ssubset_of_stabilizer_le hB_ss_sc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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)
⊢ ∃ (a : ↥(stabilizer (↥G) sᶜ)), toPerm a = g
have 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))
Tactic: obtain ⟨⟨k, hk⟩, rfl⟩ := alternatingGroup.stabilizer.surjective_toPerm (by rwa [compl_compl]) g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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
⊢ ∃ (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))
have hk₁ : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) k
Tactic: rw [stabilizer_compl] at hk
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have this : s.ncard + sᶜ.ncard = Nat.card α
Tactic: have := ncard_add_ncard_compl s
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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 α
⊢ sᶜ.Nontrivial
have rw : 1 < sᶜ.ncard
Tactic: rw [← one_lt_ncard_iff_nontrivial]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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 α
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have h1 : sᶜ.Nontrivial
Tactic: have h1 : sᶜ.Nontrivial := by
    rw [← one_lt_ncard_iff_nontrivial]
    exact lt_of_le_of_lt h0.nonempty.ncard_pos hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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 α
h1 : sᶜ.Nontrivial
⊢ 4 < Nat.card α
have h0₁ : 1 < s.ncard
Tactic: rw [← Set.one_lt_ncard_iff_nontrivial] at h0
Cleared hypotheses: h0, hs, this, h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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 α
h1 : sᶜ.Nontrivial
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have hα : 4 < Nat.card α
Tactic: have hα : 4 < Nat.card α := by
    rw [← Set.one_lt_ncard_iff_nontrivial] at h0
    grind
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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 α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have right : ∀ (b : Subgroup ↥(alternatingGroup α)), stabilizer (↥(alternatingGroup α)) s < b → b = ⊤
Tactic: use stabilizer_ne_top h0.nonempty h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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 α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
⊢ G = ⊤
have right : IsPreprimitive (↥G) α
Tactic: suffices IsPreprimitive G α from subgroup_eq_top_of_isPreprimitive hα G hG.le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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 α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
⊢ IsPreprimitive (↥G) α
have this₁ : IsPretransitive (↥G) α
Tactic: have := G.isPretransitive_of_stabilizer_lt hG
    (exists_mem_stabilizer_smul_eq (Nat.le_of_succ_le hα))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
⊢ IsPreprimitive (↥G) α
have right : ∀ {B : Set α}, IsBlock (↥G) B → IsTrivialBlock B
Tactic: apply IsPreprimitive.mk
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
⊢ IsTrivialBlock B
have right : ¬B.Subsingleton → B = univ
Tactic: rw [IsTrivialBlock, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ B = univ
have apply : Nat.card α < B.ncard * 2
Tactic: apply hB.eq_univ_of_card_lt
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ Nat.card α < B.ncard * 2
have this₁ : sᶜ.ncard ≤ B.ncard
Tactic: have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ B = univ
have right : sᶜ ⊆ B
Tactic: suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    grind