internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case out.right
α : 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ᶜ
⊢ ∀ (b : Subgroup (Perm α)), stabilizer (Perm α) s < b → b = ⊤
Tactic:
intro G hG
Proof state after:
case out.right
α : 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 = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case out.right
α : 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 = ⊤
Tactic:
obtain ⟨g, hg_swap, hg⟩ := has_swap_of_lt_stabilizer s G hG
Proof state after:
case out.right.intro.intro
α : 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
⊢ G = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case out.right.intro.intro
α : 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
⊢ G = ⊤
Tactic:
apply jordan_swap _ g hg_swap 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
⊢ IsPreprimitive (↥G) α
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) α
⊢ IsPreprimitive (↥G) α
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
α : 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 → IsTrivialBlock B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'
α : 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 → IsTrivialBlock B
Tactic:
have hB_ne_sc : ∀ (B : Set α) (_ : IsBlock G B), ¬B = sᶜ := by
  intro B hB hBsc
  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:
case has_trivial_blocks'
α : 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 α}, IsBlock (↥G) B → IsTrivialBlock B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
⊢ ∀ {B : Set α}, IsBlock (↥G) B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
⊢ IsTrivialBlock B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
⊢ IsTrivialBlock B
Tactic:
unfold IsTrivialBlock
Proof state after:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
⊢ Set.Subsingleton B ∨ B = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
⊢ Set.Subsingleton B ∨ B = ⊤
Tactic:
rw [or_iff_not_imp_left]
Proof state after:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
⊢ ¬Set.Subsingleton B → B = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
⊢ ¬Set.Subsingleton B → B = ⊤
Tactic:
intro hB'
Proof state after:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
⊢ B = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'
α : 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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → Set.Subsingleton B
B : Set α
hB : IsBlock (↥G) B
hB' : ¬Set.Subsingleton B
⊢ B = ⊤
Tactic:
obtain ⟨a, ha, ha'⟩ :=
  Set.not_subset_iff_exists_mem_not_mem.mp fun h => hB' ((hB_not_le_sc B hB) h)
Proof state after:
case has_trivial_blocks'.intro.intro
α : 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
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 = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro
α : 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
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 = ⊤
Tactic:
rw [Set.not_mem_compl_iff] at ha'
Proof state after:
case has_trivial_blocks'.intro.intro
α : 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
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 = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro
α : 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
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 = ⊤
Tactic:
obtain ⟨b, hb, hb'⟩ :=
  Set.not_subset_iff_exists_mem_not_mem.mp fun h => hB' ((hB_not_le_s B hB) h)
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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
⊢ B = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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
⊢ B = ⊤
Tactic:
rw [← Set.mem_compl_iff] at hb'
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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ᶜ
⊢ B = ⊤
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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
⊢ B = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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
⊢ ⊤ ≤ B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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
⊢ ⊤ ≤ B
Tactic:
intro x _
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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 ∈ ⊤
⊢ x ∈ B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro
α : 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
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 ∈ ⊤
⊢ x ∈ B
Tactic:
obtain ⟨b, hb⟩ := h1
Proof state after:
case has_trivial_blocks'.intro.intro.intro.intro.intro
α : 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ᶜ
⊢ x ∈ B
Theorem: Equiv.Perm.isMaximalStab'
Proof state before:
case has_trivial_blocks'.intro.intro.intro.intro.intro
α : 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ᶜ
⊢ x ∈ B
Tactic:
obtain ⟨⟨g, hg⟩, hgbx : g • b = x⟩ := exists_smul_eq G b x
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
⊢ x ∈ 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
⊢ x ∈ B
Tactic:
suffices g • B = B by
  rw [← hgbx, ← this, Set.smul_mem_smul_set_iff]
  exact hsc_le_B hb
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
⊢ g • B = B