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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
hm : reduceCyclically x.toWord = reduceCyclically y.toWord
this : x = y
⊢ x = y

Tactic:
]

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
hm : reduceCyclically x.toWord = reduceCyclically y.toWord
this : x = y
⊢ x = y
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
hm : m < n
⊢ H (n - m) = H (n - m)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
hC✝ : 0 < g.toWord.length
h : g.toWord[0].1 = w.1 → g.toWord[0].2 = w.2
hC : True
⊢ (List.rec [w] (fun head tail tail_ih ↦ if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
        (g.toWord.head ⋯ :: g.toWord.tail))[0]? =
    some w

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
hC✝ : 0 < g.toWord.length
h : g.toWord[0].1 = w.1 → g.toWord[0].2 = w.2
hC : True
⊢ (List.rec [w] (fun head tail tail_ih ↦ if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
        (g.toWord.head ⋯ :: g.toWord.tail))[0]? =
    some w
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥

Tactic:
]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Tactic:
]

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ ⁅S.lowerCentralSeries d, S⁆.Characteristic

Tactic:
]

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ ⁅S.lowerCentralSeries d, S⁆.Characteristic
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑⁅S.lowerCentralSeries n, S⁆

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑⁅S.lowerCentralSeries n, S⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑(S.lowerCentralSeries n)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑(S.lowerCentralSeries n)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ ⁅(map f S).lowerCentralSeries d, map f S⁆ = ⁅(map f S).lowerCentralSeries d, map f S⁆

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ H.lowerCentralSeries n = H.lowerCentralSeries n

Tactic:
]

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

Goal state before:
pp: G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ homOfPath T ?m.29 = homOfPath T p

pp: G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, S.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, S.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ treeHom T
        (have this := a;
        this) ≫
      of e =
    treeHom T b

Tactic:
]

Goal state after:
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ treeHom T
        (have this := a;
        this) ≫
      of e =
    treeHom T b
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:
]

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 = ⊥
⊢ S.lowerCentralSeries n = ⊥
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 = ⊥
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inl e ∈ T a b
⊢ treeHom T
        (have this := a;
        this) ≫
      of e =
    homOfPath T default ≫ Sum.recOn (↑⟨Sum.inl e, H⟩) (fun e ↦ of e) fun e ↦ inv (of e)

Tactic:
]

Goal state after:
case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inl e ∈ T a b
⊢ treeHom T
        (have this := a;
        this) ≫
      of e =
    homOfPath T default ≫ Sum.recOn (↑⟨Sum.inl e, H⟩) (fun e ↦ of e) fun e ↦ inv (of e)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ S.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ S.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ Nat.find ⋯ ≤ n

Tactic:
]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ Nat.find ⋯ ≤ n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n

Tactic:
]

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inr e ∈ T b a
⊢ (homOfPath T default ≫ Sum.recOn (↑⟨Sum.inr e, H⟩) (fun e ↦ of e) fun e ↦ inv (of e)) ≫ of e = treeHom T b

Tactic:
]

Goal state after:
case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inr e ∈ T b a
⊢ (homOfPath T default ≫ Sum.recOn (↑⟨Sum.inr e, H⟩) (fun e ↦ of e) fun e ↦ inv (of e)) ≫ of e = treeHom T b
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ⊤.lowerCentralSeries n ≤ H n
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: 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.18
inst✝ : Monoid X
f : End (root' T) →* X
a : G
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries (Nat.find ⋯) = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries (Nat.find ⋯) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
⊢ Nat.find ⋯ ≤ n

Tactic:
]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
⊢ Nat.find ⋯ ≤ n
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: 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.18
inst✝ : Monoid X
f : End (root' T) →* X
X✝ Y✝ Z✝ : G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f (loopOfHom T (f✝ ≫ g✝)) = f (loopOfHom T g✝ * loopOfHom T f✝)

Tactic:
]

Goal state after:
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.18
inst✝ : Monoid X
f : End (root' T) →* X
X✝ Y✝ Z✝ : G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f (loopOfHom T (f✝ ≫ g✝)) = f (loopOfHom T g✝ * loopOfHom T f✝)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ ⊤.lowerCentralSeries n ≤ ⊤.lowerCentralSeries (nilpotencyClass G)

Tactic:
]

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ ⊤.lowerCentralSeries n ≤ ⊤.lowerCentralSeries (nilpotencyClass G)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
this : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
this : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ
h : upperCentralSeries G n = ⊤
this : Group.IsNilpotent G
⊢ upperCentralSeries G n = ⊤

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ
h : upperCentralSeries G n = ⊤
this : Group.IsNilpotent G
⊢ upperCentralSeries G n = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : Type u_2
inst✝ : Group K
f : G →* K
n : ℕ
⊢ (Subgroup.map f ⊤).lowerCentralSeries n ≤ ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
K : Type u_2
inst✝ : Group K
f : G →* K
n : ℕ
⊢ (Subgroup.map f ⊤).lowerCentralSeries n ≤ ⊤.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 S = ⊤

Tactic:
]

Goal state after:
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 S = ⊤
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 ι
f : G →* H
hf : Function.Surjective ⇑f
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
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✝ P : Generators G ι
e : ι' ≃ ι
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ ⁅S.lowerCentralSeries n, S⁆.Normal

Tactic:
]

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ ⁅S.lowerCentralSeries n, S⁆.Normal
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hG : ∃ n, ⊤.lowerCentralSeries n = ⊥
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hG : ∃ n, ⊤.lowerCentralSeries n = ⊥
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass G

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.nil
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 : WideSubquiver.toType (Symmetrify (Generators G)) T
⊢ 1 = 1

Tactic:
]

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
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
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
⊢ ∀ y ∈ {g | ∃ g₁ ∈ S.lowerCentralSeries n, ∃ g₂ ∈ S, ⁅g₁, g₂⁆ = g}, y = 1

Tactic:
]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ ↑y.1 = ↑x.1 ↔ ↑x.2 = ↑y.2

Tactic:
]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ ↑y.1 = ↑x.1 ↔ ↑x.2 = ↑y.2
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
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ z * y = y * z

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ z * y = y * z
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.cons
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✝
e : b✝ ⟶ c✝
ih : F'.map (homOfPath T p) = 1
⊢ F'.map (Sum.recOn (↑e) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

Tactic:
]

Goal state after:
case refine_1.cons
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✝
e : b✝ ⟶ c✝
ih : F'.map (homOfPath T p) = 1
⊢ F'.map (Sum.recOn (↑e) (fun e ↦ of e) fun e ↦ inv (of e)) = 1
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✝ : Group.IsNilpotent H
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥

Tactic:
]

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✝ : Group.IsNilpotent H
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