G : Type ?u.332663
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
k : ℕ
⊢ nilpotencyClass (G₁ × G₂) ≤ k ↔ max (nilpotencyClass G₁) (nilpotencyClass G₂) ≤ k
G : Type ?u.332663
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
⊢ nilpotencyClass (G₁ × G₂) = max (nilpotencyClass G₁) (nilpotencyClass G₂)
refine' eq_of_forall_ge_iff fun k => _
no goals
G : Type ?u.332663
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
k : ℕ
⊢ nilpotencyClass (G₁ × G₂) ≤ k ↔ max (nilpotencyClass G₁) (nilpotencyClass G₂) ≤ k
simp only [max_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
  lowerCentralSeries_prod, prod_eq_bot_iff]