Theorem: alternatingGroup.stabilizer.isPreprimitive (Jordan/StabilizerPrimitive.lean)

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
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

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
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nontrivial sᶜ
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → Equiv.Perm ↑s := toPerm
⊢ Function.Surjective φ

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
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

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⟩
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

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 _]
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 }

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]
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 }

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]
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

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
State after:
no goals

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] }
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

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
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

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]
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

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
State after:
no goals

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]
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 }

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]
State after:
no goals

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
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 φ

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
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 φ

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)
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 φ

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
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

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
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

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'
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

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]
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

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]
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

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
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

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, φ]
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

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
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

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]
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

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
State after:
no goals

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]
State after:
no goals

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]
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

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
State after:
no goals

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]
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

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
State after:
no goals

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]
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

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
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)

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]
State after:
no goals

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]
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

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
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)

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]
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)

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]
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)

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 _]
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ᶜ

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
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ᶜ

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]
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

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
State after:
no goals