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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨j✝, _w₁✝.last⟩ ∈ _w₁✝.toList.getLast?
_w₂_ih✝ : ⟨l✝, _w₂✝.last⟩ ∈ _w₂✝.toList.getLast?
⊢ ⟨l✝, (_w₁✝.append _hne✝ _w₂✝).last⟩ ∈ _w₂✝.toList.getLast?

Tactic:
by assumption

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
⊢ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList

Tactic:
by assumption

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
⊢ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList

Tactic:
by assumption

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω = (cs.wordProd ω)⁻¹ * cs.simple i * (cs.wordProd ω)⁻¹⁻¹

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * 1

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : DivisibleHull M
⊢ a ≤ a

Tactic:
induction a with | mk m s

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m : M
s : ℕ+
⊢ mk m s ≤ mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ≥0
h : b < c
⊢ b • a < c • a

Tactic:
induction a with | mk m s

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ b • mk m s < c • mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk a) =
    OrderHom.id (ArchimedeanClass.mk a)

Tactic:
induction a with | mk m s

Goal state after:
case h₁.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk (mk m s)) =
    OrderHom.id (ArchimedeanClass.mk (mk m s))
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ u * r * s = u * (r * s * (↑(f (r * s)))⁻¹) * ↑(f (r * s))

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ u * r * s⁻¹ = u * (↑(f (r * s⁻¹)) * s * r⁻¹)⁻¹ * ↑(f (r * s⁻¹))

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card ↥(_root_.commutator G) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ 0 <
    (center ↥(closureCommutatorRepresentatives G)).index ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)

Tactic:
exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.index_ne_zero) _

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hxP : x ∈ H
u : G
hzH : ⁅x, u⁆ ∈ H
⊢ g * ⁅x, u⁆ * g⁻¹ = ⁅g * x * g⁻¹, g * u * g⁻¹⁆

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ (g⁻¹ * h * g)⁻¹ * h = ⁅(g⁻¹ * h * g)⁻¹, g⁆

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
a b : G
ha : a ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
hb : b ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
y : G
⊢ ⁅a * b, y⁆ = ⁅a, b * y * b⁻¹⁆ * ⁅b, y⁆

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
⊢ ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g

Tactic:
rcases IsFreeGroup.unique_lift f' with ⟨F', hF', uF'⟩

Goal state after:
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk L₁ * mk L₂ * (mk L₃)⁻¹ * (mk L₃ * mk L₄ * mk L₅) = mk L₁ * (mk L₂ * mk L₄) * mk L₅

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ ⁅1, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
commutatorElement_one_left

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ 1 ∈ (fun m ↦ H (n - m)) (m + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
H : ℕ → Subgroup ↥S
hH : IsDescendingCentralSeries H
hn : H n = ⊥
h1 : ⊤.lowerCentralSeries n = ⊥
⊢ S.lowerCentralSeries n = ⊥

Tactic:
← top_subtype_lowerCentralSeries,

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
H : ℕ → Subgroup ↥S
hH : IsDescendingCentralSeries H
hn : H n = ⊥
h1 : ⊤.lowerCentralSeries n = ⊥
⊢ map S.subtype (⊤.lowerCentralSeries n) = ⊥
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P : Generators G ι
S : Set G
h : Subgroup.closure S = ⊤
⊢ Subgroup.closure (Set.range Subtype.val) = ⊤

Tactic:
by rwa [Subtype.range_coe]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Subgroup G
inst✝ : Group.IsNilpotent ↥S
n : ℕ
hn : nilpotencyClass ↥S ≤ n
⊢ S.lowerCentralSeries n = ⊥

Tactic:
← top_subtype_lowerCentralSeries,

Goal state after:
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
inst✝ : Group.IsNilpotent ↥S
n : ℕ
hn : nilpotencyClass ↥S ≤ n
⊢ map S.subtype (⊤.lowerCentralSeries n) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ closure {g | ∃ g₁ ∈ S.lowerCentralSeries n, ∃ g₂ ∈ S, ⁅g₁, g₂⁆ = g} = ⊥

Tactic:
closure_eq_bot_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ {g | ∃ g₁ ∈ S.lowerCentralSeries n, ∃ g₂ ∈ S, ⁅g₁, g₂⁆ = g} ⊆ {1}
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G b

Tactic:
exact upperCentralSeries_mono _ (by grind)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ nilpotencyClass (G₁ × G₂) = max (nilpotencyClass G₁) (nilpotencyClass G₂)

Tactic:
refine eq_of_forall_ge_iff fun k => ?_

Goal state after:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
k : ℕ
⊢ nilpotencyClass (G₁ × G₂) ≤ k ↔ max (nilpotencyClass G₁) (nilpotencyClass G₂) ≤ k
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ (have this := a✝;
    this) ⟶
    b✝

Tactic:
by assumption

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

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

Tactic:
obtain hB | hB := hB
  · apply Or.intro_left; apply Set.Subsingleton.image hB
  · apply Or.intro_right; rw [hB]
    simp only [Set.image_univ, Set.range_eq_univ, hf]

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

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

Tactic:
by
  obtain hB | hB := hB
  · apply Or.intro_left; exact Set.Subsingleton.preimage hB hf
  · apply Or.intro_right; simp only [hB]; apply Set.preimage_univ

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • op d • ↑s = b • ↑s

Tactic:
op_smul_coe_set hd

Goal state after:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • ↑s = b • ↑s
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
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a → x ∈ B

pp: case mpr
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
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a

Tactic:
· rintro ⟨⟨k, k_mem⟩, rfl⟩
    simp only [Subgroup.mk_smul]
    rw [← k_mem, Set.smul_mem_smul_set_iff]
    exact ha

Goal state after:
case mpr
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
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a
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:
exact fun hb ↦ hB' (Nat.mul_le_mul_right _ hb)

Goal state after:
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
⊢ ∃ g, g • a = x

Tactic:
rw [← MulAction.mem_orbit_iff, H]

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: 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)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B = Set.univ

