Theorem: alternatingGroup.Stabilizer.isMaximal (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
have hα : 3 ≤ Fintype.card α := by
  rw [← Set.ncard_pos, ← Nat.succ_le_iff] at h0 h1
  refine' three_le h0 _ hs
  rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s]
  exact Nat.lt_add_of_pos_right h1
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
have : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial]
  apply lt_of_lt_of_le _ hα
  norm_num
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
by_cases h0' : Set.Nontrivial s
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
by_cases h1' : Set.Nontrivial sᶜ
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : ¬Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : ¬Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
cases' Nat.lt_trichotomy (Set.ncard s) (Set.ncard (sᶜ : Set α)) with hs' hs'
State after:
case pos.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s < Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case pos.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ ∨ Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : ¬Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
case pos.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ ∨ Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : ¬Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
cases' hs' with hs' hs'
State after:
case pos.inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : ¬Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ 3 ≤ Fintype.card α
Tactic:
rw [← Set.ncard_pos, ← Nat.succ_le_iff] at h0 h1
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Nat.succ 0 ≤ Set.ncard s
h1 : Nat.succ 0 ≤ Set.ncard sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ 3 ≤ Fintype.card α

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Nat.succ 0 ≤ Set.ncard s
h1 : Nat.succ 0 ≤ Set.ncard sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ 3 ≤ Fintype.card α
Tactic:
refine' three_le h0 _ hs
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Nat.succ 0 ≤ Set.ncard s
h1 : Nat.succ 0 ≤ Set.ncard sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ Set.ncard s < Fintype.card α

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Nat.succ 0 ≤ Set.ncard s
h1 : Nat.succ 0 ≤ Set.ncard sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ Set.ncard s < 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 : Nat.succ 0 ≤ Set.ncard s
h1 : Nat.succ 0 ≤ Set.ncard sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ Set.ncard s < Set.ncard s + Set.ncard sᶜ

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Nat.succ 0 ≤ Set.ncard s
h1 : Nat.succ 0 ≤ Set.ncard sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
⊢ Set.ncard s < Set.ncard s + Set.ncard sᶜ
Tactic:
exact Nat.lt_add_of_pos_right h1
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
⊢ Nontrivial α
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
⊢ 1 < Fintype.card α

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
⊢ 1 < Fintype.card α
Tactic:
apply lt_of_lt_of_le _ hα
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
⊢ 1 < 3

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
⊢ 1 < 3
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
⊢ ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
Tactic:
intro t ht ht'
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
Tactic:
suffices ∃ a : α, t = ({a} : Set α) by
  obtain ⟨a, rfl⟩ := this
  have : stabilizer (alternatingGroup α) ({a} : Set α) = stabilizer (alternatingGroup α) a := by
    ext
    simp only [mem_stabilizer_iff, Set.smul_set_singleton, Set.singleton_eq_singleton_iff]
  rw [this]
  apply hasMaximalStabilizersOfPreprimitive
  apply AlternatingGroup.isPreprimitive hα
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
⊢ ∃ a, t = {a}

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this✝ : Nontrivial α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
this : ∃ a, t = {a}
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
Tactic:
obtain ⟨a, rfl⟩ := this
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
⊢ Subgroup.IsMaximal (stabilizer ↥(alternatingGroup α) {a})

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
⊢ Subgroup.IsMaximal (stabilizer ↥(alternatingGroup α) {a})
Tactic:
have : stabilizer (alternatingGroup α) ({a} : Set α) = stabilizer (alternatingGroup α) a := by
  ext
  simp only [mem_stabilizer_iff, Set.smul_set_singleton, Set.singleton_eq_singleton_iff]
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this✝ : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
this : stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
⊢ Subgroup.IsMaximal (stabilizer ↥(alternatingGroup α) {a})

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this✝ : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
this : stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
⊢ Subgroup.IsMaximal (stabilizer ↥(alternatingGroup α) {a})
Tactic:
rw [this]
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this✝ : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
this : stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) a)

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this✝ : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
this : stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) a)
Tactic:
apply hasMaximalStabilizersOfPreprimitive
State after:
case intro.hpGX
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this✝ : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
this : stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
⊢ IsPreprimitive (↥(alternatingGroup α)) α

State before:
case intro.hpGX
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this✝ : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
this : stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Tactic:
apply AlternatingGroup.isPreprimitive hα
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
⊢ stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
Tactic:
ext
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
x✝ : ↥(alternatingGroup α)
⊢ x✝ ∈ stabilizer ↥(alternatingGroup α) {a} ↔ x✝ ∈ stabilizer (↥(alternatingGroup α)) a

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
x✝ : ↥(alternatingGroup α)
⊢ x✝ ∈ stabilizer ↥(alternatingGroup α) {a} ↔ x✝ ∈ stabilizer (↥(alternatingGroup α)) a
Tactic:
simp only [mem_stabilizer_iff, Set.smul_set_singleton, Set.singleton_eq_singleton_iff]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
⊢ ∃ a, t = {a}
Tactic:
obtain ⟨a, ha⟩ := ht
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht' : Set.Subsingleton t
a : α
ha : a ∈ t
⊢ ∃ a, t = {a}

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht' : Set.Subsingleton t
a : α
ha : a ∈ t
⊢ ∃ a, t = {a}
Tactic:
use a
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht' : Set.Subsingleton t
a : α
ha : a ∈ t
⊢ t = {a}

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
t : Set α
ht' : Set.Subsingleton t
a : α
ha : a ∈ t
⊢ t = {a}
Tactic:
exact Set.Subsingleton.eq_singleton_of_mem ht' ha
State after:
no goals

State before:
case pos.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s < Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
exact isMaximalStab' s h0' h1' hs'
State after:
no goals

State before:
case pos.inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
exfalso
State after:
case pos.inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ
⊢ False

State before:
case pos.inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ
⊢ False
Tactic:
apply hs
State after:
case pos.inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ
⊢ Fintype.card α = 2 * Set.ncard s

State before:
case pos.inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard s = Set.ncard sᶜ
⊢ Fintype.card α = 2 * Set.ncard s
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s, ← hs', ← two_mul]
State after:
no goals

State before:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
rw [← compl_compl s] at h0'
State after:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
rw [← stabilizer_compl]
State after:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sᶜ)

State before:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sᶜ)
Tactic:
apply isMaximalStab' (sᶜ) h1' h0'
State after:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard sᶜᶜ

State before:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard sᶜᶜ
Tactic:
simp_rw [compl_compl s]
State after:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard s

State before:
case pos.inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial sᶜᶜ
h1' : Set.Nontrivial sᶜ
hs' : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard s
Tactic:
convert hs'
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : ¬Set.Nontrivial sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
simp only [Set.not_nontrivial_iff] at h1'
State after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Subsingleton sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Subsingleton sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
rw [← stabilizer_compl]
State after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Subsingleton sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sᶜ)

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Nontrivial s
h1' : Set.Subsingleton sᶜ
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sᶜ)
Tactic:
exact h (sᶜ) h1 h1'
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : ¬Set.Nontrivial s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
simp only [Set.not_nontrivial_iff] at h0'
State after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Subsingleton s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hs : Fintype.card α ≠ 2 * Set.ncard s
hα : 3 ≤ Fintype.card α
this : Nontrivial α
h : ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
h0' : Set.Subsingleton s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) s)
Tactic:
exact h s h0 h0'
State after:
no goals