awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x y : G
h : x * y * x⁻¹ * y⁻¹ ∈ H ↔ x * y * (x⁻¹ * y⁻¹) ∈ H
⊢ ⁅x, y⁆ ∈ H ↔
    HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑y : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑y : G ⧸ H)

Tactic:
rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem,
    div_eq_mul_inv, mul_inv_rev, commutatorElement_def]

Premises used: QuotientGroup.coe_mk', commutatorElement_def, QuotientGroup.eq_iff_div_mem, eq_comm, div_eq_mul_inv, mul_inv_rev, QuotientGroup.mk_mul
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ H ↔ x * y * (x⁻¹ * y⁻¹) ∈ H

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
inst_2 : H.Characteristic
⊢ H.upperCentralSeriesStep.Characteristic

Tactic:
(upperCentralSeriesStep_eq_comap_center H) ▸ Characteristic.comap_quotient_mk centerCharacteristic

Premises used: Subgroup.centerCharacteristic, Eq.rec, Subgroup.upperCentralSeriesStep_eq_comap_center, Eq.symm, Subgroup.Characteristic.comap_quotient_mk
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
n : ℕ
⊢ Characteristic (upperCentralSeries G n)

Tactic:
(upperCentralSeriesAux G n).2

Premises used: PSigma.snd, Subgroup.upperCentralSeries, Subgroup.upperCentralSeriesAux
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (upperCentralSeries G 0) ⊥

Tactic:
rfl

Premises used: Subgroup.upperCentralSeries, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
h :
  ∀ (x : G), Membership.mem (γ := Subgroup G) (upperCentralSeries G 1) x ↔ Membership.mem (γ := Subgroup G) (center G) x
⊢ Eq (α := Subgroup G) (upperCentralSeries G 1) (center G)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
x : G
h : (∀ (y : G), ⁅x, y⁆ = 1) ↔ ∀ (g : G), g * x = x * g
⊢ Membership.mem (γ := Subgroup G) (upperCentralSeries G 1) x ↔ Membership.mem (γ := Subgroup G) (center G) x

Tactic:
simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep, mem_bot, mem_mk,
    Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_setOf_eq, mem_center_iff]

Premises used: Subgroup.mem_mk, Subgroup.upperCentralSeries, Subgroup.mem_center_iff, Subsemigroup.mem_mk, Set.mem_setOf_eq, Submonoid.mem_mk, Subgroup.upperCentralSeriesStep, Subgroup.upperCentralSeriesAux, Subgroup.mem_bot
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
x y : G
rw : x * y * x⁻¹ * y⁻¹ = 1 ↔ y * x = x * y
rw₁ : x * y * x⁻¹ = y ↔ y * x = x * y
rw₂ : x * y = y * x ↔ y * x = x * y
rw₃ rw₄ : y * x = x * y ↔ y * x = x * y
⊢ ⁅x, y⁆ = 1 ↔ y * x = x * y

Tactic:
rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]

Premises used: commutatorElement_def, mul_inv_eq_one, eq_comm, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
x : G
⊢ (∀ (y : G), ⁅x, y⁆ = 1) ↔ ∀ (g : G), g * x = x * g

Tactic:
exact forall_congr' fun y => by
    rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : AddGroup G
h :
  ∀ (x : G),
    Membership.mem (γ := AddSubgroup G) (AddSubgroup.upperCentralSeries G 1) x ↔
      Membership.mem (γ := AddSubgroup G) (AddSubgroup.center G) x
⊢ Eq (α := AddSubgroup G) (AddSubgroup.upperCentralSeries G 1) (AddSubgroup.center G)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : AddGroup G
x : G
h : (∀ (y : G), ⁅x, y⁆ = 0) ↔ ∀ (g : G), g + x = x + g
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.upperCentralSeries G 1) x ↔
    Membership.mem (γ := AddSubgroup G) (AddSubgroup.center G) x

Tactic:
simp only [AddSubgroup.upperCentralSeries, AddSubgroup.upperCentralSeriesAux,
    AddSubgroup.upperCentralSeriesStep, AddSubgroup.mem_bot, AddSubgroup.mem_mk,
    AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_setOf_eq, AddSubgroup.mem_center_iff]

