G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∃ n, lowerCentralSeries ((i : η) → Gs i) n = ⊥
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ Group.IsNilpotent ((i : η) → Gs i)
rw [nilpotent_iff_lowerCentralSeries]
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n = ⊥
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∃ n, lowerCentralSeries ((i : η) → Gs i) n = ⊥
refine' ⟨n, _⟩
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ ⊥
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n = ⊥
rw [eq_bot_iff]
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ (pi Set.univ fun i => lowerCentralSeries (Gs i) n) ≤ ⊥
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ ⊥
apply le_trans (lowerCentralSeries_pi_le _)
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), lowerCentralSeries (Gs i) n = ⊥
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ (pi Set.univ fun i => lowerCentralSeries (Gs i) n) ≤ ⊥
rw [← eq_bot_iff, pi_eq_bot_iff]
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
i : η
⊢ lowerCentralSeries (Gs i) n = ⊥
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), lowerCentralSeries (Gs i) n = ⊥
intro i
no goals
G : Type ?u.339405
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_1
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
i : η
⊢ lowerCentralSeries (Gs i) n = ⊥
apply lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (h i)