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ᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
this : IsPreprimitive ↥(stabilizer (↥G) sᶜ) ↑sᶜ
⊢ IsBlock (↥(stabilizer (↥G) sᶜ)) (Subtype.val ⁻¹' B)
Tactic:
let φ' : stabilizer G (sᶜ : Set α) → G := Subtype.val
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ᶜ
φ' : ↥(stabilizer (↥G) sᶜ) → ↥G := Subtype.val
⊢ IsBlock (↥(stabilizer (↥G) sᶜ)) (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 : IsPreprimitive ↥(stabilizer (↥G) sᶜ) ↑sᶜ
φ' : ↥(stabilizer (↥G) sᶜ) → ↥G := Subtype.val
⊢ IsBlock (↥(stabilizer (↥G) sᶜ)) (Subtype.val ⁻¹' B)
Tactic:
let f' : (sᶜ : Set α) →ₑ[φ'] α := {
  toFun := Subtype.val
  map_smul' := fun m x => by simp only [SMul.smul_stabilizer_def] }
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ᶜ
φ' : ↥(stabilizer (↥G) sᶜ) → ↥G := Subtype.val
f' : ↑sᶜ →ₑ[φ'] α := { toFun := Subtype.val, map_smul' := ⋯ }
⊢ IsBlock (↥(stabilizer (↥G) sᶜ)) (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 : IsPreprimitive ↥(stabilizer (↥G) sᶜ) ↑sᶜ
φ' : ↥(stabilizer (↥G) sᶜ) → ↥G := Subtype.val
f' : ↑sᶜ →ₑ[φ'] α := { toFun := Subtype.val, map_smul' := ⋯ }
⊢ IsBlock (↥(stabilizer (↥G) sᶜ)) (Subtype.val ⁻¹' B)
Tactic:
apply MulAction.IsBlock_preimage f' 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ᶜ
φ' : ↥(stabilizer (↥G) sᶜ) → ↥G := Subtype.val
m : ↥(stabilizer (↥G) sᶜ)
x : ↑sᶜ
⊢ ↑(m • x) = φ' m • ↑x
Tactic:
simp only [SMul.smul_stabilizer_def]
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
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ᶜᶜ
Tactic:
rw [compl_compl]
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
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
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
Tactic:
exact h0
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
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
Tactic:
rw [stabilizer_compl]
Proof state after:
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:
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
Tactic:
exact le_trans (le_of_lt hG) inf_le_left
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 α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
Tactic:
intro B hB hBs
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
⊢ 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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)
Tactic:
suffices IsPreprimitive (stabilizer G s) (s : Set α) by
  refine' IsPreprimitive.has_trivial_blocks this _
  let φ' : stabilizer G s → G := Subtype.val
  let f' : s →ₑ[φ'] α := {
    toFun := Subtype.val
    map_smul' := fun ⟨m, _⟩ x => by simp }
  apply MulAction.IsBlock_preimage f' 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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
apply stabilizer.isPreprimitive' s h1
Proof state after:
case 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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
Tactic:
apply le_trans (le_of_lt hG) inf_le_left
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
this : IsTrivialBlock (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton B
Tactic:
cases' this with hB' hB'
Proof state after:
case 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' : Set.Subsingleton (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton B

case 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 = ⊤
⊢ Set.Subsingleton B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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' : Set.Subsingleton (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton B
Tactic:
rw [← Equiv.Perm.Subtype.image_preimage_of_val hBs]
Proof state after:
case 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' : Set.Subsingleton (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton (Subtype.val '' (Subtype.val ⁻¹' B))
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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' : Set.Subsingleton (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton (Subtype.val '' (Subtype.val ⁻¹' B))
Tactic:
apply Set.Subsingleton.image
Proof state after:
case inl.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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Set.Subsingleton (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton (Subtype.val ⁻¹' B)
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inl.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ᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
hB' : Set.Subsingleton (Subtype.val ⁻¹' B)
⊢ Set.Subsingleton (Subtype.val ⁻¹' B)
Tactic:
exact hB'
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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 = ⊤
⊢ Set.Subsingleton B
Tactic:
have hBs' : B = s := by
  apply Set.Subset.antisymm hBs
  intro x hx
  suffices x = Subtype.val (⟨x, hx⟩ : s) by
    rw [this, ← Set.mem_preimage, hB', Set.top_eq_univ]
    apply Set.mem_univ
  rfl
Proof state after:
case 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
⊢ Set.Subsingleton B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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
⊢ Set.Subsingleton B
Tactic:
have : ∃ g' ∈ G, g' • s ≠ s := by
  by_contra h
  push_neg at h
  apply ne_of_lt hG
  apply le_antisymm (le_of_lt hG)
  intro g' hg'
  rw [Subgroup.mem_inf] at hg' ⊢
  exact ⟨h g' hg'.left, hg'.right⟩
Proof state after:
case 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
this : ∃ g' ∈ G, g' • s ≠ s
⊢ Set.Subsingleton B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case 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
this : ∃ g' ∈ G, g' • s ≠ s
⊢ Set.Subsingleton B
Tactic:
obtain ⟨g', hg', hg's⟩ := this
Proof state after:
case inr.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) α
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
⊢ Set.Subsingleton B
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
case inr.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) α
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
⊢ Set.Subsingleton B
Tactic:
cases' IsBlock.def_one.mp hB ⟨g', hg'⟩ with h h
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
⊢ Set.Subsingleton B

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
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 = ⊤
⊢ B = s
Tactic:
apply Set.Subset.antisymm hBs
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 = ⊤
⊢ s ⊆ B