awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact upperCentralSeries_nilpotencyClass

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

Tactic:
apply le_of_add_le_add_right

Premises used: le_of_add_le_add_right
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n + 1 = nilpotencyClass G

Tactic:
hn.symm

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

Tactic:
nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _))

Premises used: Group.nilpotencyClass_le_of_ker_le_center, le_of_eq, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ ℕ

Tactic:
n + 1 = Group.nilpotencyClass G := hn.symm
        _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 :=
          nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _))

Premises used: Subgroup.center, Group.nilpotencyClass, HasQuotient.Quotient, Group.nilpotencyClass_le_of_ker_le_center, le_of_eq, Eq.symm, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n + 1 ≤ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) + 1

Tactic:
calc
        n + 1 = Group.nilpotencyClass G := hn.symm
        _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 :=
          nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _))

Premises used: Subgroup.center, Group.nilpotencyClass, HasQuotient.Quotient, Group.nilpotencyClass_le_of_ker_le_center, le_of_eq, Eq.symm, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
rw : nilpotencyClass G = nilpotencyClass G - 1 + 1
⊢ nilpotencyClass G = nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) + 1

Tactic:
rw [nilpotencyClass_quotient_center]

Premises used: Group.nilpotencyClass_quotient_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
zero : ∀ (h : nilpotencyClass G = 0), 0 = HSub.hSub (α := ℕ) 0 1 + 1
succ : ∀ (n : ℕ) (h : nilpotencyClass G = n + 1), n + 1 = n + 1 - 1 + 1
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1

Tactic:
rcases h : Group.nilpotencyClass G with ⟨⟩

Premises used: Group.nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
h : nilpotencyClass G = 0
zero : False
⊢ 0 = HSub.hSub (α := ℕ) 0 1 + 1

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
h : nilpotencyClass G = 0
⊢ Subsingleton G

Tactic:
rw [nilpotencyClass_zero_iff_subsingleton] at h

Premises used: Group.nilpotencyClass_zero_iff_subsingleton
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
h : Subsingleton G
⊢ False

Tactic:
apply false_of_nontrivial_of_subsingleton G

Premises used: false_of_nontrivial_of_subsingleton
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
n : ℕ
h : nilpotencyClass G = n + 1
⊢ n + 1 = n + 1 - 1 + 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
⊢ ∃ (n : ℕ), nilpotencyClass G = n

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
obtain : ∀ (n : ℕ) (h : nilpotencyClass G = n), P G
⊢ P G

Tactic:
obtain ⟨n, h⟩ : ∃ n, Group.nilpotencyClass G = n := ⟨_, rfl⟩

Premises used: Group.nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = 0
zero : ∀ (this : Subsingleton G), P G
⊢ P G

Tactic:
haveI := nilpotencyClass_zero_iff_subsingleton.mp h
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = 0
this : Subsingleton G
⊢ P G

Tactic:
hbase _
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = 0
this : Subsingleton G
⊢ P G

Tactic:
exact hbase _
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n), P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = n + 1
⊢ nilpotencyClass.{u_2} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n

Tactic:
simp [nilpotencyClass_quotient_center, h]

Premises used: Group.nilpotencyClass_quotient_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n), P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = n + 1
succ : ∀ (hn : nilpotencyClass.{u_2} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n), P G
⊢ P G

Tactic:
have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
      simp [nilpotencyClass_quotient_center, h]
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n), P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = n + 1
hn : nilpotencyClass.{u_2} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n
⊢ P G

Tactic:
hstep _ (ih _ hn)
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n), P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = n + 1
hn : nilpotencyClass.{u_2} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n
⊢ P G

Tactic:
exact hstep _ (ih _ hn)
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
h : nilpotencyClass G = n
zero : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = 0), P G
succ :
  ∀ (n : ℕ) (ih : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n), P G)
    (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n + 1), P G
⊢ P G

Tactic:
induction n generalizing G with
  | zero =>
    haveI := nilpotencyClass_zero_iff_subsingleton.mp h
    exact hbase _
  | succ n ih =>
    have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
      simp [nilpotencyClass_quotient_center, h]
    exact hstep _ (ih _ hn)
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ LE.le (α := Subgroup G) (derivedSeries G 0) (lowerCentralSeries G 0)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
i : ℕ
ih : LE.le (α := Subgroup G) (derivedSeries G i) (lowerCentralSeries G i)
succ : LE.le (α := Subgroup G) (derivedSeries G i) ⊤
⊢ LE.le (α := Subgroup G) (derivedSeries G (i + 1)) (lowerCentralSeries G (i + 1))

