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
α : 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.Nonempty (g • B ∩ B)
Tactic:
apply Set.ncard_pigeonhole
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.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
⊢ Fintype.card α < Set.ncard (g • B) + Set.ncard B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.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
⊢ Fintype.card α < Set.ncard (g • B) + Set.ncard B
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s]
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.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 sᶜ < Set.ncard (g • B) + Set.ncard B
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ᶜ ≤ Set.ncard (g • B) + Set.ncard B
Tactic:
apply Nat.add_le_add
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 sᶜ ≤ Set.ncard (g • B)

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 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 sᶜ ≤ Set.ncard B
Tactic:
exact Set.ncard_le_ncard hsc_le_B
Proof state after:
no goals
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 α
⊢ IsPretransitive (↥G) α
Tactic:
have hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G :=
  le_trans (le_of_lt hG) inf_le_left
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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ IsPretransitive (↥G) α
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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ IsPretransitive (↥G) α
Tactic:
apply Equiv.Perm.IsPretransitive.of_partition G s
Proof state after:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ stabilizer (↥G) s ≠ ⊤
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
Tactic:
intro a ha b hb
Proof state after:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ∃ g, g • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ∃ g, g • a = b
Tactic:
obtain ⟨g, hg, H⟩ := moves_in h4 s a ha b hb
Proof state after:
case a.intro.intro
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.intro.intro
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b
Tactic:
use! g
Proof state after:
case property
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case property
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b
Tactic:
exact hG' hg
Proof state after:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ s
b : α
hb : b ∈ s
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b
Tactic:
exact H
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
Tactic:
intro a ha b hb
Proof state after:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
⊢ ∃ g, g • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
⊢ ∃ g, g • a = b
Tactic:
obtain ⟨g, hg, H⟩ := moves_in h4 (sᶜ) a ha b hb
Proof state after:
case a.intro.intro
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.intro.intro
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b
Tactic:
use! g
Proof state after:
case property
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case property
α : 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b
Tactic:
apply hG'
Proof state after:
case property.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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case property.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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b
Tactic:
rw [stabilizer_compl] at hg
Proof state after:
case property.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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

case 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 α
hG' : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b