awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯
have refine_2 : ∀ (n : ℕ),
  (∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) →
    ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
Tactic: refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊥
have refine_1 : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊥
Tactic: refine ⟨fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥
have refine_1 : H 0 = ⊥
Tactic: rw [tsub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊤
have refine_2 : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊤
Tactic: refine ⟨fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤
have refine_2 : H 0 = ⊤
Tactic: rw [tsub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ = nilpotencyClass G
have rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) sorry =
  Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) sorry
Tactic: rw [← least_descending_central_series_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊥) ⋯
have refine_1 : ∀ (n : ℕ),
  (∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) → Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
Tactic: refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯
have refine_2 : ∀ (n : ℕ),
  Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
Tactic: refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have refine_1 : lowerCentralSeries G n ≤ H n
Tactic: rw [← le_bot_iff, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass G)) ⊥
have rw : Eq (α := Subgroup G)
  (lowerCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) sorry)) ⊥
Tactic: rw [← lowerCentralSeries_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass G)) ⊥
have rw : Eq (α := Subgroup G)
  (lowerCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) sorry)) ⊥
Tactic: classical
  rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ ↔ nilpotencyClass G ≤ n
have mp : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → nilpotencyClass G ≤ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → nilpotencyClass G ≤ n
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ ↔ nilpotencyClass G ≤ n
have mpr : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ nilpotencyClass G ≤ n
have mp : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) sorry ≤ n
Tactic: rw [← lowerCentralSeries_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have mpr : LE.le (α := Subgroup G) (lowerCentralSeries G n) (lowerCentralSeries G (nilpotencyClass G))
Tactic: rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ ↔ nilpotencyClass G ≤ n
have mp : 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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → nilpotencyClass G ≤ n
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ ↔ nilpotencyClass G ≤ n
have mpr : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (lowerCentralSeries 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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
d : ℕ
hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ map H.subtype (lowerCentralSeries (↥H) (d + 1)) ≤ lowerCentralSeries G (d + 1)
have 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})
Tactic: rw [lowerCentralSeries_succ, lowerCentralSeries_succ, MonoidHom.map_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
d : ℕ
hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ 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})
have 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}
Tactic: apply Subgroup.closure_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n : ℕ
⊢ map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
have zero : map H.subtype (lowerCentralSeries (↥H) 0) ≤ lowerCentralSeries G 0
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⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n : ℕ
zero : map H.subtype (lowerCentralSeries (↥H) 0) ≤ lowerCentralSeries G 0
⊢ map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
have succ : ∀ (d : ℕ) (hd : map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d),
  map H.subtype (lowerCentralSeries (↥H) (d + 1)) ≤ lowerCentralSeries G (d + 1)
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⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
inst_1 : H_1.Normal
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Group.IsNilpotent.{u_1} ↥H
have rw : ∀ (hG : ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥),
  ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
Tactic: rw [nilpotent_iff_lowerCentralSeries] at *
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) ⊥
⊢ ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
have rcases : ∀ (n : ℕ) (hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥),
  ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
Tactic: rcases hG with ⟨n, hG⟩
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) ⊥
⊢ ∃ (n : ℕ), Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
have h : Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
Tactic: use n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
have this : map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
Tactic: have := lowerCentralSeries_map_subtype_le H n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
have 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
Tactic: simp only [hG, SetLike.le_def, mem_map, exists_imp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ nilpotencyClass.{u_1} ↥H ≤ nilpotencyClass G
have rw : Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) sorry ≤ nilpotencyClass G
Tactic: rw [← lowerCentralSeries_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) ⋯ ≤ nilpotencyClass G
have rw : Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) sorry ≤
  Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) sorry
Tactic: rw [← lowerCentralSeries_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ nilpotencyClass.{u_1} ↥H ≤ nilpotencyClass G
have repeat : Nat.find (p := fun (n : ℕ) ↦ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥) sorry ≤
  Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) sorry
Tactic: repeat rw [← lowerCentralSeries_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ 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) ⊥) ⋯
have h : ∀ (n : ℕ),
  Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
Tactic: apply Nat.find_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ 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) ⊥) ⋯
have h : ∀ (n : ℕ),
  Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥ → Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
