internlm/Lean-Github huggingface dataset:
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 = B
Tactic:
intro 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
h : k • B = B
⊢ 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
h : k • B = B
⊢ False
Tactic:
apply Set.not_mem_empty 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
h : k • B = B
⊢ a ∈ ∅
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
h : k • B = B
⊢ a ∈ ∅
Tactic:
rw [← Set.inter_compl_self 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
h : k • B = B
⊢ a ∈ s ∩ 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
h : k • B = B
⊢ a ∈ s ∩ sᶜ
Tactic:
constructor
Proof state after:
case intro.intro.intro.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 α
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
h : k • B = B
⊢ a ∈ s

case intro.intro.intro.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 α
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
h : k • B = B
⊢ a ∈ 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) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
this : Set.ncard B ≤ Set.ncard s
⊢ False
Tactic:
apply Nat.lt_irrefl (Set.ncard B)
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ᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
this : Set.ncard B ≤ Set.ncard s
⊢ Set.ncard B < Set.ncard B
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ᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
this : Set.ncard B ≤ Set.ncard s
⊢ Set.ncard B < Set.ncard B
Tactic:
apply lt_of_le_of_lt this
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ᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
this : Set.ncard B ≤ Set.ncard s
⊢ Set.ncard s < Set.ncard B
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ᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
this : Set.ncard B ≤ Set.ncard s
⊢ Set.ncard s < Set.ncard B
Tactic:
simp_rw [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ᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
this : Set.ncard B ≤ Set.ncard s
⊢ 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) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
b : α
hb : b ∈ B
a : α
ha : a ∈ s
k : ↥G
hk : k • b = a
this : Set.ncard B ≤ Set.ncard s
⊢ Set.ncard s < Set.ncard sᶜ
Tactic:
exact hα
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.intro.intro.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 α
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
h : k • B = B
⊢ a ∈ s
Tactic:
exact ha
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.intro.intro.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 α
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
h : k • B = B
⊢ a ∈ sᶜ
Tactic:
rw [← hk, ← hBsc, ← h, Set.smul_mem_smul_set_iff]
Proof state after:
case intro.intro.intro.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 α
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
h : k • B = B
⊢ b ∈ B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case intro.intro.intro.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 α
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
h : k • B = B
⊢ b ∈ B
Tactic:
exact hb
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) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
⊢ ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
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) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ Set.Subsingleton B
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ Set.Subsingleton B
Tactic:
rw [← Equiv.Perm.Subtype.image_preimage_of_val 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) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ Set.Subsingleton (Subtype.val '' (Subtype.val ⁻¹' B))
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ Set.Subsingleton (Subtype.val '' (Subtype.val ⁻¹' B))
Tactic:
apply Set.Subsingleton.image
Proof state after:
case hs
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ Set.Subsingleton (Subtype.val ⁻¹' B)
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case hs
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ Set.Subsingleton (Subtype.val ⁻¹' B)
Tactic:
suffices IsTrivialBlock (Subtype.val ⁻¹' B : Set (sᶜ : Set α)) by
  apply Or.resolve_right this
  intro hB'
  apply hB_ne_sc B hB
  simp only [Set.top_eq_univ, Set.preimage_eq_univ_iff, Subtype.range_coe_subtype] at hB'
  apply Set.Subset.antisymm hBsc hB'
Proof state after:
case hs
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case hs
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)
Tactic:
suffices IsPreprimitive (stabilizer G (sᶜ : Set α)) (sᶜ : Set α) by
  refine' IsPreprimitive.has_trivial_blocks this _
  let φ' : stabilizer G (sᶜ : Set α) → G := Subtype.val
  let f' : (sᶜ : Set α) →ₑ[φ'] α := {
    toFun := Subtype.val
    map_smul' := fun m x => by simp only [SMul.smul_stabilizer_def] }
  apply MulAction.IsBlock_preimage f' hB
Proof state after:
case hs
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ IsPreprimitive ↥(stabilizer (↥G) sᶜ) ↑sᶜ
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case hs
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ IsPreprimitive ↥(stabilizer (↥G) sᶜ) ↑sᶜ
Tactic:
apply stabilizer.isPreprimitive'
Proof state after:
case hs.hsc
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ Set.Nontrivial sᶜᶜ

case hs.hG
α : 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ stabilizer (Equiv.Perm α) sᶜ ⊓ alternatingGroup α ≤ 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 α
this✝ : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton (Subtype.val ⁻¹' B)
Tactic:
apply Or.resolve_right this
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
⊢ ¬Subtype.val ⁻¹' B = ⊤
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
⊢ ¬Subtype.val ⁻¹' B = ⊤
Tactic:
intro hB'
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
hB' : Subtype.val ⁻¹' B = ⊤
⊢ 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) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
hB' : Subtype.val ⁻¹' B = ⊤
⊢ False
Tactic:
apply hB_ne_sc B hB
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
hB' : Subtype.val ⁻¹' B = ⊤
⊢ B = 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
hB' : Subtype.val ⁻¹' B = ⊤
⊢ B = sᶜ
Tactic:
simp only [Set.top_eq_univ, Set.preimage_eq_univ_iff, Subtype.range_coe_subtype] at hB'
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
hB' : {x | x ∈ sᶜ} ⊆ B
⊢ B = 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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsTrivialBlock (Subtype.val ⁻¹' B)
hB' : {x | x ∈ sᶜ} ⊆ B
⊢ B = sᶜ
Tactic:
apply Set.Subset.antisymm hBsc hB'
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) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsPreprimitive ↥(stabilizer (↥G) sᶜ) ↑sᶜ
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)
Tactic:
refine' IsPreprimitive.has_trivial_blocks this _
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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsPreprimitive ↥(stabilizer (↥G) sᶜ) ↑sᶜ
⊢ IsBlock (↥(stabilizer (↥G) sᶜ)) (Subtype.val ⁻¹' B)