internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.Equiv.Perm.Stabilizer.is_preprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
let f : s →ₑ[φ] s :=
  { toFun := id
    map_smul' := fun ⟨m, hm⟩ x => by
      simp only [id_eq, ← Subtype.coe_inj, SMul.smul_stabilizer_def,
        Perm.smul_def, Submonoid.mk_smul] }
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: Equiv.Perm.Equiv.Perm.Stabilizer.is_preprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
have : Function.Surjective f := Function.surjective_id
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
this : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: Equiv.Perm.Equiv.Perm.Stabilizer.is_preprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
this : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
apply isPreprimitive_of_surjective_map this
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
this : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s
Theorem: Equiv.Perm.Equiv.Perm.Stabilizer.is_preprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
this : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s
Tactic:
apply stabilizer_isPreprimitive
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.Stabilizer.is_preprimitive'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
φ : ↥(stabilizer (Perm α) s) → ↥(stabilizer (↥G) s) := fun g => { val := { val := ↑g, property := ⋯ }, property := ⋯ }
x✝ : ↥(stabilizer (Perm α) s)
x : ↑s
m : Perm α
hm : m ∈ stabilizer (Perm α) s
⊢ id ({ val := m, property := hm } • x) = φ { val := m, property := hm } • id x
Tactic:
simp only [id_eq, ← Subtype.coe_inj, SMul.smul_stabilizer_def,
  Perm.smul_def, Submonoid.mk_smul]
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Tactic:
let φ : stabilizer (alternatingGroup α) s → Equiv.Perm s := MulAction.toPerm
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑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
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Tactic:
suffices hφ : Function.Surjective φ by
  let f : s →ₑ[φ] s := {
    toFun := id
    map_smul' := fun ⟨g, hg⟩ ⟨x, hx⟩ => by
      simp only [id.def, Equiv.Perm.smul_def]
      rw [toPerm_apply] }
  have hf : Function.Bijective f := Function.bijective_id
  rw [isPreprimitive_of_bijective_map_iff hφ hf]
  exact Equiv.Perm.isPreprimitive s
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
⊢ Function.Surjective φ
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.sign k = -1
Tactic:
obtain ⟨a, ha, b, hb, hab⟩ := hs
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ ∃ k, Equiv.Perm.sign k = -1
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ ∃ k, Equiv.Perm.sign k = -1
Tactic:
use Equiv.swap ⟨a, ha⟩ ⟨b, hb⟩
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ Equiv.Perm.sign (Equiv.swap { val := a, property := ha } { val := b, property := hb }) = -1
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ Equiv.Perm.sign (Equiv.swap { val := a, property := ha } { val := b, property := hb }) = -1
Tactic:
rw [Equiv.Perm.sign_swap _]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ { val := a, property := ha } ≠ { val := b, property := hb }
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ { val := a, property := ha } ≠ { val := b, property := hb }
Tactic:
rw [← Function.Injective.ne_iff Subtype.coe_injective]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ ↑{ val := a, property := ha } ≠ ↑{ val := b, property := hb }
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ ↑{ val := a, property := ha } ≠ ↑{ val := b, property := hb }
Tactic:
simp only [Subtype.coe_mk]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ a ≠ b
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ a ≠ b
Tactic:
exact hab
Proof state after:
no goals
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
hφ : Function.Surjective φ
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Tactic:
let f : s →ₑ[φ] s := {
  toFun := id
  map_smul' := fun ⟨g, hg⟩ ⟨x, hx⟩ => by
    simp only [id.def, Equiv.Perm.smul_def]
    rw [toPerm_apply] }
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
hφ : Function.Surjective φ
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑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
hφ : Function.Surjective φ
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Tactic:
have hf : Function.Bijective f := Function.bijective_id
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
hφ : Function.Surjective φ
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑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
hφ : Function.Surjective φ
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Tactic:
rw [isPreprimitive_of_bijective_map_iff hφ hf]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
hφ : Function.Surjective φ
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive (Equiv.Perm ↑s) ↑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
hφ : Function.Surjective φ
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive (Equiv.Perm ↑s) ↑s
Tactic:
exact Equiv.Perm.isPreprimitive s
Proof state after:
no goals
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
hφ : Function.Surjective φ
x✝¹ : ↥(stabilizer (↥(alternatingGroup α)) s)
x✝ : ↑s
g : ↥(alternatingGroup α)
hg : g ∈ stabilizer (↥(alternatingGroup α)) s
x : α
hx : x ∈ s
⊢ id ({ val := g, property := hg } • { val := x, property := hx }) =
    φ { val := g, property := hg } • id { val := x, property := hx }
