mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ a ∈ B

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ a ∈ B
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x

Tactic:
]

Goal state after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case mp
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ a ∈ B

Tactic:
]

Goal state after:
case mp
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ a ∈ B
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ H.Normal

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ H.Normal
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ ⊤.Normal

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ ⊤.Normal
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
]

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 1
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Tactic:
]

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 1
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.index = H.index

Tactic:
]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.index = H.index
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card ↥(toPermHom G (G ⧸ H)).range ∣ Nat.card (Equiv.Perm (G ⧸ H))

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card ↥(toPermHom G (G ⧸ H)).range ∣ Nat.card (Equiv.Perm (G ⧸ H))
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ ⟨g, hg⟩ • orbit (↥H) a = orbit (↥H) a

Tactic:
]

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ ⟨g, hg⟩ • orbit (↥H) a = orbit (↥H) a
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index ∣ H.index !

pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index.Coprime (H.index - 1)!

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index ∣ H.index !

G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index.Coprime (H.index - 1)!
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.index - 1 < H.normalCore.index.minFac

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.index - 1 < H.normalCore.index.minFac
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
⊢ ∃ x y, x ≠ y

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
⊢ ∃ x y, x ≠ y
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False

Tactic:
]

Goal state after:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : {a} = univ
b : X
hb : b ≠ a
⊢ b ∈ univ

Tactic:
]

Goal state after:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : {a} = univ
b : X
hb : b ≠ a
⊢ b ∈ univ
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a✝ : α
⊢ a✝ ∈ ConjAct.ofConjAct k • g.support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
⊢ k • g.support = k • g.support

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (↥(stabilizer G B)) x
⊢ B.ncard = B.ncard

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ Nat.card X = Nat.card X

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB' : B.ncard * (orbit G B).ncard < B.ncard * 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B.Nonempty

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB' : B.ncard * (orbit G B).ncard < B.ncard * 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B.Nonempty
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB' : (orbit G B).ncard < 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ

Tactic:
]

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB' : (orbit G B).ncard < 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : IsEmpty X
⊢ B = Set.univ

Tactic:
]

Goal state after:
case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : IsEmpty X
⊢ B = Set.univ
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard = Set.univ.ncard
⊢ B = Set.univ

Tactic:
]

Goal state after:
case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard = Set.univ.ncard
⊢ B = Set.univ
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard = Set.univ.ncard
⊢ Set.univ = Set.univ

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ 0 < 2

Tactic:
]

Goal state after:
case inl
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ 0 < 2
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2

Tactic:
]

Goal state after:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
h : B.Nonempty
⊢ ¬2 ≤ B.ncard

Tactic:
]

Goal state after:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
h : B.Nonempty
⊢ ¬2 ≤ B.ncard
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ ∀ ⦃g : G⦄,
    ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B).Nonempty →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
]

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ ∀ ⦃g : G⦄,
    ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B).Nonempty →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True

Tactic:
]

Goal state after:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X

Tactic:
]

Goal state after:
X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)

Tactic:
]

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ g • b ∈ g • B

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ g • b ∈ g • B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ ∀ (x : X), ∃ g, g • a = x

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ ∀ (x : X), ∃ g, g • a = x
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
⊢ a ∈ fixedPoints G X

Tactic:
]

Goal state after:
case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
⊢ a ∈ fixedPoints G X
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ {a}

Tactic:
]

Goal state after:
case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ {a}
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ orbit G a

Tactic:
]

Goal state after:
case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ orbit G a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ b ∈ g • B'

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ b ∈ g • B'
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ x ∈ Set.univ

Tactic:
]

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ x ∈ Set.univ
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)

Tactic:
]

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: M : Type u_3
inst✝⁴ : Group M
α : Type u_4
inst✝³ : MulAction M α
N : Type u_5
β : Type u_6
inst✝² : Group N
inst✝¹ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst✝ : IsPreprimitive M α
hf : Function.Surjective ⇑f
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f '' ⇑f ⁻¹' B)

Tactic:
]

Goal state after:
M : Type u_3
inst✝⁴ : Group M
α : Type u_4
inst✝³ : MulAction M α
N : Type u_5
β : Type u_6
inst✝² : Group N
inst✝¹ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst✝ : IsPreprimitive M α
hf : Function.Surjective ⇑f
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f '' ⇑f ⁻¹' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
]

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
]

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B