A statement about the center of a direct product

Stream: maths

[Move fast]

 import Mathlib
open Subgroup

variable {n : ℕ}
variable {G : Fin n → Type} [∀ i, Group (G i)]

/--
The center of a direct product is the direct product of the centers:
$$ Z(G_1 \times G_2 \times \cdots \times G_n) = Z(G_1) \times Z(G_2) \times \cdots \times Z(G_n). $$
-/
theorem pro_center_eq_center_pro :
  (Π i : Fin n, center (G i)) = center (Π i : Fin n, G i) := by
  -- We will prove this by showing that the two sets are equal.
  -- First, interpret both sides as subsets of `Π i, G i`.
  apply Set.eq_of_subset_of_subset
  · -- Forward inclusion: (Π i, center (G i)) ⊆ center (Π i, G i)
    intro x hx
    -- Assume `x` belongs to the product of centers.
    -- We need to show that `x * y = y * x` for all `y`.
    have h_comm : ∀ y : Π i, G i, x * y = y * x := by
      intro y
      ext i
      -- Use the fact that `x i` is in the center of `G i`.
      exact (hx i).prop (y i)
    -- This shows that `x` is in the center of the direct product.
    exact mem_center_iff.mpr h_comm
  · -- Reverse inclusion: center (Π i, G i) ⊆ (Π i, center (G i))
    intro x hx i g
    -- Assume `x` belongs to the center of the direct product.
    -- We need to show that `x i` commutes with every element of `G i`.
    -- Construct an element `y` that is non-trivial only at index `i`.
    let y : Π i', G i' := fun i' => if i' = i then g else 1
    -- By definition of the center, `x` commutes with every element of the direct product.
    have h_comm : x * y = y * x := mem_center_iff.mp hx y
    -- Compare the `i`-th component.
    rw [Pi.mul_apply, Pi.mul_apply] at h_comm
    simp only [y, dif_pos (Eq.refl i), dif_neg (ne_of_lt (Fin.lt_succ _))] at h_comm
    exact h_comm

image.png
How can I solve this problem:
(Π i : Fin n, center (G i)) and center (Π i : Fin n, G i) are not the same type, so

  apply Set.eq_of_subset_of_subset

is false.

[Aaron Liu]

In this case you want to use docs#Subgroup.pi

[Move fast]

ok, thank you!