internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
⊢ g' • s = s

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
⊢ φ { val := { val := g', property := ⋯ }, property := ⋯ } = g
Tactic:
cases' Int.units_eq_one_or (Equiv.Perm.sign g) with hsg hsg
Proof state after:
case property.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ g' • s = s

case property.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ g' • s = s

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
⊢ φ { val := { val := g', property := ⋯ }, property := ⋯ } = g
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
⊢ φ { val := { val := g', property := ⋯ }, property := ⋯ } = g
Tactic:
dsimp only [id_eq, ite_true, ite_false, eq_mpr_eq_cast, cast_eq, φ]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
⊢ toPerm { val := { val := g', property := ⋯ }, property := ⋯ } = g
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
⊢ toPerm { val := { val := g', property := ⋯ }, property := ⋯ } = g
Tactic:
cases' Int.units_eq_one_or (Equiv.Perm.sign g) with hsg hsg
Proof state after:
case h.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ toPerm { val := { val := g', property := ⋯ }, property := ⋯ } = g

case h.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ toPerm { val := { val := g', property := ⋯ }, property := ⋯ } = g
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
⊢ Equiv.Perm.ofSubtype k • s = s
Tactic:
rw [← mem_stabilizer_iff]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
⊢ Equiv.Perm.ofSubtype k ∈ stabilizer (Equiv.Perm α) s
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
⊢ Equiv.Perm.ofSubtype k ∈ stabilizer (Equiv.Perm α) s
Tactic:
exact Equiv.Perm.ofSubtype_mem_stabilizer' s k
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case property.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ Equiv.Perm.sign g' = 1
Tactic:
simp only [g', hsg, eq_self_iff_true, if_true, hminus_one_ne_one, if_false, Equiv.Perm.sign_ofSubtype, Equiv.Perm.sign_mul, mul_neg, mul_one, neg_neg, hsg, hk_sign]
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case property.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ g' • s = s
Tactic:
simp only [g', hsg, eq_self_iff_true, if_true]
Proof state after:
case property.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ Equiv.Perm.ofSubtype g • s = s
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case property.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ Equiv.Perm.ofSubtype g • s = s
Tactic:
exact Equiv.Perm.ofSubtype_mem_stabilizer s g
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case property.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ g' • s = s
Tactic:
simp only [g', hsg, hminus_one_ne_one, if_false, mul_smul, hks]
Proof state after:
case property.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ Equiv.Perm.ofSubtype g • s = s
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case property.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ Equiv.Perm.ofSubtype g • s = s
Tactic:
exact Equiv.Perm.ofSubtype_mem_stabilizer s g
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ toPerm { val := { val := g', property := ⋯ }, property := ⋯ } = g
Tactic:
simp only [g', hsg, eq_self_iff_true, if_true, hminus_one_ne_one, if_false]
Proof state after:
case h.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ toPerm { val := { val := Equiv.Perm.ofSubtype g, property := ⋯ }, property := ⋯ } = g
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
⊢ toPerm { val := { val := Equiv.Perm.ofSubtype g, property := ⋯ }, property := ⋯ } = g
Tactic:
ext x
Proof state after:
case h.inl.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
x : ↑s
⊢ ↑((toPerm { val := { val := Equiv.Perm.ofSubtype g, property := ⋯ }, property := ⋯ }) x) = ↑(g x)
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inl.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = 1
x : ↑s
⊢ ↑((toPerm { val := { val := Equiv.Perm.ofSubtype g, property := ⋯ }, property := ⋯ }) x) = ↑(g x)
Tactic:
simp only [toPerm_apply, SMul.smul_stabilizer_def, Submonoid.mk_smul, Equiv.Perm.smul_def,
  Equiv.Perm.ofSubtype_apply_coe]
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ toPerm { val := { val := g', property := ⋯ }, property := ⋯ } = g
Tactic:
simp only [g', hsg, eq_self_iff_true, if_true, hminus_one_ne_one, if_false]
Proof state after:
case h.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ toPerm { val := { val := Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k, property := ⋯ }, property := ⋯ } = g
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
⊢ toPerm { val := { val := Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k, property := ⋯ }, property := ⋯ } = g
Tactic:
ext x
Proof state after:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑((toPerm { val := { val := Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k, property := ⋯ }, property := ⋯ }) x) =
    ↑(g x)
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑((toPerm { val := { val := Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k, property := ⋯ }, property := ⋯ }) x) =
    ↑(g x)
Tactic:
simp only [toPerm_apply, SMul.smul_stabilizer_def, Submonoid.mk_smul]
Proof state after:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ (Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k) • ↑x = ↑(g x)
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ (Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k) • ↑x = ↑(g x)
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ (Equiv.Perm.ofSubtype g) ((Equiv.Perm.ofSubtype k) ↑x) = ↑(g x)
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ (Equiv.Perm.ofSubtype g) ((Equiv.Perm.ofSubtype k) ↑x) = ↑(g x)
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem k _]
Proof state after:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ (Equiv.Perm.ofSubtype g) ↑x = ↑(g x)

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑x ∉ sᶜ
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h.inr.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ (Equiv.Perm.ofSubtype g) ↑x = ↑(g x)

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑x ∉ sᶜ
Tactic:
exact Equiv.Perm.ofSubtype_apply_coe g x
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑x ∉ sᶜ
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑x ∉ sᶜ
Tactic:
rw [Set.not_mem_compl_iff]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑x ∈ s
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
k : Equiv.Perm ↑sᶜ
hk_sign : Equiv.Perm.sign k = -1
hks : Equiv.Perm.ofSubtype k • s = s
hminus_one_ne_one : -1 ≠ 1
g : Equiv.Perm ↑s
g' : Equiv.Perm α :=
  if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
hsg : Equiv.Perm.sign g = -1
x : ↑s
⊢ ↑x ∈ s
Tactic:
exact x.prop
Proof state after:
no goals