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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ { val := x, property := ?m.82434 } ∈ Subtype.val ⁻¹' B

α : 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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ α → Prop

α : 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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ ?m.82433 x

α : 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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ α → Prop

α : 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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ ?m.82433 x
Tactic:
rw [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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ { val := x, property := ?m.82434 } ∈ ⊤

α : 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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ x ∈ 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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ x ∈ 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
hB' : Subtype.val ⁻¹' B = ⊤
x : α
hx : x ∈ s
⊢ x ∈ s