awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
rw :
  Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯
⊢ nilpotencyClass G' ≤ nilpotencyClass G

Tactic:
rw [nilpotencyClass_def, nilpotencyClass_def]

Premises used: Group.nilpotencyClass_def
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
h₁ : ∀ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯

Tactic:
apply Nat.find_mono

Premises used: Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
h₁ : ∀ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯

Tactic:
classical apply Nat.find_mono

Premises used: Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
h₁ : LE.le (α := Subgroup G') ⊤ (upperCentralSeries G' n)
⊢ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ ⊤ = f.range

Tactic:
symm (f.range_eq_top_of_surjective hf)

Premises used: MonoidHom.range_eq_top_of_surjective, symm
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ f.range = map f ⊤

Tactic:
MonoidHom.range_eq_map _

Premises used: MonoidHom.range_eq_map
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
rw rw₁ : map f ⊤ = map f ⊤
⊢ map f ⊤ = map f (upperCentralSeries G n)

Tactic:
rw [hn]
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ map f (upperCentralSeries G n) ≤ upperCentralSeries G' n

Tactic:
upperCentralSeries.map hf n

Premises used: Subgroup.upperCentralSeries.map
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
symm : map f ⊤ = map f (upperCentralSeries G n)
⊢ LE.le (α := Subgroup G') ⊤ (upperCentralSeries G' n)

Tactic:
calc
    ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
    _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
    _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
    _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n

Premises used: MonoidHom.range, Subgroup.map, MonoidHom.range_eq_map, Subgroup.upperCentralSeries, Subgroup.upperCentralSeries.map, MonoidHom.range_eq_top_of_surjective, symm, Top.top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
_h : IsNilpotent G
f : G ≃* G'
⊢ IsNilpotent G'

Tactic:
nilpotent_of_surjective f.toMonoidHom (MulEquiv.surjective f)

Premises used: MulEquiv.surjective, MulEquiv.toMonoidHom, Group.nilpotent_of_surjective
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
inst_2 : H.Normal
_h : IsNilpotent G
⊢ IsNilpotent.{u_1} (G ⧸ H)

Tactic:
nilpotent_of_surjective (QuotientGroup.mk' H) QuotientGroup.mk_surjective

Premises used: QuotientGroup.mk', Group.nilpotent_of_surjective, QuotientGroup.mk_surjective
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
_h : IsNilpotent G
⊢ nilpotencyClass.{u_1} (G ⧸ H) ≤ nilpotencyClass G

Tactic:
nilpotencyClass_le_of_surjective (QuotientGroup.mk' H) QuotientGroup.mk_surjective

Premises used: QuotientGroup.mk', QuotientGroup.mk_surjective, Group.nilpotencyClass_le_of_surjective
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
inst_1 : H₁.Normal
inst_2 : H₂.Normal
h : H₁ = H₂
subst : ∀ [inst_3 : H₁.Normal], comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂))

Tactic:
subst h
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H₁ : Subgroup G
inst_1 inst_2 : H₁.Normal
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) 0))
    (upperCentralSeries G (Nat.succ 0))

Tactic:
simp only [upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk',
      (upperCentralSeries_one G).symm]

Premises used: MonoidHom.comap_bot, Subgroup.upperCentralSeries_zero, Subgroup.upperCentralSeries_one, Eq.symm, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
Hn : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) :=
  upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n
rw rw₁ :
  comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn))) =
    comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn)))
⊢ comap (mk' (center G)) Hn.upperCentralSeriesStep =
    comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn)))

Tactic:
rw [upperCentralSeriesStep_eq_comap_center]

Premises used: Subgroup.upperCentralSeriesStep_eq_comap_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
Hn : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) :=
  upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n
⊢ comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn))) =
    comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn))

Tactic:
QuotientGroup.comap_comap_center

Premises used: QuotientGroup.comap_comap_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
Hn : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) :=
  upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n
⊢ comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) =
    comap (N := HasQuotient.Quotient G (B := Subgroup G) (upperCentralSeries G n.succ))
      (mk' (upperCentralSeries G n.succ))
      (center (HasQuotient.Quotient G (B := Subgroup G) (upperCentralSeries G n.succ)))

Tactic:
(comap_center_subst ih)

Premises used: _private.0.Subgroup.comap_center_subst
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
Hn : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) :=
  upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n
⊢ Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (upperCentralSeries G n.succ))
      (mk' (upperCentralSeries G n.succ))
      (center (HasQuotient.Quotient G (B := Subgroup G) (upperCentralSeries G n.succ))))
    (upperCentralSeriesStep (upperCentralSeries G n.succ))

Tactic:
symm (upperCentralSeriesStep_eq_comap_center _)

Premises used: Subgroup.upperCentralSeriesStep_eq_comap_center, symm
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  Eq (α := Subgroup G)
    (Subgroup.comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
Hn : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) :=
  upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n
comap :
  Subgroup.comap (mk' (center G)) Hn.upperCentralSeriesStep =
    Subgroup.comap (mk' (center G))
      (Subgroup.comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn)))
⊢ Eq (α := Subgroup G)
    (Subgroup.comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) (n + 1)))
    (upperCentralSeries G (n + 1).succ)

Tactic:
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 _)

Premises used: Subgroup.upperCentralSeries, Subgroup.center, _private.0.Subgroup.comap_center_subst, HasQuotient.Quotient, Subgroup.upperCentralSeriesStep_eq_comap_center, QuotientGroup.mk', Subgroup.upperCentralSeriesStep, symm, QuotientGroup.comap_comap_center, Nat.succ, Subgroup.comap
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
zero :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) 0))
    (upperCentralSeries G (Nat.succ 0))