Tactic:
rw [Set.eq_univ_iff_ncard, eq_comm, ← hp.dvd_iff_eq ((Set.one_lt_ncard).mpr hB').ne']

Goal state after:
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)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B.ncard ∣ Nat.card X
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: case h
α : Type u_1
m n : ℕ
hn : ↑m + ↑n ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (range ⇑x) (range ⇑y)
i : Fin m
⊢ ((fun x ↦ (castAddEmb n).trans x) (append hxy)) i = x i

Tactic:
simp [trans_apply, coe_castAddEmb, append]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ 2 * 1 < (Nat.card α).factorial

Tactic:
← Nat.succ_le_iff

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ (2 * 1).succ ≤ (Nat.card α).factorial
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
H : Type u_3
β : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective ⇑f
y : ι ↪ β
⊢ ∃ a, (Injective.mulActionHom_embedding ι ⋯) a = y

Tactic:
obtain ⟨g, _, hfg⟩ := Function.bijective_iff_has_inverse.mp hf

Goal state after:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
H : Type u_3
β : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective ⇑f
y : ι ↪ β
g : β → α
left✝ : LeftInverse g ⇑f
hfg : RightInverse g ⇑f
⊢ ∃ a, (Injective.mulActionHom_embedding ι ⋯) a = y
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ g * (g⁻¹ * k * g) * g⁻¹ = k

Tactic:
group

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
g : M
hg : g • t = s
x✝ : ↥(ofFixingSubgroup M t)
x : α
hx : x ∈ ofFixingSubgroup M t
hgxt : g • x ∈ s
⊢ False

Tactic:
apply hx

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
g : M
hg : g • t = s
x✝ : ↥(ofFixingSubgroup M t)
x : α
hx : x ∈ ofFixingSubgroup M t
hgxt : g • x ∈ s
⊢ x ∈ t
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
g : M
hg : g • t = s
x✝ : ↥(ofFixingSubgroup M t)
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g • x ∈ ofFixingSubgroup M s

Tactic:
by
      intro hgxt; apply hx
      rw [← hg] at hgxt
      exact Set.smul_mem_smul_set_iff.mp hgxt

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

Goal state before:
pp: case h.inl
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ IsPretransitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a}) → IsMultiplyPretransitive G α 2

Tactic:
ofStabilizer.isMultiplyPretransitive (a := a)

Goal state after:
case h.inl
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ IsPretransitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a}) →
    IsMultiplyPretransitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case property
α : Type u_2
s : Set α
g : Perm ↑s
⊢ ofSubtype g ∈ stabilizer (Perm α) s

Tactic:
apply ofSubtype_mem_stabilizer

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
x✝¹ x✝ : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
⊢ S.inl n₁ * (s g₁ * S.inl n₂ * (s g₁)⁻¹) * (s g₁ * s g₂) = S.inl n₁ * s g₁ * (S.inl n₂ * s g₂)

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g ↦ S.inl n * s₂ g * (S.inl n)⁻¹
⊢ ⇑s₂ = fun g ↦ (S.inl n)⁻¹ * (S.inl n * s₂ g * (S.inl n)⁻¹) * (S.inl n)⁻¹⁻¹

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g ↦ S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g ↦ S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ (fun g ↦ S.inl n₁ * (S.inl n₂ * s₃ g * (S.inl n₂)⁻¹) * (S.inl n₁)⁻¹) = fun g ↦
    S.inl n₁ * S.inl n₂ * s₃ g * (S.inl n₁ * S.inl n₂)⁻¹

Tactic:
group

Goal state after:
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
A B : AddSubgroup M
inst✝² : Module.Finite ℤ ↥B
inst✝¹ : IsTorsionFree ℤ ↥B
h : A ≤ B
inst✝ : A.IsFiniteRelIndex B
this : (A.addSubgroupOf B).FiniteIndex
⊢ finrank ℤ ↥A = finrank ℤ ↥B

Tactic:
← finrank_eq_of_finiteIndex (A.addSubgroupOf B)

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
A B : AddSubgroup M
inst✝² : Module.Finite ℤ ↥B
inst✝¹ : IsTorsionFree ℤ ↥B
h : A ≤ B
inst✝ : A.IsFiniteRelIndex B
this : (A.addSubgroupOf B).FiniteIndex
⊢ finrank ℤ ↥A = finrank ℤ ↥(A.addSubgroupOf B)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ ReducedWord.prod φ (cons g u w h1 h2).toReducedWord • empty = cons g u w h1 h2

Tactic:
rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
      of_smul_eq_smul, unitsSMul]

Goal state after:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case inl
α : Type u_2
inst✝² : DecidableEq α
a c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a a ∈ M
hbc : Equiv.swap a c ∈ M
⊢ Equiv.swap a c ∈ M

pp: case inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
⊢ Equiv.swap a c ∈ M

Tactic:
· exact hbc

Goal state after:
case inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
⊢ Equiv.swap a c ∈ M
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∉ g.support
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d).support
⊢ False

Tactic:
apply hx

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∉ g.support
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d).support
⊢ x ∈ g.support