awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯

Tactic:
le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Premises used: le_antisymm, Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
refine_1 :
  ∀ (n : ℕ),
    (∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) →
      ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
refine_2 :
  ∀ (n : ℕ),
    (∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) →
      ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Premises used: le_antisymm, Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
⟨fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩

Premises used: HSub.hSub, Subgroup.is_descending_rev_series_of_is_ascending, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
refine_1 : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊥
⊢ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
refine ⟨fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
refine_1 : H (n - n) = ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊥

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
refine_1 : H 0 = ⊥
⊢ H (n - n) = ⊥

Tactic:
rw [tsub_self]

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

Tactic:
hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥

Tactic:
exact hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
⟨fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩

Premises used: HSub.hSub, And.intro, Exists.intro, Subgroup.is_ascending_rev_series_of_is_descending
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
refine_2 : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊤
⊢ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
refine ⟨fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
refine_2 : H (n - n) = ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊤

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
refine_2 : H 0 = ⊤
⊢ H (n - n) = ⊤

Tactic:
rw [tsub_self]

Premises used: tsub_self
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Tactic:
hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Tactic:
exact hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
rw :
  Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ = nilpotencyClass G

Tactic:
rw [← least_descending_central_series_length_eq_nilpotencyClass]

Premises used: Subgroup.least_descending_central_series_length_eq_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯

Tactic:
le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Premises used: le_antisymm, Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
refine_1 :
  ∀ (n : ℕ),
    (∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) → Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
refine_2 :
  ∀ (n : ℕ),
    Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Premises used: le_antisymm, Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
refine_1 : lowerCentralSeries G n ≤ H n
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
rw [← le_bot_iff, ← hn]

Premises used: le_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n ≤ H n

Tactic:
descending_central_series_ge_lower H hH n

Premises used: Subgroup.descending_central_series_ge_lower
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n ≤ H n

Tactic:
exact descending_central_series_ge_lower H hH n

Premises used: Subgroup.descending_central_series_ge_lower
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
⟨lowerCentralSeries G, ⟨lowerCentralSeries_isDescendingCentralSeries, h⟩⟩

Premises used: Subgroup.lowerCentralSeries_isDescendingCentralSeries, Subgroup.lowerCentralSeries, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
exact ⟨lowerCentralSeries G, ⟨lowerCentralSeries_isDescendingCentralSeries, h⟩⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
rw :
  Eq (α := Subgroup G)
    (lowerCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯)) ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass G)) ⊥

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Premises used: Subgroup.lowerCentralSeries_length_eq_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Eq (α := Subgroup G)
    (lowerCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯)) ⊥

Tactic:
Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)

Premises used: Subgroup.nilpotent_iff_lowerCentralSeries, Iff.mp, Nat.find_spec
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Eq (α := Subgroup G)
    (lowerCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯)) ⊥

Tactic:
exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)

Premises used: Subgroup.nilpotent_iff_lowerCentralSeries, Iff.mp, Nat.find_spec
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
rw rw₁ rw₂ :
  Eq (α := Subgroup G)
    (lowerCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯)) ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass G)) ⊥

Tactic:
classical
  rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)

Premises used: Subgroup.lowerCentralSeries_length_eq_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → nilpotencyClass G ≤ n
mpr : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ ↔ nilpotencyClass G ≤ n

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
mp : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ n
⊢ nilpotencyClass G ≤ n

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Premises used: Subgroup.lowerCentralSeries_length_eq_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ n

Tactic:
Nat.find_le h

Premises used: Nat.find_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ n

Tactic:
exact Nat.find_le h

Premises used: Nat.find_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
mpr : LE.le (α := Subgroup G) (lowerCentralSeries G n) (lowerCentralSeries G (nilpotencyClass G))
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]

Premises used: Subgroup.lowerCentralSeries_nilpotencyClass, eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ LE.le (α := Subgroup G) (lowerCentralSeries G n) (lowerCentralSeries G (nilpotencyClass G))

Tactic:
lowerCentralSeries_antitone h

Premises used: Subgroup.lowerCentralSeries_antitone
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ LE.le (α := Subgroup G) (lowerCentralSeries G n) (lowerCentralSeries G (nilpotencyClass G))

Tactic:
exact lowerCentralSeries_antitone h

Premises used: Subgroup.lowerCentralSeries_antitone
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → nilpotencyClass G ≤ n
mpr mpr₁ : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ ↔ nilpotencyClass G ≤ n