Tactic:
apply commutator_mono ih

Premises used: Subgroup.commutator_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
i : ℕ
ih : LE.le (α := Subgroup G) (derivedSeries G i) (lowerCentralSeries G i)
⊢ LE.le (α := Subgroup G) (derivedSeries G i) ⊤

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
zero : LE.le (α := Subgroup G) (derivedSeries G 0) (lowerCentralSeries G 0)
succ :
  ∀ (i : ℕ) (ih : LE.le (α := Subgroup G) (derivedSeries G i) (lowerCentralSeries G i)),
    LE.le (α := Subgroup G) (derivedSeries G (i + 1)) (lowerCentralSeries G (i + 1))
⊢ LE.le (α := Subgroup G) (derivedSeries G n) (lowerCentralSeries G n)

Tactic:
induction n with
  | zero => simp
  | succ i ih => apply commutator_mono ih; simp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Group G_1
H : Subgroup G_1
inst_1 : H.Normal
G : Type u_2
inst_2 : CommGroup G
h : Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤
⊢ Group.IsNilpotent G

Tactic:
use 1
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Group G_1
H : Subgroup G_1
inst_1 : H.Normal
G : Type u_2
inst_2 : CommGroup G
h : Eq (α := Subgroup G) (center G) ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤

Tactic:
rw [upperCentralSeries_one]

Premises used: Subgroup.upperCentralSeries_one
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Group G_1
H : Subgroup G_1
inst_1 : H.Normal
G : Type u_2
inst_2 : CommGroup G
⊢ Eq (α := Subgroup G) (center G) ⊤

Tactic:
apply CommGroup.center_eq_top

Premises used: CommGroup.center_eq_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : CommGroup G
rw : Eq (α := Subgroup G) (center G) ⊤
⊢ nilpotencyClass G ≤ 1

Tactic:
rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_one]

Premises used: Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le, Subgroup.upperCentralSeries_one
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : CommGroup G
⊢ Eq (α := Subgroup G) (center G) ⊤

Tactic:
apply CommGroup.center_eq_top

Premises used: CommGroup.center_eq_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
inst_2 : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
rw : Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤
⊢ Eq (α := Subgroup G) (center G) ⊤

Tactic:
rw [← upperCentralSeries_one]

Premises used: Subgroup.upperCentralSeries_one
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
inst_2 : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤

Tactic:
upperCentralSeries_eq_top_iff_nilpotencyClass_le.mpr h

Premises used: Iff.mpr, Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
inst_2 : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤

Tactic:
exact upperCentralSeries_eq_top_iff_nilpotencyClass_le.mpr h

Premises used: Iff.mpr, Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a ≤ b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)

Tactic:
Nat.le_induction rfl ?_ b ab

Premises used: Nat.le_induction
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a ≤ b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))
refine :
  ∀ (n : ℕ) (hmn : a ≤ n),
    Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G n) →
      Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (n + 1))
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)

Tactic:
refine Nat.le_induction rfl ?_ b ab
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a ≤ b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))
⊢ ∀ (n : ℕ) (hmn : a ≤ n),
    Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G n) →
      Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (n + 1))

Tactic:
grind only [eq_def, upperCentralSeriesAux.eq_def]

Premises used: Subgroup.upperCentralSeriesAux.eq_def, Subgroup.upperCentralSeries.eq_def
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G c)

Tactic:
eq_ge_of_eq_succ ac (le_antisymm ?_ ?_)

Premises used: le_antisymm, Subgroup.upperCentralSeries.eq_ge_of_eq_succ
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
refine_1 : LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))
refine_2 : LE.le (α := Subgroup G) (upperCentralSeries G (a + 1)) (upperCentralSeries G a)
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G c)

Tactic:
refine eq_ge_of_eq_succ ac (le_antisymm ?_ ?_)

Premises used: le_antisymm, Subgroup.upperCentralSeries.eq_ge_of_eq_succ
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))

Tactic:
upperCentralSeries_mono _ <| Nat.le_succ ..

