-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_pi_le (n : ℕ) :
    lowerCentralSeries (∀ i, Gs i) n ≤ Subgroup.pi Set.univ
      fun i => lowerCentralSeries (Gs i) n

Proof state:
case succ
η : Type u_2
Gs : η → Type u_3
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) (n + 1) ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) (n + 1)

Tactic:
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, pi_top]
  _ ≤ pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := commutator_pi_pi_le _ _
  _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl

Result:
no goals

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ pi Set.univ fun i => lowerCentralSeries (Gs i) n

Tactic:
let pi := fun f : ∀ i, Subgroup (Gs i) => Subgroup.pi Set.univ f

Result:
η : Type u_2
Gs : η → Type u_3
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

Proof state:
η : Type u_2
Gs : η → Type u_3
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

Tactic:
induction' n with n ih

Result:
case zero
η : Type u_2
Gs : η → Type u_3
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) 0 ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) 0

case succ
η : Type u_2
Gs : η → Type u_3
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) (n + 1) ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) (n + 1)

Proof state:
case zero
η : Type u_2
Gs : η → Type u_3
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) 0 ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) 0

Tactic:
simp [pi_top]

Result:
no goals

Proof state:
η : Type u_2
Gs : η → Type u_3
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 => ⊤⁆

Tactic:
simp [pi, pi_top]

Result:
no goals