Tactic:
classical
  constructor
  · intro h
    rw [← lowerCentralSeries_length_eq_nilpotencyClass]
    exact Nat.find_le h
  · intro h
    rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]
    exact lowerCentralSeries_antitone h

Premises used: Subgroup.lowerCentralSeries_nilpotencyClass, Subgroup.lowerCentralSeries_length_eq_nilpotencyClass, eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ map H.subtype (lowerCentralSeries (↥H) 0) ≤ lowerCentralSeries G 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
d : ℕ
hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
succ :
  LE.le (α := Subgroup G)
    (closure
      (Set.image (α := ↥H) (⇑H.subtype : (a : ↥H) → G)
        {x : ↥H |
          ∃ (p : ↥H),
            Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) d) p ∧
              ∃ (q : ↥H), Membership.mem (γ := Subgroup ↥H) ⊤ q ∧ ⁅p, q⁆ = x}))
    (closure
      {x : G |
        ∃ (p : G),
          Membership.mem (γ := Subgroup G) (lowerCentralSeries G d) p ∧
            ∃ (q : G), Membership.mem (γ := Subgroup G) ⊤ q ∧ ⁅p, q⁆ = x})
⊢ map H.subtype (lowerCentralSeries (↥H) (d + 1)) ≤ lowerCentralSeries G (d + 1)

Tactic:
rw [lowerCentralSeries_succ, lowerCentralSeries_succ, MonoidHom.map_closure]

Premises used: Subgroup.lowerCentralSeries_succ, MonoidHom.map_closure
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
d : ℕ
hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
succ :
  Subset (α := Set G)
    (Set.image (α := ↥H) (⇑H.subtype : (a : ↥H) → G)
      {x : ↥H |
        ∃ (p : ↥H),
          Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) d) p ∧
            ∃ (q : ↥H), Membership.mem (γ := Subgroup ↥H) ⊤ q ∧ ⁅p, q⁆ = x})
    {x : G |
      ∃ (p : G),
        Membership.mem (γ := Subgroup G) (lowerCentralSeries G d) p ∧
          ∃ (q : G), Membership.mem (γ := Subgroup G) ⊤ q ∧ ⁅p, q⁆ = x}
⊢ LE.le (α := Subgroup G)
    (closure
      (Set.image (α := ↥H) (⇑H.subtype : (a : ↥H) → G)
        {x : ↥H |
          ∃ (p : ↥H),
            Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) d) p ∧
              ∃ (q : ↥H), Membership.mem (γ := Subgroup ↥H) ⊤ q ∧ ⁅p, q⁆ = x}))
    (closure
      {x : G |
        ∃ (p : G),
          Membership.mem (γ := Subgroup G) (lowerCentralSeries G d) p ∧
            ∃ (q : G), Membership.mem (γ := Subgroup G) ⊤ q ∧ ⁅p, q⁆ = x})

Tactic:
apply Subgroup.closure_mono

Premises used: Subgroup.closure_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
d : ℕ
hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
x3 : ↥H
hx3 : Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) d) x3
x4 : ↥H
_hx4 : Membership.mem (γ := Subgroup ↥H) ⊤ x4
⊢ Membership.mem (γ := Subgroup G) ⊤ (↑x4 : G) ∧ ⁅(↑x3 : G), (↑x4 : G)⁆ = (H.subtype : (a : ↥H) → G) ⁅x3, x4⁆

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
d : ℕ
hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
x3 : ↥H
hx3 : Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) d) x3
x4 : ↥H
_hx4 : Membership.mem (γ := Subgroup ↥H) ⊤ x4
⊢ Membership.mem (α := G) (γ := Set G)
    {x : G |
      ∃ (p : G),
        Membership.mem (γ := Subgroup G) (lowerCentralSeries G d) p ∧
          ∃ (q : G), Membership.mem (γ := Subgroup G) ⊤ q ∧ ⁅p, q⁆ = x}
    ((H.subtype : (a : ↥H) → G) ⁅x3, x4⁆ : G)

Tactic:
exact ⟨x3, hd (mem_map.mpr ⟨x3, hx3, rfl⟩), x4, by simp⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n : ℕ
zero : map H.subtype (lowerCentralSeries (↥H) 0) ≤ lowerCentralSeries G 0
succ :
  ∀ (d : ℕ) (hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d),
    map H.subtype (lowerCentralSeries (↥H) (d + 1)) ≤ lowerCentralSeries G (d + 1)
