internlm/Lean-Github huggingface dataset:
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Surjective ⇑(map M hst)
Tactic:
rintro ⟨x, hxt⟩
Proof state after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (map M hst) a = { val := x, property := hxt }
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (map M hst) a = { val := x, property := hxt }
Tactic:
use ⟨x, ?_⟩
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ (map M hst) { val := x, property := ?w } = { val := x, property := hxt }

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M s
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ (map M hst) { val := x, property := ?w } = { val := x, property := hxt }

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M s
Tactic:
rfl
Proof state after:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M s
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M s
Tactic:
rw [hst]
Proof state after:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M t
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M t
Tactic:
exact hxt
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Bijective (MulActionHom.toMap (map M hst))
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Injective (MulActionHom.toMap (map M hst))

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Surjective (MulActionHom.toMap (map M hst))
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Injective (MulActionHom.toMap (map M hst))
Tactic:
rintro ⟨g, hg⟩ ⟨k, hk⟩ hgk
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  MulActionHom.toMap (map M hst) { val := g, property := hg } =
    MulActionHom.toMap (map M hst) { val := k, property := hk }
⊢ { val := g, property := hg } = { val := k, property := hk }
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  MulActionHom.toMap (map M hst) { val := g, property := hg } =
    MulActionHom.toMap (map M hst) { val := k, property := hk }
⊢ { val := g, property := hg } = { val := k, property := hk }
Tactic:
rw [← SetLike.coe_eq_coe] at hgk ⊢
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ ↑{ val := g, property := hg } = ↑{ val := k, property := hk }
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ ↑{ val := g, property := hg } = ↑{ val := k, property := hk }
Tactic:
simp only
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ g = k
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ g = k
Tactic:
exact hgk
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Surjective (MulActionHom.toMap (map M hst))
Tactic:
rintro ⟨k, hk⟩
Proof state after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ ∃ a, MulActionHom.toMap (map M hst) a = { val := k, property := hk }
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ ∃ a, MulActionHom.toMap (map M hst) a = { val := k, property := hk }
Tactic:
use ⟨k, ?_⟩
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ MulActionHom.toMap (map M hst) { val := k, property := ?w } = { val := k, property := hk }

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ MulActionHom.toMap (map M hst) { val := k, property := ?w } = { val := k, property := hk }

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s
Tactic:
rfl
Proof state after:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s
Tactic:
rw [hst]
Proof state after:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M t
Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective
Proof state before:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M t
Tactic:
exact hk
Proof state after:
no goals
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ ofSubtype g ∈ stabilizer (Perm α) s
Tactic:
rw [mem_stabilizer_of_finite_iff_smul_le]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ ofSubtype g • s ⊆ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ ofSubtype g • s ⊆ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
x : α
⊢ x ∈ ofSubtype g • s → x ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
x : α
⊢ x ∈ ofSubtype g • s → x ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
rw [Set.mem_smul_set]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
x : α
⊢ (∃ y ∈ s, ofSubtype g • y = x) → x ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
x : α
⊢ (∃ y ∈ s, ofSubtype g • y = x) → x ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
rintro ⟨y, hy, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ ofSubtype g • y ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ ofSubtype g • y ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
simp only [Equiv.Perm.smul_def]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ (ofSubtype g) y ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ (ofSubtype g) y ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem g hy]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ ↑(g { val := y, property := hy }) ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ ↑(g { val := y, property := hy }) ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
refine' Subtype.mem _
Proof state after:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer
Proof state before:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
exact s.toFinite
Proof state after:
no goals
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ ofSubtype g ∈ stabilizer (Perm α) s
Tactic:
rw [mem_stabilizer_of_finite_iff_smul_le]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ ofSubtype g • s ⊆ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ Set.Finite s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ Set.Finite s
Tactic:
exact s.toFinite
Proof state after:
no goals
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ ofSubtype g • s ⊆ s
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ x ∈ ofSubtype g • s → x ∈ s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ x ∈ ofSubtype g • s → x ∈ s
Tactic:
rw [Set.mem_smul_set]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ (∃ y ∈ s, ofSubtype g • y = x) → x ∈ s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ (∃ y ∈ s, ofSubtype g • y = x) → x ∈ s
Tactic:
rintro ⟨y, hy, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ ofSubtype g • y ∈ s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ ofSubtype g • y ∈ s
Tactic:
simp only [Equiv.Perm.smul_def]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ (ofSubtype g) y ∈ s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ (ofSubtype g) y ∈ s
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem g (Set.not_mem_compl_iff.mpr hy)]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ y ∈ s
Theorem: Equiv.Perm.ofSubtype_mem_stabilizer'
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ y ∈ s
Tactic:
exact hy
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
φ : ↥(stabilizer (Perm α) s) → Perm ↑s := toPerm
⊢ IsPreprimitive ↥(stabilizer (Perm α) s) ↑s
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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, φ] }
Proof 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
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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]
Proof 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 φ
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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
Proof 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 φ
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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, φ]
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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⟩
Proof 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 })
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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 = _
Proof 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 })
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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]
Proof 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 })
Theorem: Equiv.Perm.stabilizer_isPreprimitive
Proof 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]
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
⊢ 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⟩
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 := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s