G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥) ≤ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ nilpotencyClass { x // x ∈ H } ≤ nilpotencyClass G
repeat rw [← lowerCentralSeries_length_eq_nilpotencyClass]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → lowerCentralSeries { x // x ∈ H } n = ⊥
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥) ≤ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)
refine @Nat.find_mono _ _ (Classical.decPred _) (Classical.decPred _) ?_ _ _
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → lowerCentralSeries { x // x ∈ H } n = ⊥
intro n hG
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } n) ≤ lowerCentralSeries G n
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
have := lowerCentralSeries_map_subtype_le H n
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this :
  ∀ ⦃x : G⦄ (x_1 : { x // x ∈ H }), x_1 ∈ lowerCentralSeries { x // x ∈ H } n ∧ ↑(Subgroup.subtype H) x_1 = x → x ∈ ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } n) ≤ lowerCentralSeries G n
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
simp only [hG, SetLike.le_def, mem_map, forall_apply_eq_imp_iff₂, exists_imp] at this
no goals
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this :
  ∀ ⦃x : G⦄ (x_1 : { x // x ∈ H }), x_1 ∈ lowerCentralSeries { x // x ∈ H } n ∧ ↑(Subgroup.subtype H) x_1 = x → x ∈ ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
exact eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥) ≤ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥) ≤ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)
rw [← lowerCentralSeries_length_eq_nilpotencyClass]