internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
Tactic:
rw [← Subgroup.subgroupOf_map_subtype, Subgroup.map_subtype_le_map_subtype]
Proof state after:
case out.right.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ Subgroup.subgroupOf (stabilizer (Equiv.Perm α) s) (alternatingGroup α) ≤ G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ Subgroup.subgroupOf (stabilizer (Equiv.Perm α) s) (alternatingGroup α) ≤ G'
Tactic:
rw [MulAction.stabilizer_subgroupOf_eq] at hG'
Proof state after:
case out.right.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : Subgroup.subgroupOf (stabilizer (Equiv.Perm α) s) (alternatingGroup α) < G'
⊢ Subgroup.subgroupOf (stabilizer (Equiv.Perm α) s) (alternatingGroup α) ≤ G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : Subgroup.subgroupOf (stabilizer (Equiv.Perm α) s) (alternatingGroup α) < G'
⊢ Subgroup.subgroupOf (stabilizer (Equiv.Perm α) s) (alternatingGroup α) ≤ G'
Tactic:
exact le_of_lt hG'
Proof state after:
no goals
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ IsPreprimitive (↥(Subgroup.map (Subgroup.subtype (alternatingGroup α)) G')) α
Tactic:
apply isPreprimitive_of_stabilizer_lt s h0' h1' hs (le_of_lt hα)
Proof state after:
case out.right.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α <
    Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α <
    Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α
Tactic:
rw [lt_iff_le_not_le]
Proof state after:
case out.right.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤
      Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ∧
    ¬Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
        stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤
      Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ∧
    ¬Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
        stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Tactic:
constructor
Proof state after:
case out.right.a.hG.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤
    Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α

case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ ¬Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
      stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤
    Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α
Tactic:
intro g
Proof state after:
case out.right.a.hG.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α →
    g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α →
    g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α
Tactic:
simp only [Subgroup.mem_inf]
Proof state after:
case out.right.a.hG.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
⊢ g ∈ stabilizer (Equiv.Perm α) s ∧ g ∈ alternatingGroup α →
    g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ∧ g ∈ alternatingGroup α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
⊢ g ∈ stabilizer (Equiv.Perm α) s ∧ g ∈ alternatingGroup α →
    g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ∧ g ∈ alternatingGroup α
Tactic:
rintro ⟨hg, hg'⟩
Proof state after:
case out.right.a.hG.left.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ∧ g ∈ alternatingGroup α
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.left.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ∧ g ∈ alternatingGroup α
Tactic:
refine' And.intro _ hg'
Proof state after:
case out.right.a.hG.left.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.left.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ g ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
Tactic:
simp only [Subgroup.mem_map, Subgroup.coeSubtype, exists_prop]
Proof state after:
case out.right.a.hG.left.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ ∃ x ∈ G', ↑x = g
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.left.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ ∃ x ∈ G', ↑x = g
Tactic:
use ⟨g, hg'⟩
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ { val := g, property := hg' } ∈ G' ∧ ↑{ val := g, property := hg' } = g
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ { val := g, property := hg' } ∈ G' ∧ ↑{ val := g, property := hg' } = g
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ { val := g, property := hg' } ∈ G'

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ ↑{ val := g, property := hg' } = g
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ { val := g, property := hg' } ∈ G'
Tactic:
apply le_of_lt hG'
Proof state after:
case h.left.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ { val := g, property := hg' } ∈ stabilizer (↥(alternatingGroup α)) s
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case h.left.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ { val := g, property := hg' } ∈ stabilizer (↥(alternatingGroup α)) s
Tactic:
simpa only [mem_stabilizer_iff] using hg
Proof state after:
no goals
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) s
hg' : g ∈ alternatingGroup α
⊢ ↑{ val := g, property := hg' } = g
Tactic:
rfl
Proof state after:
no goals
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
⊢ ¬Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
      stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Tactic:
intro h
Proof state after:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
⊢ False
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s < G'
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
⊢ False
Tactic:
rw [lt_iff_le_not_le] at hG'
Proof state after:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
⊢ False
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
⊢ False
Tactic:
apply hG'.right
Proof state after:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
⊢ G' ≤ stabilizer (↥(alternatingGroup α)) s
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
⊢ G' ≤ stabilizer (↥(alternatingGroup α)) s
Tactic:
intro g' hg'
Proof state after:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ g' ∈ stabilizer (↥(alternatingGroup α)) s
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ g' ∈ stabilizer (↥(alternatingGroup α)) s
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ g' • s = s
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ g' • s = s
Tactic:
change (g' : Equiv.Perm α) • s = s
Proof state after:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ ↑g' • s = s
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ ↑g' • s = s
Tactic:
rw [← mem_stabilizer_iff]
Proof state after:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ ↑g' ∈ stabilizer (Equiv.Perm α) s
Theorem: alternatingGroup.isMaximalStab'
Proof state before:
case out.right.a.hG.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ ↑g' ∈ stabilizer (Equiv.Perm α) s
Tactic:
apply @inf_le_left (Subgroup (Equiv.Perm α)) _
Proof state after:
case out.right.a.hG.right.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ ↑g' ∈ stabilizer (Equiv.Perm α) s ⊓ ?out.right.a.hG.right.b

case out.right.a.hG.right.b
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
hα : 4 < Fintype.card α
G' : Subgroup ↥(alternatingGroup α)
hG' : stabilizer (↥(alternatingGroup α)) s ≤ G' ∧ ¬G' ≤ stabilizer (↥(alternatingGroup α)) s
h :
  Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α ≤
    stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
g' : ↥(alternatingGroup α)
hg' : g' ∈ G'
⊢ Subgroup (Equiv.Perm α)