no goals
X : Type u_2
Y : Type u_1
Z : Type ?u.33260
α : Type ?u.33263
ι : Type ?u.33266
π : ι → Type ?u.33271
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)
simp only [Inseparable, nhds_prod_eq, prod_inj]