succ :
  ∀ (n : ℕ)
    (ih :
      Eq (α := Subgroup G)
        (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
          (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
        (upperCentralSeries G n.succ)),
    Eq (α := Subgroup G)
      (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
        (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) (n + 1)))
      (upperCentralSeries G (n + 1).succ)
⊢ Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)

Tactic:
induction n with
  | zero =>
    simp only [upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk',
      (upperCentralSeries_one G).symm]
  | succ n ih =>
    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 _)

Premises used: MonoidHom.comap_bot, Subgroup.upperCentralSeries, Subgroup.center, HasQuotient.Quotient, Subgroup.upperCentralSeriesStep_eq_comap_center, QuotientGroup.mk', Subgroup.upperCentralSeries_zero, Subgroup.upperCentralSeries_one, Subgroup.upperCentralSeriesStep, symm, QuotientGroup.comap_comap_center, Eq.symm, QuotientGroup.ker_mk', Nat.succ, Subgroup.comap
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
rw₃ : Subsingleton.{u_1 + 1} (Subgroup G) ↔ Subsingleton G
rw₄ rw₅ : Subsingleton G ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G

Tactic:
rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]

Premises used: Nat.find_eq_zero, Group.nilpotencyClass_def, Subgroup.subsingleton_iff, Subgroup.upperCentralSeries_zero, subsingleton_iff_bot_eq_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
rw₃ : Subsingleton.{u_1 + 1} (Subgroup G) ↔ Subsingleton G
rw₄ rw₅ : Subsingleton G ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G

Tactic:
classical
  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]

Premises used: Nat.find_eq_zero, Group.nilpotencyClass_def, Subgroup.subsingleton_iff, Subgroup.upperCentralSeries_zero, subsingleton_iff_bot_eq_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
obtain :
  ∀ (n : ℕ)
    (hn :
      Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
        (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤),
    IsNilpotent G
⊢ IsNilpotent G

Tactic:
obtain ⟨n, hn⟩ := h.nilpotent

Premises used: Group.IsNilpotent.nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
n : ℕ
hn :
  Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
    (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤
h₁ : Eq (α := Subgroup G) (upperCentralSeries G n.succ) ⊤
⊢ IsNilpotent G

Tactic:
use n.succ

Premises used: Nat.succ
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
n : ℕ
hn :
  Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
    (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G n.succ) ⊤

Tactic:
simp [← comap_upperCentralSeries_quotient_center, hn]

Premises used: Subgroup.comap_upperCentralSeries_quotient_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
pos :
  ∀ (hH : IsNilpotent G),
    nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
neg :
  ∀ (hH : ¬IsNilpotent G),
    nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1

Tactic:
by_cases hH : IsNilpotent G

Premises used: Group.IsNilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : ¬IsNilpotent G
neg : ¬IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1

Tactic:
rw [nilpotencyClass_of_not_nilpotent hH, zero_tsub, nilpotencyClass_of_not_nilpotent]

Premises used: Group.nilpotencyClass_of_not_nilpotent, zero_tsub
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : ¬IsNilpotent G
⊢ ¬IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
mt of_quotient_center_nilpotent hH

Premises used: mt, Group.of_quotient_center_nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : ¬IsNilpotent G
⊢ ¬IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
exact mt of_quotient_center_nilpotent hH

Premises used: mt, Group.of_quotient_center_nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
pos :
  ∀ (n : ℕ) (hn : nilpotencyClass G = n),
    nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n - 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1

Tactic:
generalize hn : Group.nilpotencyClass G = n

Premises used: Group.nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
pos :
  ∀ (hn : nilpotencyClass G = 0),
    nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = HSub.hSub (α := ℕ) 0 1
pos₁ :
  ∀ (n : ℕ) (hn : nilpotencyClass G = n + 1),
    nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n + 1 - 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n - 1

Tactic:
rcases n with (rfl | n)

Premises used: rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
pos : ∀ (hn : Subsingleton G), Subsingleton.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = HSub.hSub (α := ℕ) 0 1

Tactic:
simp only [nilpotencyClass_zero_iff_subsingleton, zero_tsub] at *

Premises used: Group.nilpotencyClass_zero_iff_subsingleton, zero_tsub
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
Quotient.instSubsingletonQuotient (leftRel (center G))

Premises used: QuotientGroup.leftRel, Subgroup.center, Quotient.instSubsingletonQuotient
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
exact Quotient.instSubsingletonQuotient (leftRel (center G))

Premises used: QuotientGroup.leftRel, Subgroup.center, Quotient.instSubsingletonQuotient
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
this : nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n + 1 - 1

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
pos : nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n + 1 - 1

Tactic:
suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
pos : nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ≤ n
pos₁ : n ≤ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
pos :
  Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
    (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ≤ n

Tactic:
apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp

Premises used: Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le, Iff.mp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
pos :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ⊤)
⊢ Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
    (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤

Tactic:
apply comap_injective (f := (mk' (center G))) Quot.mk_surjective

Premises used: Subgroup.comap_injective, Quot.mk_surjective
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
pos : Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤
⊢ Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ⊤)

Tactic:
rw [comap_upperCentralSeries_quotient_center, comap_top, Nat.succ_eq_add_one, ← hn]

Premises used: Nat.succ_eq_add_one, Subgroup.comap_top, Subgroup.comap_upperCentralSeries_quotient_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤

Tactic:
upperCentralSeries_nilpotencyClass

Premises used: Subgroup.upperCentralSeries_nilpotencyClass