internlm/Lean-Github huggingface dataset:
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:
exact 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
⊢ stabilizer (↥G) s ≠ ⊤
Tactic:
intro h
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
h : stabilizer (↥G) s = ⊤
⊢ False
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
h : stabilizer (↥G) s = ⊤
⊢ False
Tactic:
apply (lt_iff_le_not_le.mp hG).right
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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Tactic:
rw [le_inf_iff]
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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s ∧ G ⊓ alternatingGroup α ≤ alternatingGroup α
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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s ∧ G ⊓ alternatingGroup α ≤ alternatingGroup α
Tactic:
constructor
Proof state after:
case a.left
α : 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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s

case a.right
α : 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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ alternatingGroup α
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.left
α : 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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s
Tactic:
intro g
Proof state after:
case a.left
α : 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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
⊢ g ∈ G ⊓ alternatingGroup α → g ∈ stabilizer (Equiv.Perm α) s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.left
α : 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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
⊢ g ∈ G ⊓ alternatingGroup α → g ∈ stabilizer (Equiv.Perm α) s
Tactic:
rw [Subgroup.mem_inf, mem_stabilizer_iff]
Proof state after:
case a.left
α : 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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
⊢ g ∈ G ∧ g ∈ alternatingGroup α → g • s = s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.left
α : 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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
⊢ g ∈ G ∧ g ∈ alternatingGroup α → g • s = s
Tactic:
rintro ⟨hg, _⟩
Proof state after:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ g • s = s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ g • s = s
Tactic:
rw [← Subgroup.coe_mk G g hg]
Proof state after:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ ↑{ val := g, property := hg } • s = s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ ↑{ val := g, property := hg } • s = s
Tactic:
change (⟨g, hg⟩ : ↥G) • s = s
Proof state after:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ { val := g, property := hg } • s = s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ { val := g, property := hg } • s = s
Tactic:
rw [← mem_stabilizer_iff, h]
Proof state after:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ ⊤
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.left.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
h : stabilizer (↥G) s = ⊤
g : Equiv.Perm α
hg : g ∈ G
right✝ : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ ⊤
Tactic:
exact Subgroup.mem_top _
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case a.right
α : 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
h : stabilizer (↥G) s = ⊤
⊢ G ⊓ alternatingGroup α ≤ alternatingGroup α
Tactic:
exact inf_le_right
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 α
this : IsPretransitive (↥G) α
⊢ ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
Tactic:
intro B hB hBsc
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) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
⊢ False
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) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
⊢ False
Tactic:
obtain ⟨b, hb⟩ := h1.nonempty
Proof state after:
case 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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ sᶜ
⊢ False
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ sᶜ
⊢ False
Tactic:
rw [← hBsc] at hb
Proof state after:
case 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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
⊢ False
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
⊢ False
Tactic:
obtain ⟨a, ha⟩ := h0.nonempty
Proof state after:
case 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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
⊢ False
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
⊢ False
Tactic:
obtain ⟨k, hk⟩ := exists_smul_eq G b a
Proof state after:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ False
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ False
Tactic:
suffices Set.ncard (B : Set α) ≤ Set.ncard s by
  apply Nat.lt_irrefl (Set.ncard B)
  apply lt_of_le_of_lt this
  simp_rw [hBsc]; exact hα
Proof state after:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ Set.ncard B ≤ Set.ncard s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ Set.ncard B ≤ Set.ncard s
Tactic:
rw [← smul_set_ncard_eq k B]
Proof state after:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ Set.ncard (k • B) ≤ Set.ncard s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ Set.ncard (k • B) ≤ Set.ncard s
Tactic:
apply Set.ncard_le_ncard (ht := Set.toFinite s)
Proof state after:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ k • B ⊆ s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ k • B ⊆ s
Tactic:
rw [← Set.disjoint_compl_right_iff_subset, ← hBsc]
Proof state after:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ Disjoint (k • B) B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ Disjoint (k • B) B
Tactic:
apply or_iff_not_imp_left.mp (IsBlock.def_one.mp hB k)
Proof state after:
case intro.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 α
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
⊢ ¬k • B = B