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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) 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'⟩, hm⟩ ⟨a, ha⟩ => rfl }
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) 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 α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) 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 hf : Function.Surjective f := Function.surjective_id
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
apply isPreprimitive_of_surjective_map hf
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥(alternatingGroup α)) s) ↑s
Tactic:
apply stabilizer.isPreprimitive
State after:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ Set.Nontrivial sᶜ

State before:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
φ : ↥(stabilizer (↥(alternatingGroup α)) s) → ↥(stabilizer (↥G) s) :=
  fun g => { val := { val := ↑↑g, property := ⋯ }, property := ⋯ }
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Surjective ⇑f
⊢ Set.Nontrivial sᶜ
Tactic:
exact hsc
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↥(stabilizer (↥G) s)
Tactic:
use! (g : alternatingGroup α)
State after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ G

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ?property } ∈ stabilizer (↥G) s

State before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ G

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ?property } ∈ stabilizer (↥G) s
Tactic:
apply hG
State after:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s

State before:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Tactic:
rw [Subgroup.mem_inf]
State after:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ∧ ↑↑g ∈ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s

State before:
case property.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s ∧ ↑↑g ∈ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Tactic:
constructor
State after:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s

case property.a.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ alternatingGroup α

case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s

State before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ { val := ↑↑g, property := ⋯ } ∈ stabilizer (↥G) s
Tactic:
exact g.prop
State after:
no goals

State before:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s
Tactic:
let h := g.prop
State after:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g ∈ stabilizer (↥(alternatingGroup α)) s := Subtype.prop g
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s

State before:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g ∈ stabilizer (↥(alternatingGroup α)) s := Subtype.prop g
⊢ ↑↑g ∈ stabilizer (Equiv.Perm α) s
Tactic:
rw [mem_stabilizer_iff] at h ⊢
State after:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g • s = s
⊢ ↑↑g • s = s

State before:
case property.a.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
h : ↑g • s = s
⊢ ↑↑g • s = s
Tactic:
exact h
State after:
no goals

State before:
case property.a.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
g : ↥(stabilizer (↥(alternatingGroup α)) s)
⊢ ↑↑g ∈ alternatingGroup α
Tactic:
exact SetLike.coe_mem _
State after:
no goals