no goals
p : ℝ≥0∞
𝕜 : Type ?u.494939
𝕜' : Type ?u.494942
ι : Type u_1
α : ι → Type ?u.494950
β : ι → Type u_2
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x y : PiLp p β
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type ?u.495151
inst✝³ : Fintype ι'
E : Type ?u.495157
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ edist (↑(PiLp.equiv p β).symm (Pi.single i b₁)) (↑(PiLp.equiv p β).symm (Pi.single i b₂)) = edist b₁ b₂
simp only [edist_nndist, nndist_equiv_symm_single_same p β i b₁ b₂]