Tactic: classical apply Nat.find_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG_1 : Group.IsNilpotent G
n : ℕ
hG : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
have this : map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
Tactic: have := lowerCentralSeries_map_subtype_le H n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (lowerCentralSeries (↥H) n) ⊥
have 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
Tactic: simp only [hG, SetLike.le_def, mem_map, exists_imp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
x : G
hx : Membership.mem (γ := Subgroup G) (upperCentralSeries G d.succ) x
y' : H
⊢ Membership.mem (γ := Subgroup H)
    (PSigma.fst (β := fun (H_1 : Subgroup H) ↦ H_1.Characteristic) (upperCentralSeriesAux H d))
    (Bracket.bracket (L := H) ((f : (a : G) → H) x : H) y')
have succ : ∀ (y : G),
  Membership.mem (α := H) (γ := Subgroup H)
    (PSigma.fst (β := fun (H_1 : Subgroup H) ↦ H_1.Characteristic) (upperCentralSeriesAux H d))
    (Bracket.bracket (L := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y) : H)
Tactic: rcases h y' with ⟨y, rfl⟩
Cleared hypotheses: y'
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
n : ℕ
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n
have zero : Subgroup.map f (upperCentralSeries G 0) ≤ upperCentralSeries H 0
Tactic: induction n with
  | zero => simp
  | succ d hd =>
    rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'
    rcases h y' with ⟨y, rfl⟩
    simpa using hd (mem_map_of_mem f (hx y))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
n : ℕ
zero : Subgroup.map f (upperCentralSeries G 0) ≤ upperCentralSeries H 0
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n
have succ : ∀ (d : ℕ) (hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d),
  Subgroup.map f (upperCentralSeries G (d + 1)) ≤ upperCentralSeries H (d + 1)
Tactic: induction n with
  | zero => simp
  | succ d hd =>
    rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'
    rcases h y' with ⟨y, rfl⟩
    simpa using hd (mem_map_of_mem f (hx y))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : Membership.mem (γ := Subgroup G) (lowerCentralSeries G d.succ) x
y : G
h :
  Membership.mem (γ := Subgroup G)
    (closure
      {g : G |
        ∃ (g₁ : G),
          Membership.mem (γ := Subgroup G) (lowerCentralSeries G d) g₁ ∧
            ∃ (g₂ : G), Membership.mem (γ := Subgroup G) ⊤ g₂ ∧ ⁅g₁, g₂⁆ = g})
    y
hy : Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) y : H)
⊢ Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) y⁻¹ : H)
have rw : Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) (((f : (a : G) → H) y)⁻¹ : H)
Tactic: rw [f.map_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : Membership.mem (γ := Subgroup G) (lowerCentralSeries G d.succ) x
⊢ Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) x : H)
have succ : ∀ (x : G)
  (hx :
    Membership.mem (γ := Set G)
      {g : G |
        ∃ (g₁ : G),
          Membership.mem (γ := Subgroup G) (lowerCentralSeries G d) g₁ ∧
            ∃ (g₂ : G), Membership.mem (γ := Subgroup G) ⊤ g₂ ∧ ⁅g₁, g₂⁆ = g}
      x),
  Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) x : H)
Tactic: refine closure_induction (hx := hx) ?_ (by simp [f.map_one, Subgroup.one_mem _])
      (fun y z _ _ hy hz => by simp [map_mul, Subgroup.mul_mem _ hy hz]) (fun y _ hy => by
        rw [f.map_inv]; exact Subgroup.inv_mem _ hy)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : Membership.mem (γ := Subgroup G) (lowerCentralSeries G d.succ) x
y : G
hy : Membership.mem (γ := Subgroup G) (lowerCentralSeries G d) y
z : G
⊢ Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) ⁅y, z⁆ : H)
have succ : ∀ (K : Subgroup H),
  {g : H |
        ∃ (g₁ : H),
          Membership.mem (γ := Subgroup H) (lowerCentralSeries H d) g₁ ∧
            ∃ (g₂ : H), Membership.mem (γ := Subgroup H) ⊤ g₂ ∧ ⁅g₁, g₂⁆ = g} ⊆
      (↑K : Set H) →
    Membership.mem (α := H) K ((f : (a : G) → H) ⁅y, z⁆ : H)
Tactic: apply mem_closure.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
n : ℕ
⊢ Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n
have zero : Subgroup.map f (lowerCentralSeries G 0) ≤ lowerCentralSeries H 0
Tactic: induction n with
  | zero => simp
  | succ d hd =>
    rintro a ⟨x, hx : x ∈ lowerCentralSeries G d.succ, rfl⟩
    refine closure_induction (hx := hx) ?_ (by simp [f.map_one, Subgroup.one_mem _])
      (fun y z _ _ hy hz => by simp [map_mul, Subgroup.mul_mem _ hy hz]) (fun y _ hy => by
        rw [f.map_inv]; exact Subgroup.inv_mem _ hy)
    rintro a ⟨y, hy, z, ⟨-, rfl⟩⟩
    apply mem_closure.mpr
    exact fun K hK => hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutatorElement_def]⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
n : ℕ
zero : Subgroup.map f (lowerCentralSeries G 0) ≤ lowerCentralSeries H 0
⊢ Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n
have succ : ∀ (d : ℕ) (hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d),
  Subgroup.map f (lowerCentralSeries G (d + 1)) ≤ lowerCentralSeries H (d + 1)
Tactic: induction n with
  | zero => simp
  | succ d hd =>
    rintro a ⟨x, hx : x ∈ lowerCentralSeries G d.succ, rfl⟩
    refine closure_induction (hx := hx) ?_ (by simp [f.map_one, Subgroup.one_mem _])
      (fun y z _ _ hy hz => by simp [map_mul, Subgroup.mul_mem _ hy hz]) (fun y _ hy => by
        rw [f.map_inv]; exact Subgroup.inv_mem _ hy)
    rintro a ⟨y, hy, z, ⟨-, rfl⟩⟩
    apply mem_closure.mpr
    exact fun K hK => hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutatorElement_def]⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
h : LE.le (α := Subgroup G) (lowerCentralSeries G n) (center G)
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (n + 1)) ⊥
have rw : ∀ (y : G),
  Membership.mem (γ := Set G)
      {x : G |
        ∃ (p : G),
          Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧
            ∃ (q : G), Membership.mem (γ := Subgroup G) ⊤ q ∧ ⁅p, q⁆ = x}
      y →
    y = 1
Tactic: rw [lowerCentralSeries_succ, closure_eq_bot_iff, Set.subset_singleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
h : LE.le (α := Subgroup G) (lowerCentralSeries G n) (center G)
y : G
hy1 : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) y
z : G
⊢ ⁅y, z⁆ = 1
have rw : z * y = y * z
Tactic: rw [commutatorElement_def, mul_assoc, ← mul_inv_rev, mul_inv_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : Group.IsNilpotent H
⊢ Group.IsNilpotent G
have rw : ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
Tactic: rw [nilpotent_iff_lowerCentralSeries]