G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
n : ℕ
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ pi Set.univ fun i => lowerCentralSeries (Gs i) n
let pi := fun f : ∀ i, Subgroup (Gs i) => Subgroup.pi Set.univ f
case zero
G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) Nat.zero ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) Nat.zero

case succ
G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ lowerCentralSeries ((i : η) → Gs i) (Nat.succ n) ≤
    Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) (Nat.succ n)
G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
n : ℕ
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
induction' n with n ih
no goals
case zero
G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) Nat.zero ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) Nat.zero
simp [pi_top]
no goals
case succ
G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ lowerCentralSeries ((i : η) → Gs i) (Nat.succ n) ≤
    Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) (Nat.succ n)
calc
  lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
  _ ≤ ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_mono ih (le_refl _))
  _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆ := by simp [pi_top]
  _ ≤ pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_pi_pi_le _ _)
  _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
no goals
G : Type ?u.336571
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆
simp [pi_top]