Premises used: AddSubgroup.upperCentralSeriesStep, AddSubsemigroup.mem_mk, Set.mem_setOf_eq, AddSubgroup.mem_bot, AddSubgroup.mem_mk, AddSubmonoid.mem_mk, AddSubgroup.upperCentralSeries, AddSubgroup.mem_center_iff, AddSubgroup.upperCentralSeriesAux
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : AddGroup G
x y : G
rw : x + y + -x + -y = 0 ↔ y + x = x + y
rw₁ : x + y + -x = y ↔ y + x = x + y
rw₂ : x + y = y + x ↔ y + x = x + y
rw₃ rw₄ : y + x = x + y ↔ y + x = x + y
⊢ ⁅x, y⁆ = 0 ↔ y + x = x + y

Tactic:
rw [addCommutatorElement_def, add_neg_eq_zero, add_neg_eq_iff_eq_add, eq_comm]

Premises used: add_neg_eq_zero, addCommutatorElement_def, eq_comm, add_neg_eq_iff_eq_add
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : AddGroup G
x : G
⊢ (∀ (y : G), ⁅x, y⁆ = 0) ↔ ∀ (g : G), g + x = x + g

Tactic:
exact forall_congr' fun y => by
    rw [addCommutatorElement_def, add_neg_eq_zero, add_neg_eq_iff_eq_add, eq_comm]

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
⊢ Membership.mem (γ := Subgroup G) (upperCentralSeries G (n + 1)) x ↔
    ∀ (y : G), Membership.mem (γ := Subgroup G) (upperCentralSeries G n) ⁅x, y⁆

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : H ≃* G
⊢ Eq (α := Subgroup H) (comap (↑e : H →* G) (upperCentralSeries G 0)) (upperCentralSeries H 0)

Tactic:
simpa [MonoidHom.ker_eq_bot_iff] using e.injective

Premises used: MonoidHom.ker_eq_bot_iff, MulEquiv.injective
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : H ≃* G
n : ℕ
h :
  ∀ (x : H),
    Membership.mem (γ := Subgroup H) (comap (↑e : H →* G) (upperCentralSeries G (n + 1))) x ↔
      Membership.mem (γ := Subgroup H) (upperCentralSeries H (n + 1)) x
⊢ Eq (α := Subgroup H) (comap (↑e : H →* G) (upperCentralSeries G (n + 1))) (upperCentralSeries H (n + 1))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : H ≃* G
n : ℕ
x : H
⊢ Membership.mem (γ := Subgroup H) (comap (↑e : H →* G) (upperCentralSeries G (n + 1))) x ↔
    Membership.mem (γ := Subgroup H) (upperCentralSeries H (n + 1)) x

Tactic:
simp [mem_upperCentralSeries_succ_iff, ← comap_upperCentralSeries e n,
      ← e.toEquiv.forall_congr_right, commutatorElement_def]

Premises used: commutatorElement_def, Subgroup.mem_upperCentralSeries_succ_iff, MulEquiv.toEquiv, Equiv.forall_congr_right
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤

Tactic:
Group.IsNilpotent.nilpotent'

Premises used: Group.IsNilpotent.nilpotent'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
simp_rw :
  (∃ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ↔
    ∃ (n : ℕ), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
⊢ IsNilpotent G ↔ IsNilpotent H

Tactic:
simp_rw [isNilpotent_iff]

Premises used: Group.isNilpotent_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
⊢ (∃ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ↔
    ∃ (n : ℕ), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤

Tactic:
exists_congr fun n ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
refine_1 :
  ∀ (n : ℕ) (h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
refine_2 :
  ∀ (n : ℕ) (h : Eq (α := Subgroup H) (upperCentralSeries H n) ⊤), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ (∃ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ↔
    ∃ (n : ℕ), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤

Tactic:
refine exists_congr fun n ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
n : ℕ
h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Eq (α := Subgroup H) (upperCentralSeries H n) ⊤

Tactic:
simp [← Subgroup.comap_top e.symm.toMonoidHom, ← h]

Premises used: MulEquiv.toMonoidHom, Subgroup.comap_top, MulEquiv.symm
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
n : ℕ
h : Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤

Tactic:
simp [← Subgroup.comap_top e.toMonoidHom, ← h]

Premises used: MulEquiv.toMonoidHom, Subgroup.comap_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ IsNilpotent.{u_1} ↥⊤ ↔ IsNilpotent G

Tactic:
isNilpotent_congr Subgroup.topEquiv

Premises used: Group.isNilpotent_congr, Subgroup.topEquiv
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : IsNilpotent G
⊢ IsNilpotent.{u_1} ↥⊤

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
rw : ∀ (y : G), Membership.mem (γ := Subgroup G) (upperCentralSeries G n) ⁅x, y⁆
⊢ Membership.mem (γ := Subgroup G) (upperCentralSeries G (n + 1)) x

Tactic:
rw [mem_upperCentralSeries_succ_iff]

Premises used: Subgroup.mem_upperCentralSeries_succ_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), Membership.mem (γ := Subgroup G) (upperCentralSeries G n) ⁅x, y⁆

Tactic:
fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)

Premises used: And.right
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), Membership.mem (γ := Subgroup G) (upperCentralSeries G n) ⁅x, y⁆

Tactic:
exact fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)