⊢ map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n

Tactic:
induction n with
  | zero => simp
  | succ d hd =>
    rw [lowerCentralSeries_succ, lowerCentralSeries_succ, MonoidHom.map_closure]
    apply Subgroup.closure_mono
    rintro x1 ⟨x2, ⟨x3, hx3, x4, _hx4, rfl⟩, rfl⟩
    exact ⟨x3, hd (mem_map.mpr ⟨x3, hx3, rfl⟩), x4, by simp⟩

Premises used: Subgroup.closure_mono, Subgroup.lowerCentralSeries_succ, MonoidHom.map_closure, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
hG : Group.IsNilpotent G
rw :
  ∀ (hG : ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥),
    ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
⊢ Group.IsNilpotent.{u_1} ↥H

Tactic:
rw [nilpotent_iff_lowerCentralSeries] at *

Premises used: Subgroup.nilpotent_iff_lowerCentralSeries
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
hG : ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
rcases :
  ∀ (n : ℕ) (hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥),
    ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
⊢ ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥

Tactic:
rcases hG with ⟨n, hG⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
h : Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
⊢ ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥

Tactic:
use n
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n

Tactic:
have := lowerCentralSeries_map_subtype_le H n
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
this : map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
⊢ ∀ ⦃x : G⦄ (x_1 : ↥H),
    Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) n) x_1 ∧ (H.subtype : (a : ↥H) → G) x_1 = x →
      Membership.mem (γ := Subgroup G) ⊥ x

Tactic:
simp only [hG, SetLike.le_def, mem_map, exists_imp] at this

Premises used: SetLike.le_def, Subgroup.mem_map, exists_imp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
this :
  ∀ ⦃x : G⦄ (x_1 : ↥H),
    Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) n) x_1 ∧ (H.subtype : (a : ↥H) → G) x_1 = x →
      Membership.mem (γ := Subgroup G) ⊥ x
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥

Tactic:
eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)

Premises used: Iff.mpr, And.intro, eq_bot_iff, rfl, Subtype.ext
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
this :
  ∀ ⦃x : G⦄ (x_1 : ↥H),
    Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) n) x_1 ∧ (H.subtype : (a : ↥H) → G) x_1 = x →
      Membership.mem (γ := Subgroup G) ⊥ x
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥

Tactic:
exact eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) ⋯ ≤ nilpotencyClass G
⊢ nilpotencyClass.{u_1} ↥H ≤ nilpotencyClass G

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Premises used: Subgroup.lowerCentralSeries_length_eq_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
rw :
  Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) ⋯ ≤ nilpotencyClass G

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Premises used: Subgroup.lowerCentralSeries_length_eq_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
repeat :
  Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯
⊢ nilpotencyClass.{u_1} ↥H ≤ nilpotencyClass G

Tactic:
repeat rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Premises used: Subgroup.lowerCentralSeries_length_eq_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
h :
  ∀ (n : ℕ),
    Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯

Tactic:
apply Nat.find_mono

Premises used: Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
h :
  ∀ (n : ℕ),
    Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries 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
H : Subgroup G
hG_1 : Group.IsNilpotent G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n

Tactic:
have := lowerCentralSeries_map_subtype_le H n
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG_1 : Group.IsNilpotent G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
this : map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
⊢ ∀ ⦃x : G⦄ (x_1 : ↥H),
    Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) n) x_1 ∧ (H.subtype : (a : ↥H) → G) x_1 = x →
      Membership.mem (γ := Subgroup G) ⊥ x

Tactic:
simp only [hG, SetLike.le_def, mem_map, exists_imp] at this

Premises used: SetLike.le_def, Subgroup.mem_map, exists_imp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG_1 : Group.IsNilpotent G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
this :
  ∀ ⦃x : G⦄ (x_1 : ↥H),
    Membership.mem (γ := Subgroup ↥H) (lowerCentralSeries (↥H) n) x_1 ∧ (H.subtype : (a : ↥H) → G) x_1 = x →
      Membership.mem (γ := Subgroup G) ⊥ x
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥

Tactic:
eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)

Premises used: Iff.mpr, And.intro, eq_bot_iff, rfl, Subtype.ext