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
a : X
⊢ ∀ (a_1 : BlockMem G a), ⟨{a}, ⋯⟩ ≤ a_1

Tactic:
by

Goal state after:
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
⊢ H.Normal

Tactic:
by

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
B : Set X
inst✝ : Nontrivial X
a : X
⊢ Nontrivial (BlockMem G a)

Tactic:
by

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
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (↥(stabilizer G B)) x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k : Perm α
⊢ (ConjAct.toConjAct k • g).cycleFactorsFinset = Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset

Tactic:
by

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 • g).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
by

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
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ B.ncard = (stabilizer G x).relIndex (stabilizer G B)

Tactic:
by

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

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

Tactic:
by

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
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ (stabilizer G x).relIndex (stabilizer G B) * (orbit G B).ncard = Nat.card X

Tactic:
← index_stabilizer,

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
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ (stabilizer G x).relIndex (stabilizer G B) * (stabilizer G B).index = Nat.card X
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
hB_ne : B.Nonempty
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
g : Perm α
s : Finset α
⊢ ConjAct.toConjAct g • ofSubtype.range = ofSubtype.range

Tactic:
by

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
⊢ 0 < B.ncard

Tactic:
by

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' : Nat.card X < B.ncard * 2
⊢ B = Set.univ

Tactic:
by

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
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
by

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
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
⊢ B.Subsingleton

Tactic:
by

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
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ ∀ (k : G), a ∈ k • B → B' ⊆ k • B

Tactic:
by

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
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
⊢ B'.Finite

Tactic:
by

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
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
⊢ ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'

Tactic:
by

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
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:
by

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ ∃ g, g • x = y

Tactic:
by

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
B✝ : Set X
B : IsBlock G B✝
⊢ IsTrivialBlock B✝

Tactic:
by

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

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

Tactic:
by

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
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
⊢ a ∈ k⁻¹ • B'

Tactic:
by

Goal state after:
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
⊢ IsTrivialBlock B

Tactic:
by

Goal state after:
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
⊢ IsPretransitive G X

Tactic:
by

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
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'
⊢ a ∈ (k⁻¹ * g) • B'

Tactic:
by

Goal state after:
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
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
⊢ IsTrivialBlock B

Tactic:
by

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X

Tactic:
by

Goal state after:
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 B

Tactic:
by

Goal state after:
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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B

Tactic:
by

Goal state after:
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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α ↔ IsPreprimitive N β

Tactic:
by

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
a : X
hfB : B.Finite
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: ⊢ -1 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g g' : Perm α
hg : g.IsSwap
hg' : g'.IsSwap
⊢ g * g' ∈ alternatingGroup α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ l.prod ∈ alternatingGroup α ↔ Even l.length

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: n : ℕ
⊢ finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsSimpleOrder (BlockMem G a) ↔ IsPreprimitive G X

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ (alternatingGroup α).index = 2

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ (alternatingGroup α).index = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
β : Type u_2
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
⊢ map (↑e.permCongrHom) (alternatingGroup α) = alternatingGroup β

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ 2 * Nat.card ↥(alternatingGroup α) = Nat.card (Perm α)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ 2 * card ↥(alternatingGroup α) = card (Perm α)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ Nat.card ↥(alternatingGroup α) = (Nat.card α).factorial / 2

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : Nontrivial X
inst✝ : IsPreprimitive G X
a : X
⊢ IsCoatom (stabilizer G a)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
⊢ IsCyclic ↥(alternatingGroup α)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
⊢ x ∈ {a}ᶜ → g • x ∈ {a}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
t : Set ↥(ofStabilizer G a)
b : ↥(ofStabilizer G a)
hb : b ∈ t ∧ ↑b = a
⊢ ↑b ∈ {a}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
t : Set ↥(ofStabilizer G a)
⊢ a ∉ Subtype.val '' t

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ ENat.card ↥(ofStabilizer G a) + 1 = ENat.card α

