internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.isMaximalStab'
Proof 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
Proof 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 α
Theorem: alternatingGroup.isMaximalStab'
Proof 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]
Proof 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 α
Theorem: alternatingGroup.isMaximalStab'
Proof 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
Proof 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'
Theorem: alternatingGroup.isMaximalStab'
Proof 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]
Proof 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'
Theorem: alternatingGroup.isMaximalStab'
Proof 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'
Proof state after:
no goals
Theorem: alternatingGroup.isMaximalStab'
Proof 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]
Proof 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
Theorem: alternatingGroup.isMaximalStab'
Proof 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'
Proof state after:
no goals
Theorem: alternatingGroup.three_le
Proof state before:
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
⊢ 3 ≤ c
Tactic:
cases' Nat.eq_or_lt_of_le h with h h
Proof state after:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 = n
⊢ 3 ≤ c

case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 3 ≤ c
Theorem: alternatingGroup.three_le
Proof state before:
case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 3 ≤ c
Tactic:
rw [Nat.succ_le_iff]
Proof state after:
case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 2 < c
Theorem: alternatingGroup.three_le
Proof state before:
case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 2 < c
Tactic:
exact lt_of_le_of_lt h h'
Proof state after:
no goals
Theorem: alternatingGroup.three_le
Proof state before:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 = n
⊢ 3 ≤ c
Tactic:
rw [← h] at h' hh'
Proof state after:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
⊢ 3 ≤ c
Theorem: alternatingGroup.three_le
Proof state before:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
⊢ 3 ≤ c
Tactic:
cases' Nat.eq_or_lt_of_le h' with h' h'
Proof state after:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ 3 ≤ c

case inl.inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 < c
⊢ 3 ≤ c
Theorem: alternatingGroup.three_le
Proof state before:
case inl.inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 < c
⊢ 3 ≤ c
Tactic:
exact h'
Proof state after:
no goals
Theorem: alternatingGroup.three_le
Proof state before:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ 3 ≤ c
Tactic:
exfalso
Proof state after:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ False
Theorem: alternatingGroup.three_le
Proof state before:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ False
Tactic:
apply hh' h'.symm
Proof state after:
no goals
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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ᶜ
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof 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 α
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof 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 α
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof 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ᶜ
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof 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 α
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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α
Proof 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
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof state after:
no goals