no goals
α✝ : Type u
β : Type v
X : Type ?u.421600
ι : Type ?u.421603
inst✝³ : PseudoMetricSpace α✝
π : β → Type ?u.421611
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)
⊢ dist (insertNth i x f) (insertNth i y g) = max (dist x y) (dist f g)
simp only [dist_nndist, Fin.nndist_insertNth_insertNth, NNReal.coe_max]