case zero
G : Type ?u.325527
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
⊢ lowerCentralSeries (G₁ × G₂) Nat.zero = prod (lowerCentralSeries G₁ Nat.zero) (lowerCentralSeries G₂ Nat.zero)

case succ
G : Type ?u.325527
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
⊢ lowerCentralSeries (G₁ × G₂) (Nat.succ n) =
    prod (lowerCentralSeries G₁ (Nat.succ n)) (lowerCentralSeries G₂ (Nat.succ n))
G : Type ?u.325527
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
⊢ lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
induction' n with n ih
no goals
case zero
G : Type ?u.325527
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
⊢ lowerCentralSeries (G₁ × G₂) Nat.zero = prod (lowerCentralSeries G₁ Nat.zero) (lowerCentralSeries G₂ Nat.zero)
simp
no goals
case succ
G : Type ?u.325527
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
⊢ lowerCentralSeries (G₁ × G₂) (Nat.succ n) =
    prod (lowerCentralSeries G₁ (Nat.succ n)) (lowerCentralSeries G₂ (Nat.succ n))
calc
  lowerCentralSeries (G₁ × G₂) n.succ = ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ := rfl
  _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤⁆ := by rw [ih]
  _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), (⊤ : Subgroup G₁).prod ⊤⁆ :=
    by simp
  _ = ⁅lowerCentralSeries G₁ n, (⊤ : Subgroup G₁)⁆.prod ⁅lowerCentralSeries G₂ n, ⊤⁆ :=
    (commutator_prod_prod _ _ _ _)
  _ = (lowerCentralSeries G₁ n.succ).prod (lowerCentralSeries G₂ n.succ) := rfl
no goals
G : Type ?u.325527
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
⊢ ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ = ⁅prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n), ⊤⁆
rw [ih]
no goals
G : Type ?u.325527
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
⊢ ⁅prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n), ⊤⁆ =
    ⁅prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n), prod ⊤ ⊤⁆
simp