internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case property.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ ofSubtype g ∈ stabilizer (Perm α) s
Tactic:
rw [← stabilizer_compl]
Proof state after:
case property.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ ofSubtype g ∈ stabilizer (Perm α) sᶜ
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case property.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ ofSubtype g ∈ stabilizer (Perm α) sᶜ
Tactic:
convert ofSubtype_mem_stabilizer _ g
Proof state after:
no goals
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case property
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ { val := ofSubtype g, property := ⋯ } ∈ stabilizer (↥G) sᶜ
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
case property
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ { val := ofSubtype g, property := ⋯ } • sᶜ = sᶜ
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case property
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ { val := ofSubtype g, property := ⋯ } • sᶜ = sᶜ
Tactic:
change Equiv.Perm.ofSubtype g • sᶜ = sᶜ
Proof state after:
case property
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ ofSubtype g • sᶜ = sᶜ
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case property
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ ofSubtype g • sᶜ = sᶜ
Tactic:
rw [← mem_stabilizer_iff]
Proof state after:
case property
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ ofSubtype g ∈ stabilizer (Perm α) sᶜ
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case property
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ ofSubtype g ∈ stabilizer (Perm α) sᶜ
Tactic:
convert ofSubtype_mem_stabilizer _ g
Proof state after:
no goals
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
⊢ φ { val := { val := ofSubtype g, property := ⋯ }, property := ⋯ } = g
Tactic:
ext ⟨x, hx⟩
Proof state after:
case h.H.mk.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
x : α
hx : x ∈ sᶜ
⊢ ↑((φ { val := { val := ofSubtype g, property := ⋯ }, property := ⋯ }) { val := x, property := hx }) =
    ↑(g { val := x, property := hx })
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case h.H.mk.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) sᶜ) → Perm ↑sᶜ := toPerm
f : ↑sᶜ →ₑ[φ] ↑sᶜ := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑sᶜ
x : α
hx : x ∈ sᶜ
⊢ ↑((φ { val := { val := ofSubtype g, property := ⋯ }, 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✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) 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.isMaximalStab'
Proof state before:
case h.H.mk.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) 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✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) 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.isMaximalStab'
Proof state before:
case h.H.mk.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
φ : ↥(stabilizer (↥G) 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.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
⊢ ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
Tactic:
intro B hB hBs
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ Set.Subsingleton B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)
Tactic:
suffices IsPreprimitive (stabilizer G s) s by
  apply IsPreprimitive.has_trivial_blocks this
  let φ' : stabilizer G s → G := Subtype.val
  let f' : s →ₑ[φ'] α := {
    toFun := Subtype.val
    map_smul' := fun ⟨m, _⟩ x => by
      simp only [SMul.smul_stabilizer_def] }
  apply MulAction.IsBlock_preimage f' hB
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
let φ : stabilizer G s → Equiv.Perm s := MulAction.toPerm
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
let f : s →ₑ[φ] s := {
    toFun := id
    map_smul' := fun g x => by
      simp only [φ, id.def, Equiv.Perm.smul_def, toPerm_apply] }
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
have hf : Function.Bijective f := Function.bijective_id
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Tactic:
rw [isPreprimitive_of_bijective_map_iff _ hf]
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive (Perm ↑s) ↑s

α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective φ
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive (Perm ↑s) ↑s

α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective φ
Tactic:
apply Equiv.Perm.isPreprimitive
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ Function.Surjective φ
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g : Perm α
hg_swap : IsSwap g
hg : g ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) 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✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Set.ncard s < Set.ncard sᶜ
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
g✝ : Perm α
hg_swap : IsSwap g✝
hg : g✝ ∈ G
this : IsPretransitive (↥G) α
hB_ne_sc : ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hBs : B ⊆ s
φ : ↥(stabilizer (↥G) s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
g : Perm ↑s
⊢ ∃ a, φ a = g