no goals
ι✝ : Type ?u.3111
α✝ : Type u
β✝ : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α✝
inst✝⁴ : PseudoEMetricSpace β✝
inst✝³ : PseudoEMetricSpace γ
f✝ : α✝ → β✝
x✝ y✝ z : α✝
s : Set α✝
ι : Type u_1
inst✝² : Fintype ι
α : ι → Type u_2
β : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Isometry (f i)
x y : (i : ι) → α i
⊢ edist ((fun g i => f i (g i)) x) ((fun g i => f i (g i)) y) = edist x y
simp only [edist_pi_def, (hf _).edist_eq]