Tactic:
simp only [id.def, Equiv.Perm.smul_def]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
hφ : Function.Surjective φ
x✝¹ : ↥(stabilizer (↥(alternatingGroup α)) s)
x✝ : ↑s
g : ↥(alternatingGroup α)
hg : g ∈ stabilizer (↥(alternatingGroup α)) s
x : α
hx : x ∈ s
⊢ { val := g, property := hg } • { val := x, property := hx } =
    (φ { val := g, property := hg }) { val := x, property := hx }
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
hφ : Function.Surjective φ
x✝¹ : ↥(stabilizer (↥(alternatingGroup α)) s)
x✝ : ↑s
g : ↥(alternatingGroup α)
hg : g ∈ stabilizer (↥(alternatingGroup α)) s
x : α
hx : x ∈ s
⊢ { val := g, property := hg } • { val := x, property := hx } =
    (φ { val := g, property := hg }) { val := x, property := hx }
Tactic:
rw [toPerm_apply]
Proof state after:
no goals
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
this : ∃ k, Equiv.Perm.sign k = -1
⊢ Function.Surjective φ
Tactic:
obtain ⟨k, hk_sign⟩ := this
Proof state after:
case intro
α : 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
⊢ Function.Surjective φ
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case intro
α : 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
⊢ Function.Surjective φ
Tactic:
have hks : Equiv.Perm.ofSubtype k • s = s := by
  rw [← mem_stabilizer_iff]
  exact Equiv.Perm.ofSubtype_mem_stabilizer' s k
Proof state after:
case intro
α : 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
⊢ Function.Surjective φ
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case intro
α : 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
⊢ Function.Surjective φ
Tactic:
have hminus_one_ne_one : (-1 : Units ℤ) ≠ 1 := Ne.symm (units_ne_neg_self 1)
Proof state after:
case intro
α : 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
⊢ Function.Surjective φ
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case intro
α : 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
⊢ Function.Surjective φ
Tactic:
intro g
Proof state after:
case intro
α : 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
⊢ ∃ a, φ a = g
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case intro
α : 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
⊢ ∃ a, φ a = g
Tactic:
let g' := if Equiv.Perm.sign g = 1 then Equiv.Perm.ofSubtype g else Equiv.Perm.ofSubtype g * Equiv.Perm.ofSubtype k
Proof state after:
case intro
α : 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
⊢ ∃ a, φ a = g
Theorem: alternatingGroup.stabilizer.isPreprimitive
Proof state before:
case intro
α : 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
⊢ ∃ a, φ a = g
Tactic:
use! g'
Proof state after:
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' ∈ alternatingGroup α

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
⊢ { val := g', property := ?property } ∈ stabilizer (↥(alternatingGroup α)) 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 }, property := ?property } = g
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' ∈ alternatingGroup α

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
⊢ { val := g', property := ?property } ∈ stabilizer (↥(alternatingGroup α)) 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 }, property := ?property } = g
Tactic:
rw [Equiv.Perm.mem_alternatingGroup]
Proof state after:
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
⊢ Equiv.Perm.sign g' = 1

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
⊢ { val := g', property := ⋯ } ∈ stabilizer (↥(alternatingGroup α)) 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 := ?property } = g
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
⊢ { val := g', property := ⋯ } ∈ stabilizer (↥(alternatingGroup α)) 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 := ?property } = g
Tactic:
rw [mem_stabilizer_iff, Submonoid.mk_smul]
Proof state after:
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