Theorem: alternatingGroup.isMaximalStab' (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
⊢ 4 < Fintype.card α
Tactic:
have h0 : 2 ≤ Set.ncard s := by
  rw [Nat.succ_le_iff, Set.one_lt_ncard_iff_nontrivial]
  exact h0'
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Fintype.card α

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Fintype.card α
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Set.ncard s + Set.ncard sᶜ

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 4 < Set.ncard s + Set.ncard sᶜ
Tactic:
change 2 + 2 < _
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 < Set.ncard s + Set.ncard sᶜ

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 < Set.ncard s + Set.ncard sᶜ
Tactic:
apply lt_of_le_of_lt
State after:
case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 ≤ ?b

case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ ?b < Set.ncard s + Set.ncard sᶜ

case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ ℕ

State before:
case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 + 2 ≤ ?b

case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ ?b < Set.ncard s + Set.ncard sᶜ

case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ ℕ
Tactic:
exact Nat.add_le_add_right h0 2
State after:
case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ Set.ncard s + 2 < Set.ncard s + Set.ncard sᶜ

State before:
case 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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ Set.ncard s + 2 < Set.ncard s + Set.ncard sᶜ
Tactic:
apply Nat.add_lt_add_left
State after:
case a.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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 < Set.ncard sᶜ

State before:
case a.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ᶜ
h0 : 2 ≤ Set.ncard s
⊢ 2 < Set.ncard sᶜ
Tactic:
exact lt_of_le_of_lt h0 hs
State after:
no goals

State before:
α : 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 α
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
constructor
State after:
case out
α : 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 α
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

State before:
case out
α : 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 α
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)
Tactic:
constructor
State after:
case out.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 α
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

case out.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 α
⊢ ∀ (b : Subgroup ↥(alternatingGroup α)), stabilizer (↥(alternatingGroup α)) s < b → b = ⊤

State before:
case out.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 α
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
exact stabilizer_ne_top' s h0'.nonempty h1'
State after:
no goals

State before:
case out.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 α
⊢ ∀ (b : Subgroup ↥(alternatingGroup α)), stabilizer (↥(alternatingGroup α)) s < b → b = ⊤
Tactic:
intro G' hG'
State after:
case out.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' = ⊤

State before:
case out.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' = ⊤
Tactic:
suffices alternatingGroup α ≤ G'.map (alternatingGroup α).subtype by
  rw [eq_top_iff]; intro g _
  obtain ⟨g', hg', hgg'⟩ := this g.prop
  simp only [Subgroup.coeSubtype, SetLike.coe_eq_coe] at hgg'
  rw [← hgg']; exact hg'
State after:
case out.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'
⊢ alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'

State before:
case out.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'
⊢ alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
Tactic:
apply le_of_isPreprimitive s hα
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'
⊢ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'

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')) α

State before:
α : 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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
⊢ G' = ⊤
Tactic:
rw [eq_top_iff]
State after:
α : 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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
⊢ ⊤ ≤ G'

State before:
α : 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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
⊢ ⊤ ≤ G'
Tactic:
intro g _
State after:
α : 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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
⊢ g ∈ G'

State before:
α : 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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
⊢ g ∈ G'
Tactic:
obtain ⟨g', hg', hgg'⟩ := this g.prop
State after:
case intro.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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : (Subgroup.subtype (alternatingGroup α)) g' = ↑g
⊢ g ∈ G'

State before:
case intro.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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : (Subgroup.subtype (alternatingGroup α)) g' = ↑g
⊢ g ∈ G'
Tactic:
simp only [Subgroup.coeSubtype, SetLike.coe_eq_coe] at hgg'
State after:
case intro.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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g ∈ G'

State before:
case intro.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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g ∈ G'
Tactic:
rw [← hgg']
State after:
case intro.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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g' ∈ G'

State before:
case intro.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'
this : alternatingGroup α ≤ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
g : ↥(alternatingGroup α)
a✝ : g ∈ ⊤
g' : ↥(alternatingGroup α)
hg' : g' ∈ ↑G'
hgg' : g' = g
⊢ g' ∈ G'
Tactic:
exact hg'
State after:
no goals

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]
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'

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'
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'

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'
State after:
no goals

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α)
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 α

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]
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 α

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
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 α

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
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 α

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]
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 α

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'⟩
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 α

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'
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'

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]
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

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'⟩
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

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
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

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'
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

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
State after:
no goals

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
State after:
no goals

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
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

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'
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

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
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

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'
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

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]
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

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
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

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]
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

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 α)) _
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 α)

State before:
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 α)
Tactic:
apply h
State after:
case out.right.a.hG.right.a.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' ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α

State before:
case out.right.a.hG.right.a.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' ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ⊓ alternatingGroup α
Tactic:
rw [Subgroup.mem_inf]
State after:
case out.right.a.hG.right.a.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' ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ∧ ↑g' ∈ alternatingGroup α

State before:
case out.right.a.hG.right.a.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' ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G' ∧ ↑g' ∈ alternatingGroup α
Tactic:
apply And.intro _ g'.prop
State after:
α : 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' ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'

State before:
α : 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' ∈ Subgroup.map (Subgroup.subtype (alternatingGroup α)) G'
Tactic:
simp only [Subgroup.mem_map, Subgroup.coeSubtype, SetLike.coe_eq_coe, exists_prop, exists_eq_right]
State after:
α : 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' ∈ G'

State before:
α : 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' ∈ G'
Tactic:
exact hg'
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
⊢ 2 ≤ Set.ncard s
Tactic:
rw [Nat.succ_le_iff, Set.one_lt_ncard_iff_nontrivial]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
⊢ Set.Nontrivial s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs : Set.ncard s < Set.ncard sᶜ
⊢ Set.Nontrivial s
Tactic:
exact h0'
State after:
no goals