Premises used: And.right
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ IsAscendingCentralSeries (upperCentralSeries G)

Tactic:
⟨rfl, fun _x _n h => h⟩

Premises used: Subgroup.IsAscendingCentralSeries, And.intro, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ Monotone (β := Subgroup G) (upperCentralSeries G)

Tactic:
monotone_nat_of_le_succ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
refine : ∀ (n : ℕ), LE.le (α := Subgroup G) (upperCentralSeries G n) (upperCentralSeries G (n + 1))
⊢ Monotone (β := Subgroup G) (upperCentralSeries G)

Tactic:
refine monotone_nat_of_le_succ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx : Membership.mem (γ := Subgroup G) (upperCentralSeries G n) x
y : G
rw :
  Membership.mem (γ := Subgroup G)
    (PSigma.fst (β := fun (H : Subgroup G) ↦ H.Characteristic) (upperCentralSeriesAux G n)) (x * (y * x⁻¹ * y⁻¹))
⊢ Membership.mem (γ := Subgroup G)
    (PSigma.fst (β := fun (H : Subgroup G) ↦ H.Characteristic) (upperCentralSeriesAux G n)) ⁅x, y⁆

Tactic:
rw [commutatorElement_def, mul_assoc, mul_assoc, ← mul_assoc y x⁻¹ y⁻¹]

Premises used: commutatorElement_def, mul_assoc, Inv.inv
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx : Membership.mem (γ := Subgroup G) (upperCentralSeries G n) x
y : G
⊢ Membership.mem (γ := Subgroup G)
    (PSigma.fst (β := fun (H : Subgroup G) ↦ H.Characteristic) (upperCentralSeriesAux G n)) (x * (y * x⁻¹ * y⁻¹))

Tactic:
mul_mem hx (Normal.conj_mem inferInstance x⁻¹ (inv_mem hx) y)

Premises used: inferInstance, InvMemClass.inv_mem, Inv.inv, Subgroup.Normal.conj_mem, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx : Membership.mem (γ := Subgroup G) (upperCentralSeries G n) x
y : G
⊢ Membership.mem (γ := Subgroup G)
    (PSigma.fst (β := fun (H : Subgroup G) ↦ H.Characteristic) (upperCentralSeriesAux G n)) (x * (y * x⁻¹ * y⁻¹))

Tactic:
exact mul_mem hx (Normal.conj_mem inferInstance x⁻¹ (inv_mem hx) y)

Premises used: inferInstance, InvMemClass.inv_mem, Inv.inv, Subgroup.Normal.conj_mem, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
mp : Group.IsNilpotent G → ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
mpr : (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) → Group.IsNilpotent G
⊢ Group.IsNilpotent G ↔ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
nH : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
⟨_, _, upperCentralSeries_isAscendingCentralSeries G, nH⟩

Premises used: Subgroup.upperCentralSeries_isAscendingCentralSeries, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
nH : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
exact ⟨_, _, upperCentralSeries_isAscendingCentralSeries G, nH⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Group.IsNilpotent G

Tactic:
use n
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
h : H n ≤ upperCentralSeries G n
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤

Tactic:
rw [eq_top_iff, ← hn]

Premises used: eq_top_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Tactic:
ascending_central_series_le_upper H hH n

Premises used: Subgroup.ascending_central_series_le_upper
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Tactic:
exact ascending_central_series_le_upper H hH n

