Theorem: Equiv.Perm.stabilizer_isPreprimitive (Jordan/StabilizerPrimitive.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s
Tactic:
let φ : stabilizer (Equiv.Perm α) s → Equiv.Perm s := MulAction.toPerm
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s
Tactic:
let f : s →ₑ[φ] s :=
  { toFun := id
    map_smul' := fun g x => by
      simp only [id_eq, Perm.smul_def, toPerm_apply, φ] }
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s
Tactic:
have hf : Function.Bijective f := Function.bijective_id
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s
Tactic:
rw [isPreprimitive_of_bijective_map_iff _ hf]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive (Perm ↑s) ↑s

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective φ

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive (Perm ↑s) ↑s

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective φ
Tactic:
exact Equiv.Perm.isPreprimitive s
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective φ

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective φ
Tactic:
intro g
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
⊢ ∃ a, φ a = g

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
⊢ ∃ a, φ a = g
Tactic:
use! Equiv.Perm.ofSubtype g
State after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
⊢ ofSubtype g ∈ stabilizer (Perm α) s

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
⊢ φ { val := ofSubtype g, property := ?property } = g

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
g : ↥(stabilizer (Perm α) s)
x : ↑s
⊢ id (g • x) = φ g • id x
Tactic:
simp only [id_eq, Perm.smul_def, toPerm_apply, φ]
State after:
no goals

State before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
⊢ ofSubtype g ∈ stabilizer (Perm α) s
Tactic:
apply ofSubtype_mem_stabilizer
State after:
no goals

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
⊢ φ { val := ofSubtype g, property := ⋯ } = g
Tactic:
ext ⟨x, hx⟩
State after:
case h.H.mk.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
x : α
hx : x ∈ s
⊢ ↑((φ { val := ofSubtype g, property := ⋯ }) { val := x, property := hx }) = ↑(g { val := x, property := hx })

State before:
case h.H.mk.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
x : α
hx : x ∈ s
⊢ ↑((φ { val := ofSubtype g, property := ⋯ }) { val := x, property := hx }) = ↑(g { val := x, property := hx })
Tactic:
change Equiv.Perm.ofSubtype g • x = _
State after:
case h.H.mk.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
x : α
hx : x ∈ s
⊢ ofSubtype g • x = ↑(g { val := x, property := hx })

State before:
case h.H.mk.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
x : α
hx : x ∈ s
⊢ ofSubtype g • x = ↑(g { val := x, property := hx })
Tactic:
simp only [Equiv.Perm.smul_def]
State after:
case h.H.mk.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
x : α
hx : x ∈ s
⊢ (ofSubtype g) x = ↑(g { val := x, property := hx })

State before:
case h.H.mk.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
x : α
hx : x ∈ s
⊢ (ofSubtype g) x = ↑(g { val := x, property := hx })
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem]
State after:
no goals