Premises used: Nat.le_succ, Subgroup.upperCentralSeries_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))

Tactic:
exact upperCentralSeries_mono _ <| Nat.le_succ ..

Premises used: Nat.le_succ, Subgroup.upperCentralSeries_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
refine_2 : LE.le (α := Subgroup G) (upperCentralSeries G (a + 1)) (upperCentralSeries G b)
⊢ LE.le (α := Subgroup G) (upperCentralSeries G (a + 1)) (upperCentralSeries G a)

Tactic:
rw [hn]
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ a + 1 ≤ b

Tactic:
grind
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ LE.le (α := Subgroup G) (upperCentralSeries G (a + 1)) (upperCentralSeries G b)

Tactic:
exact upperCentralSeries_mono _ (by grind)

Premises used: Subgroup.upperCentralSeries_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : Group.IsNilpotent G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) ⊤

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

Premises used: Group.IsNilpotent.nilpotent', Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le, Subgroup.upperCentralSeries.eq_ge_of_eq_gt, Group.IsNilpotent.nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
pos : ∀ (hG : Group.IsNilpotent G), nilpotencyClass G ≤ a
neg : ∀ (hG : ¬Group.IsNilpotent G), nilpotencyClass G ≤ a
⊢ nilpotencyClass G ≤ a

Tactic:
by_cases hG : IsNilpotent G

Premises used: Group.IsNilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
hG : Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a

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

Premises used: Subgroup.upperCentralSeries.eq_top, Group.IsNilpotent.nilpotent', Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le, Group.IsNilpotent.nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
hG : ¬Group.IsNilpotent G
neg : 0 ≤ a
⊢ nilpotencyClass G ≤ a

Tactic:
rw [nilpotencyClass_of_not_nilpotent hG]

Premises used: Group.nilpotencyClass_of_not_nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
hG : ¬Group.IsNilpotent G
⊢ 0 ≤ a

Tactic:
apply Nat.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
pos :
  ∀ (hG : Group.IsNilpotent G),
    _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
neg :
  ∀ (hG : ¬Group.IsNilpotent G),
    _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
⊢ _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

Tactic:
by_cases hG : IsNilpotent G

Premises used: Group.IsNilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a : ℕ
ha : a ∈ Set.Iic (nilpotencyClass G)
b : ℕ
hb : b ∈ Set.Iic (nilpotencyClass G)
ab : a < b
⊢ a ≤ nilpotencyClass G

Tactic:
simp only [Set.mem_Iic] at ha hb

Premises used: Set.mem_Iic
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a : ℕ
ha : a ∈ Set.Iic (nilpotencyClass G)
b : ℕ
hb : b ∈ Set.Iic (nilpotencyClass G)
ab : a < b
ha₁ : a ≤ nilpotencyClass G
⊢ b ≤ nilpotencyClass G

Tactic:
simp only [Set.mem_Iic] at ha hb

Premises used: Set.mem_Iic
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
pos : LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
pos₁ : Ne (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ LT.lt (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)

Tactic:
upperCentralSeries_mono _ ab.le

Premises used: LT.lt.le, Subgroup.upperCentralSeries_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)

Tactic:
exact upperCentralSeries_mono _ ab.le

Premises used: LT.lt.le, Subgroup.upperCentralSeries_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ Ne (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)

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

Premises used: Subgroup.upperCentralSeries.eq_top, Group.IsNilpotent.nilpotent', Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le, Group.IsNilpotent.nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : ¬Group.IsNilpotent G
neg : _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) {⊥}
⊢ _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

Tactic:
rw [nilpotencyClass_of_not_nilpotent hG, ← Nat.bot_eq_zero, Set.Iic_bot]

Premises used: Group.nilpotencyClass_of_not_nilpotent, Set.Iic_bot, Nat.bot_eq_zero
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) {⊥}

Tactic:
apply Set.strictMonoOn_singleton

Premises used: Set.strictMonoOn_singleton
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ Set.ncard (α := Subgroup G) (upperCentralSeries G '' Set.Iic a) = a + 1

Tactic:
Set.ncard_eq_of_bijective (fun _ => upperCentralSeries G ·) ?_ ?_ ?_

Premises used: Set.ncard_eq_of_bijective, Subgroup.upperCentralSeries