-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_pi_of_finite [Finite η] (n : ℕ) :
    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)
inst✝ : Finite η
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

Proof state:
case succ
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
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, ⊤⁆ := by rw [ih]
  _ = ⁅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_of_finite _ _
  _ = 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)
inst✝ : Finite η
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)
inst✝ : Finite η
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:
case zero
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
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)
inst✝ : Finite η
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, ⊤⁆ = ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆

Tactic:
rw [ih]

Result:
no goals

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
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)
inst✝ : Finite η
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)
inst✝ : Finite η
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)