no goals
α : Type u
β : Type v
X : Type ?u.396731
ι : Type ?u.396734
inst✝³ : PseudoMetricSpace α
π : β → Type ?u.396742
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
a b : α
⊢ (dist (fun x => a) fun x => b) = dist a b
simpa only [dist_edist] using congr_arg ENNReal.toReal (edist_pi_const a b)