Theorem: Equiv.Perm.isMaximalStab' (Jordan/PermMaximal.lean)

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 = ⊤
hBs' : B = s
g' : Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : _root_.Disjoint ({ val := g', property := hg' } • B) B
this : Set.Subsingleton (g' • B)
⊢ Function.Injective fun x => g' • x
Tactic:
apply Function.Bijective.injective
State after:
case hf
α : 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 = ⊤
hBs' : B = s
g' : Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : _root_.Disjoint ({ val := g', property := hg' } • B) B
this : Set.Subsingleton (g' • B)
⊢ Function.Bijective fun x => g' • x

State before:
case hf
α : 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 = ⊤
hBs' : B = s
g' : Perm α
hg' : g' ∈ G
hg's : g' • s ≠ s
h : _root_.Disjoint ({ val := g', property := hg' } • B) B
this : Set.Subsingleton (g' • B)
⊢ Function.Bijective fun x => g' • x
Tactic:
apply MulAction.bijective
State after:
no goals

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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)
Tactic:
apply IsPreprimitive.has_trivial_blocks this
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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)

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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)
Tactic:
let φ' : stabilizer G s → G := Subtype.val
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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
φ' : ↥(stabilizer (↥G) s) → ↥G := Subtype.val
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)

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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
φ' : ↥(stabilizer (↥G) s) → ↥G := Subtype.val
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)
Tactic:
let f' : s →ₑ[φ'] α := {
  toFun := Subtype.val
  map_smul' := fun ⟨m, _⟩ x => by
    simp only [SMul.smul_stabilizer_def] }
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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
φ' : ↥(stabilizer (↥G) s) → ↥G := Subtype.val
f' : ↑s →ₑ[φ'] α := { toFun := Subtype.val, map_smul' := ⋯ }
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)

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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
φ' : ↥(stabilizer (↥G) s) → ↥G := Subtype.val
f' : ↑s →ₑ[φ'] α := { toFun := Subtype.val, map_smul' := ⋯ }
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)
Tactic:
apply MulAction.IsBlock_preimage f' hB
State after:
no goals

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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
φ' : ↥(stabilizer (↥G) s) → ↥G := Subtype.val
x✝ : ↥(stabilizer (↥G) s)
x : ↑s
m : ↥G
property✝ : m ∈ stabilizer (↥G) s
⊢ ↑({ val := m, property := property✝ } • x) = φ' { val := m, property := property✝ } • ↑x
Tactic:
simp only [SMul.smul_stabilizer_def]
State after:
no goals

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
g : ↥(stabilizer (↥G) s)
x : ↑s
⊢ id (g • x) = φ g • id x
Tactic:
simp only [φ, id.def, Equiv.Perm.smul_def, toPerm_apply]
State after:
no goals

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ᶜ
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
⊢ ofSubtype g ∈ G
Tactic:
apply le_of_lt hG
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ᶜ
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
⊢ ofSubtype g ∈ stabilizer (Perm α) s

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ᶜ
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
⊢ ofSubtype g ∈ stabilizer (Perm α) s
Tactic:
apply ofSubtype_mem_stabilizer
State after:
no goals

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ᶜ
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
⊢ { val := ofSubtype g, property := ⋯ } ∈ stabilizer (↥G) s
Tactic:
apply ofSubtype_mem_stabilizer
State after:
no goals

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ᶜ
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
⊢ φ { val := { val := ofSubtype g, property := ⋯ }, property := ⋯ } = g
Tactic:
ext ⟨x, hx⟩
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ᶜ
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
x : α
hx : x ∈ s
⊢ ↑((φ { val := { val := ofSubtype g, property := ⋯ }, property := ⋯ }) { val := x, property := hx }) =
    ↑(g { val := x, property := hx })

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ᶜ
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
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 = _
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ᶜ
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
x : α
hx : x ∈ s
⊢ ofSubtype g • x = ↑(g { val := x, property := hx })

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ᶜ
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
x : α
hx : x ∈ s
⊢ ofSubtype g • x = ↑(g { val := x, property := hx })
Tactic:
simp only [Equiv.Perm.smul_def]
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ᶜ
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
x : α
hx : x ∈ s
⊢ (ofSubtype g) x = ↑(g { val := x, property := hx })

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ᶜ
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
x : α
hx : x ∈ s
⊢ (ofSubtype g) x = ↑(g { val := x, property := hx })
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem]
State after:
no goals

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
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ᶜ
⊢ sᶜ ⊆ B
Tactic:
intro x hx'
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
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ x ∈ B

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
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ᶜ
x : α
hx' : x ∈ sᶜ
this : ∃ k, k • b = x
⊢ x ∈ B
Tactic:
obtain ⟨⟨k, hk⟩, hkbx : k • b = x⟩ := this
State after:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ x ∈ B

