mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
hn : ⊤.lowerCentralSeries n = ⊥
⊢ (map f ⊤).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 : ℕ
hn : ⊤.lowerCentralSeries n = ⊥
⊢ (map f ⊤).lowerCentralSeries n ≤ ⊥
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)
⊢ have this := ⋯;
  have this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Tactic:
have := normal_goursatFst hI₁
  have := normal_goursatSnd hI₂
  exact (((QuotientGroup.mk' I.goursatFst).prodMap
    (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).exists_mulEquiv_range_eq_graph
    ((QuotientGroup.mk'_surjective _).comp hI₁) ((QuotientGroup.mk'_surjective _).comp hI₂)
    fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ mk_goursatFst_eq_iff_mk_goursatSnd_eq hI₁ hI₂ hx hy

Goal state after:
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
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 1

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✝ : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 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✝ : IsNilpotent H
this : IsNilpotent G
⊢ (map f ⊤).lowerCentralSeries (nilpotencyClass H) ≤ ⊤.lowerCentralSeries (nilpotencyClass H)

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✝ : 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.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' 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' e = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ map f ⊤ = map f ⊤

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find ⋯ ≤ Nat.find ⋯
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' 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' e = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n
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)
      (comap ((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd))
        (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).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)
      (comap ((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd))
        (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ map f ⊤ = map f ⊤

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
]

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

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ Subsingleton G ↔ Subsingleton G

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ 0 = 0

pp: case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ ¬IsNilpotent (G ⧸ center G)

Tactic:
]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ ¬IsNilpotent (G ⧸ center G)
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
⊢ upperCentralSeries G (nilpotencyClass 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
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
]

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

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False

Tactic:
]

Goal state after:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case pos
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
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ center G = ⊤ ↔ IsMulCommutative G

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ center G = ⊤ ↔ IsMulCommutative G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case h
G✝ : Type u_1
inst✝² : Group G✝
N : Subgroup G✝
inst✝¹ : N.Normal
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
]

Goal state after:
case h
G✝ : Type u_1
inst✝² : Group G✝
N : Subgroup G✝
inst✝¹ : N.Normal
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
]

Goal state after:
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ upperCentralSeries G 1 = ⊤

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ upperCentralSeries 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:
]

Goal state after:
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
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)
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
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : ↑(P ⟨(g₂, h₂), ⋯⟩) = g
hQ : ↑(Q ⟨(g₂, h₂), ⋯⟩) = h
⊢ (↑(P ⟨(g₂, h₂), ⋯⟩), ↑(Q ⟨(g₂, h₂), ⋯⟩)) ∈ 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)
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
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : ↑(P ⟨(g₂, h₂), ⋯⟩) = g
hQ : ↑(Q ⟨(g₂, h₂), ⋯⟩) = h
⊢ (↑(P ⟨(g₂, h₂), ⋯⟩), ↑(Q ⟨(g₂, h₂), ⋯⟩)) ∈ I
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ 0 ≤ a

Tactic:
]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ 0 ≤ a
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) {⊥}

Tactic:
]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) {⊥}
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)) * (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ = 1

Tactic:
]

Goal state after:
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)) * (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ = 1