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

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i head : ι
m✝ : M head
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some head
h2✝ : m✝ ≠ 1
a✝ :
  ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        w✝).head =
    if h : ∃ (h : w✝.toList ≠ []), (w✝.toList.head h).fst = i then ⋯ ▸ (w✝.toList.head ⋯).snd else 1
hi : i = head
⊢ ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        (cons m✝ w✝ h1✝ h2✝)).head =
    if h : ∃ (h : (cons m✝ w✝ h1✝ h2✝).toList ≠ []), ((cons m✝ w✝ h1✝ h2✝).toList.head h).fst = i then
      ⋯ ▸ ((cons m✝ w✝ h1✝ h2✝).toList.head ⋯).snd
    else 1

Tactic:
subst hi

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w✝ : Word M
a✝ :
  ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        w✝).head =
    if h : ∃ (h : w✝.toList ≠ []), (w✝.toList.head h).fst = i then ⋯ ▸ (w✝.toList.head ⋯).snd else 1
m✝ : M i
h1✝ : w✝.fstIdx ≠ some i
h2✝ : m✝ ≠ 1
⊢ ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        (cons m✝ w✝ h1✝ h2✝)).head =
    if h : ∃ (h : (cons m✝ w✝ h1✝ h2✝).toList ≠ []), ((cons m✝ w✝ h1✝ h2✝).toList.head h).fst = i then
      ⋯ ▸ ((cons m✝ w✝ h1✝ h2✝).toList.head ⋯).snd
    else 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i head : ι
m✝ : M head
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some head
h2✝ : m✝ ≠ 1
a✝ :
  ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        w✝).head =
    if h : ∃ (h : w✝.toList ≠ []), (w✝.toList.head h).fst = i then ⋯ ▸ (w✝.toList.head ⋯).snd else 1
hi : ¬i = head
⊢ ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        (cons m✝ w✝ h1✝ h2✝)).head =
    if h : ∃ (h : (cons m✝ w✝ h1✝ h2✝).toList ≠ []), ((cons m✝ w✝ h1✝ h2✝).toList.head h).fst = i then
      ⋯ ▸ ((cons m✝ w✝ h1✝ h2✝).toList.head ⋯).snd
    else 1

Tactic:
· simp [hi, Ne.symm hi]

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.lengthParity w = Multiplicative.ofAdd ↑(cs.length w)

Tactic:
by
  rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
  rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]

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

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) = 1

Tactic:
exact cs.length_simple i

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
i : B
⊢ cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)

Tactic:
simp [leftInvSeq_eq_reverse_rightInvSeq_reverse, rightInvSeq]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : 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
y : (i : ι) × M i
hy : ⟨k✝, _w₂✝.head⟩ = y
⊢ ⟨j✝, _w₁✝.last⟩.fst ≠ y.fst

Tactic:
subst hy

Goal state after:
case append
ι : 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
⊢ ⟨j✝, _w₁✝.last⟩.fst ≠ ⟨k✝, _w₂✝.head⟩.fst
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : (cs.rightInvSeq ω)[j] ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * (cs.rightInvSeq ω)[j]) < cs.length (cs.wordProd ω)

Tactic:
← List.getD_eq_getElem _ 1 hj,

Goal state after:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : (cs.rightInvSeq ω)[j] ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * (cs.rightInvSeq ω).getD j 1) < cs.length (cs.wordProd ω)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length ((cs.leftInvSeq ω)[j] * cs.wordProd ω) < cs.length (cs.wordProd ω)

Tactic:
← List.getD_eq_getElem _ 1 hj,

Goal state after:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length ((cs.leftInvSeq ω).getD j 1 * cs.wordProd ω) < cs.length (cs.wordProd ω)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : 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_w₁ : ∀ (x : M i✝) (hnotone : x * _w₁✝.head ≠ 1), (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
w_ih_w₂ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (replaceHead (x * _w₂✝.head) hnotone _w₂✝).prod = of x * _w₂✝.prod
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Tactic:
| append _ _ _ w_ih_w₁ w_ih_w₂ =>

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
m m' : M
s s' : ℕ+
⊢ mk m s = mk m' s' ↔ ↑s' • m = ↑s • m'

Tactic:
by
  aesop (add simp [mk_eq_mk, nsmul_right_inj])

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
rw [qsmul_of_nonpos h]

Goal state after:
case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ -((have this := ⟨-a, ⋯⟩;
        this) •
        mk m s) =
    mk (a.num • m) (⟨a.den, ⋯⟩ * s)
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
by
  have := eq H K (mk H K g : Quotient ↑H ↑K).out g
  rw [out_eq'] at this
  obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl
  refine ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq ?_)⟩
  rw [← mul_assoc, ← T]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
induction a with | mk _

Goal state after:
case h₂.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a✝ : M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) (ArchimedeanClass.mk a✝) =
    OrderHom.id (ArchimedeanClass.mk a✝)
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: case inv
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x✝ : G
hx✝ : x✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
IH : g * x✝ * g⁻¹ ∈ H.focalSubgroup
⊢ g * x✝⁻¹ * g⁻¹ ∈ H.focalSubgroup

Tactic:
simpa [mul_assoc] using inv_mem IH

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: 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
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
by_cases! hm : n ≤ m

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
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

