Dist From Code le iff rel Dist From Code le

theorem distFromCode_le_iff_relDistFromCode_le {C : Set (ι → F)} [Nonempty ι] (u : ι → F) (e : ℕ) :    Δ₀(u, C) ≤ e ↔ δᵣ(u, C) ≤ (e : ℝ≥0) / (Fintype.card ι : ℝ≥0) := by  have h_n_pos : 0 < Fintype.card ι := Fintype.card_pos  have h_n_pos_nnreal : 0 < (Fintype.card ι : ℝ≥0) := by exact_mod_cast h_n_pos  rw [closeToCode_iff_closeToCodeword_of_minDist]  conv_rhs => rw [←ENNReal.coe_div (hr := by    simp only [ne_eq, Nat.cast_eq_zero, Fintype.card_ne_zero, not_false_eq_true])]  rw [relCloseToCode_iff_relCloseToCodeword_of_minDist (u := u) (C := C)    (δ := (e : ℝ≥0) / (Fintype.card ι : ℝ≥0))]  apply exists_congr  intro v  simp only [and_congr_right_iff]  intro hv_mem  rw [pairRelDist_le_iff_pairDist_le]  simp only [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero, Fintype.card_ne_zero, not_false_eq_true,    IsUnit.div_mul_cancel, Nat.floor_natCast]