∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  (f : X ≅ Y) (i : I), CategoryTheory.Pi.isoApp f.symm i = (CategoryTheory.Pi.isoApp f i).symm