case H
G : Type ?u.351081
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
⊢ ∀ (c : ℕ), nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) ≤ c
G : Type ?u.351081
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
⊢ nilpotencyClass ((i : η) → Gs i) = Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)
apply eq_of_forall_ge_iff
case H
G : Type ?u.351081
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
k : ℕ
⊢ nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) ≤ k
case H
G : Type ?u.351081
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
⊢ ∀ (c : ℕ), nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) ≤ c
intro k
no goals
case H
G : Type ?u.351081
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
k : ℕ
⊢ nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) ≤ k
simp only [Finset.sup_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
  lowerCentralSeries_pi_of_finite, pi_eq_bot_iff, Finset.mem_univ, true_imp_iff]