Eq of le unique Decoding Radius

theorem eq_of_le_uniqueDecodingRadius {ι : Type*} [Fintype ι] {F : Type*}    [DecidableEq F] (C : Set (ι → F)) (u : ι → F) {v w : ι → F}    (hv : v ∈ C) (hw : w ∈ C)    (huv : Δ₀(u, v) ≤ Code.uniqueDecodingRadius C)    (huw : Δ₀(u, w) ≤ Code.uniqueDecodingRadius C) : v = w := by  -- Handle the edge case where distance is 0 (trivial code)  by_cases hd : ‖C‖₀ = 0  · simp only [uniqueDecodingRadius] at huv huw    simp only [hd, zero_tsub, Nat.zero_div, nonpos_iff_eq_zero, hammingDist_eq_zero] at huv huw    rw [←huv, ←huw]  · -- Main Case: d > 0    apply eq_of_lt_dist hv hw    calc      Δ₀(v, w) ≤ Δ₀(v, u) + Δ₀(u, w) := by exact hammingDist_triangle v u w      _ = Δ₀(u, v) + Δ₀(u, w)        := by simp only [hammingDist_comm]      _ ≤ Code.uniqueDecodingRadius C + Code.uniqueDecodingRadius C := by gcongr      _ < ‖C‖₀                          := by        -- Proof that 2 * ⌊(d-1)/2⌋ < d        simp only [uniqueDecodingRadius]        -- 2 * ((d - 1) / 2) ≤ d - 1        have h_div : 2 * ((‖C‖₀ - 1) / 2) ≤ ‖C‖₀ - 1 := by          rw [mul_comm]          apply Nat.div_mul_le_self (m := ‖C‖₀ - 1) (n := 2)        -- Since d ≠ 0, d - 1 < d        have h_sub : ‖C‖₀ - 1 < ‖C‖₀ := Nat.pred_lt hd        omega