awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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
inst_1 : H.Normal
inst_2 : Subsingleton G
⊢ Group.IsNilpotent G

Tactic:
nilpotent_iff_lowerCentralSeries.2 ⟨0, Subsingleton.elim ⊤ ⊥⟩

Premises used: Iff.mpr, Bot.bot, Subgroup.nilpotent_iff_lowerCentralSeries, Exists.intro, Subsingleton.elim, Top.top, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Nilpotent
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)
⊢ Subgroup.map f (upperCentralSeries G 0) ≤ upperCentralSeries H 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
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
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)
⊢ 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')

Tactic:
rcases h y' with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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 : 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:
simpa using hd (mem_map_of_mem f (hx y))

Premises used: Subgroup.mem_map_of_mem
-- Module: Mathlib.GroupTheory.Nilpotent
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
succ :
  ∀ (d : ℕ) (hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d),
    Subgroup.map f (upperCentralSeries G (d + 1)) ≤ upperCentralSeries H (d + 1)
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n

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))

Premises used: rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
⊢ Subgroup.map f (lowerCentralSeries G 0) ≤ lowerCentralSeries H 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
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) 1 : H)

Tactic:
simp [f.map_one, Subgroup.one_mem _]

Premises used: Subgroup.one_mem, MonoidHom.map_one
-- Module: Mathlib.GroupTheory.Nilpotent
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 z : 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
h_1 :
  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})
    z
hy : Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) y : H)
hz : Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) z : H)
⊢ Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) (y * z) : H)

Tactic:
simp [map_mul, Subgroup.mul_mem _ hy hz]

Premises used: map_mul, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Nilpotent
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)
rw : 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)

Tactic:
rw [f.map_inv]

Premises used: MonoidHom.map_inv
-- Module: Mathlib.GroupTheory.Nilpotent
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)

Tactic:
Subgroup.inv_mem _ hy

Premises used: Set.Mem, Subgroup.inv_mem
-- Module: Mathlib.GroupTheory.Nilpotent
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)

Tactic:
exact Subgroup.inv_mem _ hy

Premises used: Subgroup.inv_mem
-- Module: Mathlib.GroupTheory.Nilpotent
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
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)
⊢ 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)
-- Module: Mathlib.GroupTheory.Nilpotent
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
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)
⊢ Membership.mem (α := H) (γ := Subgroup H) (lowerCentralSeries H (d + 1)) ((f : (a : G) → H) ⁅y, z⁆ : H)

Tactic:
apply mem_closure.mpr

Premises used: Iff.mpr, Subgroup.mem_closure
-- Module: Mathlib.GroupTheory.Nilpotent
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
K : Subgroup H
hK :
  {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)
⊢ ∃ (g₂ : H),
    Membership.mem (γ := Subgroup H) ⊤ g₂ ∧
      Bracket.bracket (L := H) ((f : (a : G) → H) y : H) g₂ = (f : (a : G) → H) ⁅y, z⁆

Tactic:
simp [commutatorElement_def]

Premises used: commutatorElement_def
-- Module: Mathlib.GroupTheory.Nilpotent
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
⊢ ∀ (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:
exact fun K hK => hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutatorElement_def]⟩
-- Module: Mathlib.GroupTheory.Nilpotent
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
succ :
  ∀ (d : ℕ) (hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d),
    Subgroup.map f (lowerCentralSeries G (d + 1)) ≤ lowerCentralSeries H (d + 1)
⊢ Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n

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]⟩

Premises used: Iff.mpr, Subgroup.mem_closure, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
h : LE.le (α := Subgroup G) (lowerCentralSeries G n) (center G)
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
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (n + 1)) ⊥

Tactic:
rw [lowerCentralSeries_succ, closure_eq_bot_iff, Set.subset_singleton_iff]

Premises used: Set.subset_singleton_iff, Subgroup.lowerCentralSeries_succ, Subgroup.closure_eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
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
rw : z * y = y * z
⊢ ⁅y, z⁆ = 1

Tactic:
rw [commutatorElement_def, mul_assoc, ← mul_inv_rev, mul_inv_eq_one, eq_comm]

Premises used: commutatorElement_def, mul_inv_eq_one, mul_assoc, eq_comm, mul_inv_rev
-- Module: Mathlib.GroupTheory.Nilpotent
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
⊢ z * y = y * z

Tactic:
mem_center_iff.mp (h hy1) z

