internlm/Lean-Github huggingface dataset:
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
⊢ s ⊆ B
Tactic:
intro x hx
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ x ∈ 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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ x ∈ B
Tactic:
suffices x = Subtype.val (⟨x, hx⟩ : s) by
  rw [this, ← Set.mem_preimage, hB', Set.top_eq_univ]
  apply Set.mem_univ
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ x = ↑{ val := x, property := hx }
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ x = ↑{ val := x, property := hx }
Tactic:
rfl
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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
this : x = ↑{ val := x, property := hx }
⊢ x ∈ B
Tactic:
rw [this, ← Set.mem_preimage, hB', Set.top_eq_univ]
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
this : x = ↑{ val := x, property := hx }
⊢ { val := x, property := hx } ∈ Set.univ
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
this : x = ↑{ val := x, property := hx }
⊢ { val := x, property := hx } ∈ Set.univ
Tactic:
apply Set.mem_univ
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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
⊢ ∃ g' ∈ G, g' • s ≠ s
Tactic:
by_contra h
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ¬∃ g' ∈ G, g' • s ≠ 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) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ¬∃ g' ∈ G, g' • s ≠ s
⊢ False
Tactic:
push_neg at h
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = 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) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
⊢ False
Tactic:
apply ne_of_lt hG
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α = G ⊓ alternatingGroup α
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α = G ⊓ alternatingGroup α
Tactic:
apply le_antisymm (le_of_lt hG)
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
⊢ G ⊓ alternatingGroup α ≤ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Tactic:
intro g' hg'
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
g' : Equiv.Perm α
hg' : g' ∈ G ⊓ alternatingGroup α
⊢ g' ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
g' : Equiv.Perm α
hg' : g' ∈ G ⊓ alternatingGroup α
⊢ g' ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Tactic:
rw [Subgroup.mem_inf] at hg' ⊢
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
g' : Equiv.Perm α
hg' : g' ∈ G ∧ g' ∈ alternatingGroup α
⊢ g' ∈ stabilizer (Equiv.Perm α) s ∧ g' ∈ alternatingGroup α
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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
h : ∀ g' ∈ G, g' • s = s
g' : Equiv.Perm α
hg' : g' ∈ G ∧ g' ∈ alternatingGroup α
⊢ g' ∈ stabilizer (Equiv.Perm α) s ∧ g' ∈ alternatingGroup α
Tactic:
exact ⟨h g' hg'.left, hg'.right⟩
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inl
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : { val := g', property := hg' } • B = B
⊢ Set.Subsingleton B
Tactic:
exfalso
Proof state after:
case inr.intro.intro.inl
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : { val := g', property := hg' } • B = B
⊢ False
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inl
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : { val := g', property := hg' } • B = B
⊢ False
Tactic:
apply hg's
Proof state after:
case inr.intro.intro.inl
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : { val := g', property := hg' } • B = B
⊢ g' • s = s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inl
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : { val := g', property := hg' } • B = B
⊢ g' • s = s
Tactic:
rw [← hBs']
Proof state after:
case inr.intro.intro.inl
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : { val := g', property := hg' } • B = B
⊢ g' • B = B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inl
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : { val := g', property := hg' } • B = B
⊢ g' • B = B
Tactic:
exact h
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inr
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : Disjoint ({ val := g', property := hg' } • B) B
⊢ Set.Subsingleton B
Tactic:
suffices (g' • B).Subsingleton by
  apply Set.subsingleton_of_image _ B this
  apply Function.Bijective.injective (MulAction.bijective _)
Proof state after:
case inr.intro.intro.inr
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : Disjoint ({ val := g', property := hg' } • B) B
⊢ Set.Subsingleton (g' • B)
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inr
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : Disjoint ({ val := g', property := hg' } • B) B
⊢ Set.Subsingleton (g' • B)
Tactic:
apply hB_not_le_sc ((⟨g', hg'⟩ : G) • B) (IsBlock_of_block _ hB)
Proof state after:
case inr.intro.intro.inr
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : Disjoint ({ val := g', property := hg' } • B) B
⊢ { val := g', property := hg' } • B ⊆ sᶜ
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inr
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : Disjoint ({ val := g', property := hg' } • B) B
⊢ { val := g', property := hg' } • B ⊆ sᶜ
Tactic:
rw [← hBs']
Proof state after:
case inr.intro.intro.inr
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : Disjoint ({ val := g', property := hg' } • B) B
⊢ { val := g', property := hg' } • B ⊆ Bᶜ
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.intro.intro.inr
α : 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
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = ⊤
hBs' : B = s
g' : Equiv.Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : Disjoint ({ val := g', property := hg' } • B) B
⊢ { val := g', property := hg' } • B ⊆ Bᶜ
Tactic:
exact Disjoint.subset_compl_right h
Proof state after:
no goals