no goals
X : Type ?u.34050
Y : Type ?u.34053
Z : Type ?u.34056
α : Type ?u.34059
ι : Type u_1
π : ι → Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f✝ : X → Y
f g : (i : ι) → π i
⊢ (f ~ᵢ g) ↔ ∀ (i : ι), f i ~ᵢ g i
simp only [Inseparable, nhds_pi, funext_iff, pi_inj]