no goals
α : Type ?u.32699
β : Type ?u.32702
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ ↑(sphere n d k)
⊢ x ∈ (fun x => ↑(PiLp.equiv 2 fun a => ℝ).symm (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 (Real.sqrt ↑k)
rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]