internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ g • B = B
Tactic:
apply or_iff_not_imp_right.mp (IsBlock.def_one.mp hB ⟨g, hg⟩)
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ ¬_root_.Disjoint ({ val := g, property := hg } • B) B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ ¬_root_.Disjoint ({ val := g, property := hg } • B) B
Tactic:
rw [Set.not_disjoint_iff_nonempty_inter]
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.Nonempty ({ val := g, property := hg } • B ∩ B)
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.Nonempty ({ val := g, property := hg } • B ∩ B)
Tactic:
change (g • B ∩ B).Nonempty
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.Nonempty (g • B ∩ B)
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.Nonempty (g • B ∩ B)
Tactic:
apply Set.ncard_pigeonhole
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Fintype.card α < Set.ncard (g • B) + Set.ncard B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Fintype.card α < Set.ncard (g • B) + Set.ncard B
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s]
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.45087
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
h0 : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
a : α
ha : a ∈ B
ha' : a ∈ s
b✝ : α
hb✝ : b✝ ∈ B
hb' : b✝ ∈ sᶜ
hsc_le_B : sᶜ ⊆ B
x : α
a✝ : x ∈ ⊤
b : α
hb : b ∈ sᶜ
g : Perm α
hg : g ∈ G
hgbx : g • b = x
⊢ Set.ncard s + Set.ncard sᶜ < Set.ncard (g • B) + Set.ncard 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
⊢ IsPretransitive (↥G) α
Tactic:
apply IsPretransitive.of_partition G s
Proof state after:
case 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
⊢ ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b

case 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
⊢ ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b

case 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
⊢ stabilizer (↥G) s ≠ ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case 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
⊢ ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
Tactic:
apply moves_in
Proof state after:
case a.hGt
α : 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
⊢ stabilizer (Perm α) s < G
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case a.hGt
α : 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
⊢ stabilizer (Perm α) s < G
Tactic:
exact hG
Proof state after:
no goals
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case 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
⊢ ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
Tactic:
apply moves_in
Proof state after:
case a.hGt
α : 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
⊢ stabilizer (Perm α) sᶜ < G
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case a.hGt
α : 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
⊢ stabilizer (Perm α) sᶜ < G
Tactic:
rw [stabilizer_compl]
Proof state after:
case a.hGt
α : 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
⊢ stabilizer (Perm α) s < G
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case 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
⊢ stabilizer (↥G) s ≠ ⊤
Tactic:
intro h
Proof state after:
case 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
h : stabilizer (↥G) s = ⊤
⊢ False
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case 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
h : stabilizer (↥G) s = ⊤
⊢ False
Tactic:
apply lt_irrefl G
Proof state after:
case 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
h : stabilizer (↥G) s = ⊤
⊢ G < G
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case 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
h : stabilizer (↥G) s = ⊤
⊢ G < G
Tactic:
apply lt_of_le_of_lt _ hG
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
h : stabilizer (↥G) s = ⊤
⊢ G ≤ stabilizer (Perm α) 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
h : stabilizer (↥G) s = ⊤
⊢ G ≤ stabilizer (Perm α) s
Tactic:
intro g hg
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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ g ∈ stabilizer (Perm α) 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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ g ∈ stabilizer (Perm α) s
Tactic:
rw [mem_stabilizer_iff]
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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ 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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ g • s = s
Tactic:
rw [← Subgroup.coe_mk G g hg]
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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ ↑{ val := g, property := hg } • 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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ ↑{ val := g, property := hg } • s = s
Tactic:
change (⟨g, hg⟩ : ↥G) • s = s
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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ { val := g, property := hg } • 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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ { val := g, property := hg } • s = s
Tactic:
rw [← mem_stabilizer_iff]
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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ { val := g, property := hg } ∈ stabilizer (↥G) 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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ { val := g, property := hg } ∈ stabilizer (↥G) s
Tactic:
rw [h]
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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ { val := g, property := hg } ∈ ⊤
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
h : stabilizer (↥G) s = ⊤
g : Perm α
hg : g ∈ G
⊢ { val := g, property := hg } ∈ ⊤
Tactic:
trivial
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) α
⊢ ∀ (B : Set α), IsBlock (↥G) B → ¬B = sᶜ
Tactic:
intro B hB hBsc
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) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
⊢ False
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) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
⊢ False
Tactic:
cases MulAction.isTrivialBlock_or_2_mul_ncard_le_card hB with
| inl hB_triv =>
  cases hB_triv with
  | inl hB_subsingleton =>
    have : Set.ncard B ≤ 1 := by
      rw [Set.ncard_le_one_iff_eq]
      apply Set.Subsingleton.eq_empty_or_singleton
      exact hB_subsingleton
    apply not_lt.mpr this
    rw [hBsc]
    apply lt_of_le_of_lt _ hα
    rw [Nat.succ_le_iff, Set.ncard_pos]
    exact h0
  | inr hB_top =>
    apply Set.not_nonempty_empty
    simp only [hBsc, Set.top_eq_univ, Set.compl_univ_iff] at hB_top
    rw [← hB_top]
    exact h0
| inr hcard =>
  apply not_lt.mpr hcard
  rw [← Set.ncard_add_ncard_compl B, two_mul, add_lt_add_iff_left,
    hBsc, compl_compl]
  exact hα
Proof state after:
no goals
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case inl
α : 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) α
B : Set α
hB : IsBlock (↥G) B
hBsc : B = sᶜ
hB_triv : IsTrivialBlock B
⊢ False
Tactic:
cases hB_triv with
| inl hB_subsingleton =>
  have : Set.ncard B ≤ 1 := by
    rw [Set.ncard_le_one_iff_eq]
    apply Set.Subsingleton.eq_empty_or_singleton
    exact hB_subsingleton
  apply not_lt.mpr this
  rw [hBsc]
  apply lt_of_le_of_lt _ hα
  rw [Nat.succ_le_iff, Set.ncard_pos]
  exact h0
| inr hB_top =>
  apply Set.not_nonempty_empty
  simp only [hBsc, Set.top_eq_univ, Set.compl_univ_iff] at hB_top
  rw [← hB_top]
  exact h0
Proof state after:
no goals