no goals
α : Type u
β : Type v
X : Type ?u.398493
ι : Type ?u.398496
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ dist (f b) (g b) ≤ dist f g
simp only [dist_nndist, NNReal.coe_le_coe, nndist_le_pi_nndist f g b]