case neg
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
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
by_cases! hm : n ≤ m

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 → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ H (n - m)

case neg
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : m < n
⊢ ⁅x, g⁆ ∈ H (n - m)
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 = ⊥
⊢ map S.subtype ⊥ = ⊥

Tactic:
Subgroup.map_bot

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 = ⊥
⊢ ⊥ = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ (map f ⊤).lowerCentralSeries (nilpotencyClass H) ≤ ⊥

Tactic:
← lowerCentralSeries_nilpotencyClass (G := H)

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ (map f ⊤).lowerCentralSeries (nilpotencyClass H) ≤ ⊤.lowerCentralSeries (nilpotencyClass H)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ (F'.map (of e))⁻¹ = 1

Tactic:
inv_eq_one,

Goal state after:
case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ F'.map (of e) = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (n + 1)) = upperCentralSeries G (n + 1).succ

Tactic:
let Hn := upperCentralSeries (G ⧸ center G) n
    calc
      comap (mk' (center G)) (upperCentralSeriesStep Hn) =
          comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) := by
        rw [upperCentralSeriesStep_eq_comap_center]
      _ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
        QuotientGroup.comap_comap_center
      _ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) :=
        (comap_center_subst ih)
      _ = upperCentralSeriesStep (upperCentralSeries G n.succ) :=
        symm (upperCentralSeriesStep_eq_comap_center _)

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

Goal state before:
pp: case refine_2.e_5
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a : Generators G
⊢ ∀ (b : Generators G) (g : a ⟶ b), (functorOfMonoidHom T E).map (of g) = f' g

Tactic:
b

Goal state after:
case refine_2.e_5
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
⊢ ∀ (g : a ⟶ b), (functorOfMonoidHom T E).map (of g) = f' g
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
a b : ℕ
ab : a ≠ b
hn : upperCentralSeries G a = upperCentralSeries G b
⊢ upperCentralSeries G a = ⊤

Tactic:
grind only [IsNilpotent.nilpotent', IsNilpotent.nilpotent,
    upperCentralSeries_eq_top_iff_nilpotencyClass_le, eq_ge_of_eq_gt]

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
hB : IsBlock G B
g : G
⊢ g • B ≠ B → Disjoint (g • B) B

Tactic:
simpa using hB (g₂ := 1)

Goal state after:
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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, g • y • a = ⟨k, hk⟩ • g • a

Tactic:
use ⟨g⁻¹ * k * g, nN.conj_mem' k hk g⟩

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • ⟨g⁻¹ * k * g, ⋯⟩ • a = ⟨k, hk⟩ • g • a
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 : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
w✝ : X
ha : w✝ ∉ fixedPoints G X
⊢ IsPreprimitive G X

Tactic:
exact .of_isTrivialBlock_of_notMem_fixedPoints ha fun {B} _ ↦ H

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 : α
this : Fintype α := Fintype.ofFinite α
⊢ {a}ᶜ.card + 1 = Nat.card α

pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ ∀ (x : α), x ∈ {a}ᶜ ↔ x ∈ ofStabilizer G a

Tactic:
← Finset.card_singleton a,

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ {a}ᶜ.card + {a}.card = Nat.card α

G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ ∀ (x : α), x ∈ {a}ᶜ ↔ x ∈ ofStabilizer G a
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : ↑s
⊢ g • ↑x ∈ s

Tactic:
convert! Set.smul_mem_smul_set x.prop
    exact (mem_stabilizer_iff.mp g.prop).symm

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

Goal state before:
pp: case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a : α
⊢ ∀ {b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d

Tactic:
b

Goal state after:
case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b : α
⊢ ∀ {c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: 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 : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ (MulAut.conj g) k • y = y

Tactic:
MulAut.conj_apply,

Goal state after:
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 : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ (g * k * g⁻¹) • y = y
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
⊢ s.Nonempty

Tactic:
Set.nonempty_iff_ne_empty

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
⊢ s ≠ ∅
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
⊢ (∃ x ∈ fixingSubgroup M t, (MulAut.conj g) x = k) → k ∈ fixingSubgroup M s

Tactic:
rintro ⟨n, hn, rfl⟩
    exact Set.conj_mem_fixingSubgroup hg hn

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

Goal state before:
pp: case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Surjective ⇑(conjMap_ofFixingSubgroup hst)

Tactic:
· rintro ⟨x, hx⟩
    rw [eq_comm, ← inv_smul_eq_iff] at hst
    use (SubMulAction.conjMap_ofFixingSubgroup hst) ⟨x, hx⟩
    simp [← SetLike.coe_eq_coe]

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

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a : ↥(ofFixingSubgroup M (s ∪ t))
⊢ ∀ ⦃a₂ : ↥(ofFixingSubgroup M (s ∪ t))⦄,
    (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) a₂ → a = a₂

Tactic:
b

Goal state after:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
⊢ (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) b → a = b
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩

pp: case inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩

Tactic:
· obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨a, ha.1⟩ ⟨x, hx⟩
    use ⟨k, fun ⟨y, hy⟩ ↦ hk ⟨y, hy.1⟩⟩
    rwa [Subtype.ext_iff] at hkax ⊢

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