State before:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ x ∈ B
Tactic:
suffices k • B = B by
  rw [← hkbx, ← this, Set.smul_mem_smul_set_iff]
  exact hb
State after:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k • B = B

State before:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k • B = B
Tactic:
apply or_iff_not_imp_right.mp (IsBlock.def_one.mp hB ⟨k, _⟩)
State after:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ ¬_root_.Disjoint ({ val := k, property := ?m.108597 } • B) 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
this : k • B = B
⊢ x ∈ B
Tactic:
rw [← hkbx, ← this, Set.smul_mem_smul_set_iff]
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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
this : k • B = B
⊢ b ∈ B

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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
this : k • B = B
⊢ b ∈ B
Tactic:
exact hb
State after:
no goals

State before:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ ¬_root_.Disjoint ({ val := k, property := ?m.108597 } • B) B
Tactic:
rw [Set.not_disjoint_iff_nonempty_inter]
State after:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ Set.Nonempty ({ val := k, property := ?m.108597 } • B ∩ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

State before:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ Set.Nonempty ({ val := k, property := ?m.108597 } • B ∩ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
change (k • B ∩ B).Nonempty
State after:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ Set.Nonempty (k • B ∩ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

State before:
case 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ Set.Nonempty (k • B ∩ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
use a
State after:
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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ k • B ∩ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ k • B ∩ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
constructor
State after:
case h.left
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ k • B

case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

State before:
case h.left
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ k • B

case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
rw [mem_fixingSubgroup_iff] at hk
State after:
case h.left
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : ∀ y ∈ s, k • y = y
hkbx : k • b = x
⊢ a ∈ k • B

case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

State before:
case h.left
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : ∀ y ∈ s, k • y = y
hkbx : k • b = x
⊢ a ∈ k • B

case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
rw [← hk a ha']
State after:
case h.left
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : ∀ y ∈ s, k • y = y
hkbx : k • b = x
⊢ k • a ∈ k • B

case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

State before:
case h.left
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : ∀ y ∈ s, k • y = y
hkbx : k • b = x
⊢ k • a ∈ k • B

case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
exact Set.smul_mem_smul_set ha
State after:
case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

State before:
case h.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 : 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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ a ∈ 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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
exact ha
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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G

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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ G
Tactic:
apply le_of_lt hG
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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ stabilizer (Perm α) s

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
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ᶜ
x : α
hx' : x ∈ sᶜ
k : Perm α
hk : k ∈ fixingSubgroup (Perm α) s
hkbx : k • b = x
⊢ k ∈ stabilizer (Perm α) s
Tactic:
exact fixingSubgroup_le_stabilizer (Equiv.Perm α) s hk
State after:
no goals

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
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ ∃ k, k • b = x
Tactic:
suffices
  IsPretransitive (fixingSubgroup (Equiv.Perm α) s)
    (SubMulAction.ofFixingSubgroup (Equiv.Perm α) s) by
  obtain ⟨k, hk⟩ :=
    exists_smul_eq (fixingSubgroup (Equiv.Perm α) s)
     (⟨b, hb'⟩ : SubMulAction.ofFixingSubgroup (Equiv.Perm α) s) ⟨x, hx'⟩
  use k
  rw [← Subtype.coe_inj, SubMulAction.val_smul] at hk
  exact hk
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
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)

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
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
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
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ IsMultiplyPretransitive (↥(fixingSubgroup (Perm α) s)) (↥(SubMulAction.ofFixingSubgroup (Perm α) s)) 1

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
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ IsMultiplyPretransitive (↥(fixingSubgroup (Perm α) s)) (↥(SubMulAction.ofFixingSubgroup (Perm α) s)) 1
Tactic:
apply remaining_transitivity'
State after:
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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ IsMultiplyPretransitive (Perm α) α ?n

case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ 1 + Set.ncard s ≤ ?n

case hn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ ↑?n ≤ PartENat.card α

case n
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ ℕ

State before:
case hn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ ↑(Nat.card α) ≤ PartENat.card α
Tactic:
simp only [Nat.card_eq_fintype_card, PartENat.card_eq_coe_fintype_card, le_refl]
State after:
no goals

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
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ᶜ
x : α
hx' : x ∈ sᶜ
this : IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
⊢ ∃ k, k • b = x
Tactic:
obtain ⟨k, hk⟩ :=
  exists_smul_eq (fixingSubgroup (Equiv.Perm α) s)
   (⟨b, hb'⟩ : SubMulAction.ofFixingSubgroup (Equiv.Perm α) s) ⟨x, hx'⟩
State after:
case 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ᶜ
x : α
hx' : x ∈ sᶜ
this : IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
k : ↥(fixingSubgroup (Perm α) s)
hk : k • { val := b, property := hb' } = { val := x, property := hx' }
⊢ ∃ k, k • b = x

State before:
case 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ᶜ
x : α
hx' : x ∈ sᶜ
this : IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
k : ↥(fixingSubgroup (Perm α) s)
hk : k • { val := b, property := hb' } = { val := x, property := hx' }
⊢ ∃ k, k • b = x
Tactic:
use k
State after:
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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
this : IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
k : ↥(fixingSubgroup (Perm α) s)
hk : k • { val := b, property := hb' } = { val := x, property := hx' }
⊢ k • b = x

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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
this : IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
k : ↥(fixingSubgroup (Perm α) s)
hk : k • { val := b, property := hb' } = { val := x, property := hx' }
⊢ k • b = x
Tactic:
rw [← Subtype.coe_inj, SubMulAction.val_smul] at hk
State after:
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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
this : IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
k : ↥(fixingSubgroup (Perm α) s)
hk : k • ↑{ val := b, property := hb' } = ↑{ val := x, property := hx' }
⊢ k • b = x

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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
this : IsPretransitive ↥(fixingSubgroup (Perm α) s) ↥(SubMulAction.ofFixingSubgroup (Perm α) s)
k : ↥(fixingSubgroup (Perm α) s)
hk : k • ↑{ val := b, property := hb' } = ↑{ val := x, property := hx' }
⊢ k • b = x
Tactic:
exact hk
State after:
no goals

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ᶜ
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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ IsMultiplyPretransitive (Perm α) α ?n
Tactic:
exact Equiv.Perm.isMultiplyPretransitive α (Nat.card α)
State after:
no goals

State before:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ 1 + Set.ncard s ≤ Nat.card α
Tactic:
rw [add_comm]
State after:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ Set.ncard s + 1 ≤ Nat.card α

State before:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ Set.ncard s + 1 ≤ Nat.card α
Tactic:
rw [← Set.ncard_add_ncard_compl s]
State after:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ Set.ncard s + 1 ≤ Set.ncard s + Set.ncard sᶜ

State before:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ Set.ncard s + 1 ≤ Set.ncard s + Set.ncard sᶜ
Tactic:
simp only [add_le_add_iff_left]
State after:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ 1 ≤ Set.ncard sᶜ

State before:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ 1 ≤ Set.ncard sᶜ
Tactic:
rw [Nat.succ_le_iff, Set.ncard_pos]
State after:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ Set.Nonempty sᶜ

State before:
case hmn
α : 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ᶜ
x : α
hx' : x ∈ sᶜ
⊢ Set.Nonempty sᶜ
Tactic:
exact h1
State after:
no goals

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
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
this : g • B = B
⊢ x ∈ B
Tactic:
rw [← hgbx, ← this, Set.smul_mem_smul_set_iff]
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
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
this : g • B = B
⊢ b ∈ B

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
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
this : g • B = B
⊢ b ∈ B
Tactic:
exact hsc_le_B hb
State after:
no goals

State before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a
α : 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 < ?m.122286
Tactic:
exact hα
State after:
no goals

State before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a
α : 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
Tactic:
rw [MulAction.smul_set_ncard_eq]
State after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a
α : 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 B + Set.ncard B

State before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a
α : 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 B + Set.ncard B
Tactic:
simp only [← two_mul]
State after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a
α : 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
⊢ 2 * Set.ncard sᶜ ≤ 2 * Set.ncard B

State before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a
α : 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
⊢ 2 * Set.ncard sᶜ ≤ 2 * Set.ncard B
Tactic:
apply Nat.mul_le_mul_left
State after:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a.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 B

State before:
case has_trivial_blocks'.intro.intro.intro.intro.intro.intro.mk.h.a.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 B
Tactic:
exact Set.ncard_le_ncard hsc_le_B (Set.toFinite B)
State after:
no goals