Premises used: Subgroup.mem_center_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Nilpotent
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
⊢ z * y = y * z

Tactic:
exact mem_center_iff.mp (h hy1) z

Premises used: Subgroup.mem_center_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Nilpotent
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
rw : ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Group.IsNilpotent G

Tactic:
rw [nilpotent_iff_lowerCentralSeries]

Premises used: Subgroup.nilpotent_iff_lowerCentralSeries
-- Module: Mathlib.GroupTheory.Nilpotent
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
rcases :
  ∀ (n : ℕ) (hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥),
    ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
rcases nilpotent_iff_lowerCentralSeries.mp ‹_› with ⟨n, hn⟩

Premises used: Subgroup.nilpotent_iff_lowerCentralSeries, Iff.mp
-- Module: Mathlib.GroupTheory.Nilpotent
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
n : ℕ
hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥
h : Eq (α := Subgroup G) (lowerCentralSeries G (n + 1)) ⊥
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
use n + 1
-- Module: Mathlib.GroupTheory.Nilpotent
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
n : ℕ
hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (n + 1)) ⊥

Tactic:
lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)

Premises used: Subgroup.map_eq_bot_iff, Iff.mp, Subgroup.lowerCentralSeries_succ_eq_bot, le_trans
-- Module: Mathlib.GroupTheory.Nilpotent
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
n : ℕ
hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥
h : map f (lowerCentralSeries G n) = ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (n + 1)) ⊥

Tactic:
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)

Premises used: Subgroup.map_eq_bot_iff, Iff.mp, Subgroup.lowerCentralSeries_succ_eq_bot, le_trans
-- Module: Mathlib.GroupTheory.Nilpotent
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
n : ℕ
hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥
⊢ map f (lowerCentralSeries G n) = ⊥

Tactic:
eq_bot_iff.mpr (hn ▸ lowerCentralSeries.map f n)

Premises used: Iff.mpr, Eq.rec, eq_bot_iff, Subgroup.lowerCentralSeries.map
-- Module: Mathlib.GroupTheory.Nilpotent
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
n : ℕ
hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥
⊢ map f (lowerCentralSeries G n) = ⊥

Tactic:
exact eq_bot_iff.mpr (hn ▸ lowerCentralSeries.map f n)

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
⊢ IsNilpotent G

Tactic:
have : IsNilpotent G := isNilpotent_of_ker_le_center f hf1
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
this : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ nilpotencyClass H + 1
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1

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 : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
this : IsNilpotent G
h : Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass H + 1)) ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ nilpotencyClass H + 1

Tactic:
apply Nat.find_min'

Premises used: Nat.find_min'
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
this : IsNilpotent G
h : Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass H + 1)) ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ nilpotencyClass H + 1

Tactic:
classical apply Nat.find_min'

Premises used: Nat.find_min'
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
this : IsNilpotent G
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass H + 1)) ⊥

Tactic:
lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)

Premises used: Subgroup.map_eq_bot_iff, Iff.mp, Subgroup.lowerCentralSeries_succ_eq_bot, le_trans
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
this : IsNilpotent G
h : map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass H + 1)) ⊥

Tactic:
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)

Premises used: Subgroup.map_eq_bot_iff, Iff.mp, Subgroup.lowerCentralSeries_succ_eq_bot, le_trans
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
this : IsNilpotent G
h : map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥
⊢ map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
this : IsNilpotent G
h : LE.le (α := Subgroup H) (lowerCentralSeries H (nilpotencyClass H)) ⊥
⊢ map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥

Tactic:
apply le_trans (lowerCentralSeries.map f _)

Premises used: le_trans, Subgroup.lowerCentralSeries.map
-- Module: Mathlib.GroupTheory.Nilpotent
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 : IsNilpotent H
this : IsNilpotent G
⊢ LE.le (α := Subgroup H) (lowerCentralSeries H (nilpotencyClass H)) ⊥

Tactic:
simp only [lowerCentralSeries_nilpotencyClass, le_bot_iff]

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

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

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

Tactic:
apply eq_top_iff.mpr

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

Tactic:
symm (f.range_eq_top_of_surjective hf)

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

Tactic:
MonoidHom.range_eq_map _

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

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

Tactic:
upperCentralSeries.map hf n

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

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

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

Tactic:
have := nilpotent_of_surjective _ hf