Tactic:
by

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
this : orbit (↥N) a = {a}
⊢ n • a ∈ {a}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
⊢ Nat.card ↥(ofStabilizer G a) + 1 = Nat.card α

Tactic:
by

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
⊢ IsPretransitive (↥N) α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G✝ : Type u_1
inst✝³ : Group G✝
α✝ : Type u_2
inst✝² : MulAction G✝ α✝
G : Type u_3
inst✝¹ : AddGroup G
α : Type u_4
inst✝ : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x : ↥(SubAddAction.ofStabilizer G a)
hy : g +ᵥ ↑x ∈ {b}
⊢ ↑x ∈ {a}

Tactic:
by

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
⊢ IsPreprimitive G X

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G✝ : Type u_1
inst✝³ : Group G✝
α✝ : Type u_2
inst✝² : MulAction G✝ α✝
G : Type u_3
inst✝¹ : AddGroup G
α : Type u_4
inst✝ : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x✝ : ↥(AddAction.stabilizer G a)
x : ↥(SubAddAction.ofStabilizer G a)
k : G
hk : k ∈ AddAction.stabilizer G a
⊢ ⟨g +ᵥ ↑(⟨k, hk⟩ +ᵥ x), ⋯⟩ = (AddAction.stabilizerEquivStabilizer hg) ⟨k, hk⟩ +ᵥ ⟨g +ᵥ ↑x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
hy : g • ↑x ∈ {b}
⊢ ↑x ∈ {a}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x✝ : ↥(stabilizer G a)
k : G
hk : k ∈ stabilizer G a
⊢ ∀ (x : ↥(ofStabilizer G a)), ⟨g • ↑(⟨k, hk⟩ • x), ⋯⟩ = (stabilizerEquivStabilizer hg) ⟨k, hk⟩ • ⟨g • ↑x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ 2 ≤ σ.supportᶜ.card

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_3
inst✝¹ : AddGroup G
α : Type u_4
inst✝ : AddAction G α
g h k : G
a b c : α
hg : b = g +ᵥ a
hh : c = h +ᵥ b
hk : c = k +ᵥ a
H : k = h + g
⊢ ⇑(AddAction.stabilizerEquivStabilizer hh) ∘ ⇑(AddAction.stabilizerEquivStabilizer hg) =
    ⇑(AddAction.stabilizerEquivStabilizer hk)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x✝ : ↥(stabilizer G a)
⊢ ↑((⇑(stabilizerEquivStabilizer hh) ∘ ⇑(stabilizerEquivStabilizer hg)) x✝) = ↑((stabilizerEquivStabilizer hk) x✝)

Tactic:
simp [stabilizerEquivStabilizer, H, MulAut.conj, ← mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ ⇑(stabilizerEquivStabilizer hh) ∘ ⇑(stabilizerEquivStabilizer hg) = ⇑(stabilizerEquivStabilizer hk)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x : ↥(ofStabilizer G a)
⊢ (conjMap hh) ((conjMap hg) x) = (conjMap hk) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
⊢ (conjMap ⋯) ((conjMap hg) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G b)
⊢ (conjMap hg) ((conjMap ⋯) x) = x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (conjMap hh).comp (conjMap hg) = conjMap hk

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ Function.Bijective ⇑(conjMap hg)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
⊢ a ∉ Set.range ⇑(x.trans (subtype fun x ↦ x ∈ ofStabilizer G a))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
i : Fin n
⊢ (snoc x) i.castSucc = ↑(x i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ δ * C * ((g x) (G.symm w)) (G.symm w) + ((g' x) w) w = δ * C * ((g' x) w) w + ((g' x) w) w

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
⊢ (snoc x) (Fin.last n) = a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
i : Fin n
this : (Fin.Embedding.init (g • x)) i = (g • x) i.castSucc
⊢ ¬(Fin.Embedding.init (g • x)) i = (g • x) (Fin.last n)

Tactic:
by

Goal state after: