UDR close iff rel URD close

theorem UDR_close_iff_relURD_close {ι : Type*} [Fintype ι] {F : Type*} [DecidableEq F] [Nonempty ι]    (C : Set (ι → F)) (u : ι → F) :    Δ₀(u, C) ≤ uniqueDecodingRadius C ↔ δᵣ(u, C) ≤ relativeUniqueDecodingRadius C := by  rw [closeToCode_iff_closeToCodeword_of_minDist, relCloseToCode_iff_relCloseToCodeword_of_minDist]  -- Goal: (∃ v ∈ C, Δ₀(u, v) ≤ t) ↔ (∃ v ∈ C, δᵣ(u, v) ≤ τ)  apply exists_congr  intro v  simp only [and_congr_right_iff]  intro hv_mem  -- ⊢ Δ₀(u, v) ≤ t ↔ δᵣ(u, v) ≤ τ  rw [pairRelDist_le_iff_pairDist_le]  set n := (Fintype.card ι : NNReal)  have h_n_pos : 0 < n := by exact NeZero.pos n  conv_lhs => rw [uniqueDecodingRadius_eq_floor_div_2 (C := C)]  dsimp only [relativeUniqueDecodingRadius]  conv_rhs => rw [div_mul_cancel₀ (h := by rw [Nat.cast_ne_zero]; exact Fintype.card_ne_zero)]