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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ⊤.lowerCentralSeries n = ⊥

pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

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

pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → ⊤.lowerCentralSeries n = ⊥

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ ⊤.lowerCentralSeries n = ⊥ → nilpotencyClass G ≤ n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → ⊤.lowerCentralSeries n = ⊥

Tactic:
·

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

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

pp: case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ ⊤.lowerCentralSeries n = ⊥

Tactic:
·

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

Goal state before:
pp: case mpr
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
i : X
⊢ i ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x} →
    i ∈ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1}

Tactic:
·

Goal state after:
case mpr
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
i : X
⊢ i ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x} →
    i ∈ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1}
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: case mpr.inl
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w w' : α × Bool
hw : w' ∈ {z | z ≠ (w.1, !w.2)}
g : FreeGroup α
hg : g ∈ startsWith w'
⊢ (fun m ↦ m • x) ⟨g, hg⟩ ∈ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1}

pp: case mpr.inr
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
w : α × Bool
i : X
⊢ i ∈ {x | ∃ y ∈ MulAction.orbit (↑(startsWith w)) i, (mk [w])⁻¹ • y = x}

Tactic:
·

Goal state after:
case mpr.inl
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w w' : α × Bool
hw : w' ∈ {z | z ≠ (w.1, !w.2)}
g : FreeGroup α
hg : g ∈ startsWith w'
⊢ (fun m ↦ m • x) ⟨g, hg⟩ ∈ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1}
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: case mpr.inr
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
w : α × Bool
i : X
⊢ i ∈ {x | ∃ y ∈ MulAction.orbit (↑(startsWith w)) i, (mk [w])⁻¹ • y = x}

Tactic:
·

Goal state after:
case mpr.inr
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
w : α × Bool
i : X
⊢ i ∈ {x | ∃ y ∈ MulAction.orbit (↑(startsWith w)) i, (mk [w])⁻¹ • y = x}
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1
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'
⊢ (fun F ↦ ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a)
    (Functor.mapEnd (root' T) F')

pp: case refine_2
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'
⊢ ∀ (y : End (root' T) →* X),
    (fun F ↦ ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a)
        y →
      y = Functor.mapEnd (root' T) F'

Tactic:
·

Goal state after:
case refine_1
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'
⊢ (fun F ↦ ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a)
    (Functor.mapEnd (root' T) F')
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
⊢ FG G → ∃ n, Nonempty (Generators G (Fin n))

pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, Nonempty (Generators G (Fin n))) → FG G

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
⊢ FG G → ∃ n, Nonempty (Generators G (Fin n))
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, Nonempty (Generators G (Fin n))) → FG G

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, Nonempty (Generators G (Fin n))) → FG G
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mp
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
h : (y.1 / x.1, 1) ∈ I
⊢ (1, x.2 / y.2) ∈ I

pp: case mpr
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
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I

Tactic:
·

Goal state after:
case mp
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
h : (y.1 / x.1, 1) ∈ I
⊢ (1, x.2 / y.2) ∈ I
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mpr
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
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I

Tactic:
·

Goal state after:
case mpr
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
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

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

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 (Sum.recOn (↑⟨Sum.inr e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

Tactic:
·

Goal state after:
case refine_1.cons.inl
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 : b✝ ⟶ c✝
eT : Sum.inl e ∈ T b✝ c✝
⊢ F'.map (Sum.recOn (↑⟨Sum.inl e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1
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 (Sum.recOn (↑⟨Sum.inr e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

Tactic:
·

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 (Sum.recOn (↑⟨Sum.inr e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_2
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'
⊢ ∀ (y : End (root' T) →* X),
    (fun F ↦ ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a)
        y →
      y = Functor.mapEnd (root' T) F'

Tactic:
·

Goal state after:
case refine_2
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'
⊢ ∀ (y : End (root' T) →* X),
    (fun F ↦ ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a)
        y →
      y = Functor.mapEnd (root' T) F'
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1

pp: case pos
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 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)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ I = map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range

pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ≤
    (P.prod Q).range

Tactic:
·

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ I = map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass (G ⧸ center G) = n - 1

Tactic:
rcases n with (rfl | n)

Goal state after:
case pos.zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
⊢ nilpotencyClass (G ⧸ center G) = 0 - 1

case pos.succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
⊢ nilpotencyClass (G ⧸ center G) = 0 - 1

pp: case pos.succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1

Tactic:
·

Goal state after:
case pos.zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
⊢ nilpotencyClass (G ⧸ center G) = 0 - 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1

Tactic:
·

Goal state after:
case pos.succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) ≤ n

pp: case a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass (G ⧸ center G)

Tactic:
·

Goal state after:
case pos.succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) ≤ n
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ I →
    (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range

pp: case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range →
    (g, h) ∈ I

Tactic:
·

Goal state after:
case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ I →
    (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass (G ⧸ center G)

Tactic:
·

Goal state after:
case a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass (G ⧸ center G)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = 0
⊢ 0 = 0 - 1 + 1

pp: case succ
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = n✝ + 1
⊢ n✝ + 1 = n✝ + 1 - 1 + 1

Tactic:
·

Goal state after:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = 0
⊢ 0 = 0 - 1 + 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = n✝ + 1
⊢ n✝ + 1 = n✝ + 1 - 1 + 1

Tactic:
·

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = n✝ + 1
⊢ n✝ + 1 = n✝ + 1 - 1 + 1