no goals
α✝ : Type u
β : Type v
X : Type ?u.407920
ι : Type ?u.407923
inst✝³ : PseudoMetricSpace α✝
π : β → Type ?u.407931
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (↑(succAbove i) j)
c : ℝ≥0
⊢ nndist (insertNth i x f) (insertNth i y g) ≤ c ↔ max (nndist x y) (nndist f g) ≤ c
simp [nndist_pi_le_iff, i.forall_iff_succAbove]