Theorem: Equiv.Perm.Equiv.Perm.Stabilizer.is_preprimitive' (Jordan/StabilizerPrimitive.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s ≤ G
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
let φ : stabilizer (Equiv.Perm α) s → stabilizer G s := fun g =>
  ⟨⟨g, hG g.prop⟩, mem_stabilizer_iff.mp g.prop⟩
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 := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s

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

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

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

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

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