internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard s + Set.ncard sᶜ < ?has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.m
Tactic:
apply Nat.add_lt_add_right _ (Set.ncard (sᶜ : Set α))
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ ℕ

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard s < ?m.113382
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ ℕ

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard s < ?m.113382
Tactic:
use Set.ncard (sᶜ : Set α)
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard s < Set.ncard sᶜ
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard s < Set.ncard sᶜ
Tactic:
exact hα
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a.h₁
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard sᶜ ≤ Set.ncard (g • B)
Tactic:
apply le_trans (Set.ncard_le_ncard hsc_le_B)
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a.h₁
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard B ≤ Set.ncard (g • B)
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a.h₁
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard B ≤ Set.ncard (g • B)
Tactic:
apply le_of_eq
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a.h₁.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard B = Set.ncard (g • B)
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a.h₁.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard B = Set.ncard (g • B)
Tactic:
rw [MulAction.smul_set_ncard_eq]
Proof state after:
no goals
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
⊢ 4 < Fintype.card α
Tactic:
have h0 : 2 ≤ Set.ncard s := by
  rw [Nat.succ_le_iff, Set.one_lt_ncard_iff_nontrivial]
  exact h0'
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Fintype.card α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Fintype.card α
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Set.ncard s + Set.ncard sᶜ
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Set.ncard s + Set.ncard sᶜ
Tactic:
change 2 + 2 < _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 < Set.ncard s + Set.ncard sᶜ
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 < Set.ncard s + Set.ncard sᶜ
Tactic:
apply lt_of_le_of_lt
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 ≤ ?b

case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ ?b < Set.ncard s + Set.ncard sᶜ

case b
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ ℕ
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 ≤ ?b

case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ ?b < Set.ncard s + Set.ncard sᶜ

case b
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ ℕ
Tactic:
exact Nat.add_le_add_right h0 2
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ Set.ncard s + 2 < Set.ncard s + Set.ncard sᶜ
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ Set.ncard s + 2 < Set.ncard s + Set.ncard sᶜ
Tactic:
apply Nat.add_lt_add_left
Proof state after:
case a.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 < Set.ncard sᶜ
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case a.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 < Set.ncard sᶜ
Tactic:
exact lt_of_le_of_lt h0 hs
Proof state after:
no goals
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
constructor
Proof state after:
case out
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)
Tactic:
constructor
Proof state after:
case out.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

case out.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
⊢ ∀ (b : Subgroup ↥(alternatingGroup α)), stabilizer (↥(alternatingGroup α)) s < b → b = ⊤
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
exact stabilizer_ne_top' s h0'.nonempty h1'
Proof state after:
no goals
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
⊢ ∀ (b : Subgroup ↥(alternatingGroup α)), stabilizer (↥(alternatingGroup α)) s < b → b = ⊤
Tactic:
intro G' hG'
Proof state after:
case out.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ G' = ⊤
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ G' = ⊤
Tactic:
suffices alternatingGroup α ≤ G'.map (alternatingGroup α).subtype by
  rw [eq_top_iff]; intro g _
  obtain ⟨g', hg', hgg'⟩ := this g.prop
  simp only [Subgroup.coeSubtype, SetLike.coe_eq_coe] at hgg'
  rw [← hgg']; exact hg'
Proof state after:
case out.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
Tactic:
apply le_of_isPreprimitive s hα
Proof state after:
case out.right.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'

case out.right.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ IsPreprimitive (↥(Subgroup.map (Subgroup.subtype (alternatingGroup α)) G')) α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
⊢ G' = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
⊢ ⊤ ≤ G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
⊢ ⊤ ≤ G'
Tactic:
intro g _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
⊢ g ∈ G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
⊢ g ∈ G'
Tactic:
obtain ⟨g', hg', hgg'⟩ := this g.prop
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : (Subgroup.subtype (alternatingGroup α)) g' = ↑g
⊢ g ∈ G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : (Subgroup.subtype (alternatingGroup α)) g' = ↑g
⊢ g ∈ G'
Tactic:
simp only [Subgroup.coeSubtype, SetLike.coe_eq_coe] at hgg'
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g ∈ G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g ∈ G'
Tactic:
rw [← hgg']
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g' ∈ G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g' ∈ G'
Tactic:
exact hg'
Proof state after:
no goals