no goals
E : ℕ → Type ?u.306614
ι : Type u_1
inst✝¹ : Encodable ι
F : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
h : dist x y < (1 / 2) ^ encode i
⊢ dist (x i) (y i) ≤ dist x y
simpa only [not_le.2 h, false_or_iff] using min_le_iff.1 (min_dist_le_dist_pi x y i)