Theorem: alternatingGroup.stabilizer_ne_top (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hssc : Set.Nontrivial s ∨ Set.Nontrivial sᶜ
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
cases' hssc with hs' hsc'
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hsc' : Set.Nontrivial sᶜ
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

State before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hsc' : Set.Nontrivial sᶜ
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
exact stabilizer_ne_top' s hs hsc'
State after:
no goals

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
rw [← stabilizer_compl]
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤
Tactic:
rw [← compl_compl s] at hs'
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial sᶜᶜ
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial sᶜᶜ
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤
Tactic:
exact stabilizer_ne_top' (sᶜ) hsc hs'
State after:
no goals