Premises used: Subgroup.ascending_central_series_le_upper
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
hasc : IsAscendingCentralSeries H
⊢ H 0 = ⊥

Tactic:
obtain ⟨h0, hH⟩ := hasc
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
hasc : IsAscendingCentralSeries H
h0 : H 0 = ⊥
⊢ ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n

Tactic:
obtain ⟨h0, hH⟩ := hasc
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
⊢ IsDescendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)

Tactic:
⟨hn, fun x m hx g => ?_⟩

Premises used: And.intro, Subgroup.IsDescendingCentralSeries
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
refine :
  ∀ (x : G) (m : ℕ) (hx : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) m) x) (g : G),
    Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
⊢ IsDescendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)

Tactic:
refine ⟨hn, fun x m hx g => ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
pos : ∀ (hm : n ≤ m), Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
neg : ∀ (hm : m < n), Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆

Tactic:
by_cases! hm : n ≤ m
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : n ≤ m
pos : ∀ (hx : x = 1) (g : G) (hm : n ≤ m), Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆

Tactic:
rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx

Premises used: tsub_eq_zero_of_le, Subgroup.mem_bot
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x = 1
g : G
hm : n ≤ m
pos : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) (Bracket.bracket (L := G) 1 g)
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆

Tactic:
subst hx
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
pos : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) 1
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) (Bracket.bracket (L := G) 1 g)

Tactic:
rw [commutatorElement_one_left]

Premises used: commutatorElement_one_left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) 1

Tactic:
Subgroup.one_mem _

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) 1

Tactic:
exact Subgroup.one_mem _

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
neg : x ∈ H (n - (m + 1) + 1)
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆

Tactic:
apply hH
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ x ∈ H (n - m)

Tactic:
hx
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
h : H (n - (m + 1) + 1) = H (n - m)
⊢ x ∈ H (n - (m + 1) + 1)

Tactic:
convert! hx using 1
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
h : H (n + 1 - m.succ) = H (n - m)
h₁ : H (n + 1 - (m + 1)) = H (n - m)
h₂ h₃ : H (n - m) = H (n - m)
⊢ H (n - (m + 1) + 1) = H (n - m)

Tactic:
rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]

Premises used: Nat.succ_eq_add_one, Nat.succ_le_of_lt, tsub_add_eq_add_tsub, Nat.add_sub_add_right
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
⊢ H 0 = ⊤

Tactic:
obtain ⟨h0, hH⟩ := hdesc
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
h0 : H 0 = ⊤
⊢ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)

Tactic:
obtain ⟨h0, hH⟩ := hdesc
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
⊢ IsAscendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)

Tactic:
⟨hn, fun x m hx g => ?_⟩

Premises used: Subgroup.IsAscendingCentralSeries, And.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
refine :
  ∀ (x : G) (m : ℕ) (hx : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) x) (g : G),
    Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) m) ⁅x, g⁆
⊢ IsAscendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)

Tactic:
refine ⟨hn, fun x m hx g => ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) x
g : G
dsimp : ⁅x, g⁆ ∈ H (n - m)
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) m) ⁅x, g⁆

Tactic:
dsimp only at hx ⊢
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
pos : ∀ (hm : n ≤ m), ⁅x, g⁆ ∈ H (n - m)
neg : ∀ (hm : m < n), ⁅x, g⁆ ∈ H (n - m)
⊢ ⁅x, g⁆ ∈ H (n - m)

Tactic:
by_cases! hm : n ≤ m
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
⊢ n - m = 0

Tactic:
have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
hnm : n - m = 0
pos : Membership.mem (γ := Subgroup G) ⊤ ⁅x, g⁆
⊢ ⁅x, g⁆ ∈ H (n - m)

Tactic:
rw [hnm, h0]
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
hnm : n - m = 0
⊢ Membership.mem (γ := Subgroup G) ⊤ ⁅x, g⁆

Tactic:
mem_top _

Premises used: Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
hnm : n - m = 0
⊢ Membership.mem (γ := Subgroup G) ⊤ ⁅x, g⁆

Tactic:
exact mem_top _

Premises used: Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : m < n
⊢ ⁅x, g⁆ ∈ H (n - (m + 1) + 1)

Tactic:
hH x _ hx g