internlm/Lean-Github huggingface dataset:
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 α
⊢ ∀ (t : Set α), Set.Nonempty t → Set.Subsingleton t → Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
Tactic:
intro t ht ht'
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 α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
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 α
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α
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 α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
⊢ ∃ a, t = {a}
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 α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
this : ∃ a, t = {a}
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) t)
Tactic:
obtain ⟨a, rfl⟩ := this
Proof 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})
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof 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})
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof 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 α)) α
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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α
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 α
this : Nontrivial α
a : α
ht : Set.Nonempty {a}
ht' : Set.Subsingleton {a}
⊢ stabilizer ↥(alternatingGroup α) {a} = stabilizer (↥(alternatingGroup α)) a
Tactic:
ext
Proof 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
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
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 α
this : Nontrivial α
t : Set α
ht : Set.Nonempty t
ht' : Set.Subsingleton t
⊢ ∃ a, t = {a}
Tactic:
obtain ⟨a, ha⟩ := ht
Proof 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}
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof 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}
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof state after:
no goals
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
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ᶜ
⊢ False
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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
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ᶜ
⊢ Fintype.card α = 2 * Set.ncard s
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof state after:
no goals
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof 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ᶜ)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof 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ᶜᶜ
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof 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
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof state after:
no goals
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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]
Proof 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ᶜ)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof state after:
no goals
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof 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)
Theorem: alternatingGroup.Stabilizer.isMaximal
Proof 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'
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
have hα' : 3 ≤ Fintype.card α := three_le h_one_le hn hα
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
have : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial];
  exact lt_of_le_of_lt h_one_le hn
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
cases' Nat.eq_or_lt_of_le h_one_le with h_one h_one_lt
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one : 1 = n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one_lt : 1 < n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
have : Nontrivial (n.Combination α) :=
  Nat.Combination_nontrivial α (lt_trans (Nat.lt_succ_self 0) h_one_lt) hn
Proof state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)