Exists rel Closest codeword of Nonempty Code

lemma exists_relClosest_codeword_of_Nonempty_Code {ι : Type*} [Fintype ι] {F : Type*}    [DecidableEq F] (C : Set (ι → F)) [Nonempty C] (u : ι → F) :    ∃ M ∈ C, (relHammingDist u M) = δᵣ(u, C) := by  -- 1. Let `f` be the function that gives the relative distance as an NNReal  let f := fun (v : ι → F) => ((relHammingDist u v : ENNReal))  -- 2. Let `S_dists` be the set of all *actual* distances from `u` to `C`.  let S_dists := f '' C  -- 3. Show `S_dists` is non-empty (since C is non-empty)  have hS_nonempty : S_dists.Nonempty := by    -- `S_dists` is the image of a non-empty set `C`.    apply Set.image_nonempty.mpr    (expose_names; exact Set.nonempty_coe_sort.mp inst_2)  -- 4. Show `S_dists` is finite  have hS_finite : S_dists.Finite := by    -- The set of *possible* Hamming distances is finite (a subset of {0..n})    let S_ham_range := (SetLike.coe (Finset.range (Fintype.card ι + 1)) : Set ℕ)    have hS_ham_range_finite : S_ham_range.Finite := Finset.finite_toSet _    -- The set of *actual* Hamming distances `S_ham = {hammingDist u v | v ∈ C}`    -- is a subset of this finite set.    let S_ham := hammingDist u '' C    have hS_ham_finite : S_ham.Finite := by      apply Set.Finite.subset hS_ham_range_finite      intro d hd      simp only [S_ham, Set.mem_image] at hd      rcases hd with ⟨v, _, rfl⟩      simp only [Finset.coe_range, Set.mem_Iio, S_ham_range]      let res := hammingDist_le_card_fintype (x := u) (y := v)      omega    -- `S_dists` is the image of the finite set `S_ham` under `g(d) = d/n`.    -- So `S_dists` is also finite.    have h_img_img : S_dists =      (fun (d : ℕ) => ((((d : ℚ≥0) / ((Fintype.card ι) : ℚ≥0)) : ℚ≥0) : ENNReal)) '' S_ham := by      ext d; simp only [relHammingDist, Set.mem_image, Set.image_image, S_dists, f, S_ham]    rw [h_img_img]    exact Set.Finite.image _ hS_ham_finite  -- 5. Show that `δᵣ(u, C)` is just the `sInf` of this finite, non-empty set.  have h_sInf_eq : δᵣ(u, C) = sInf S_dists := by    -- This follows from `relDistFromCode`'s definition being the `sInf` of    -- all upper bounds, which is equivalent to the `sInf` of the set itself.    let S := {d | ∃ v ∈ C, f v ≤ d}    apply le_antisymm    · -- sInf S ≤ sInf S_dists (because S_dists ⊆ S)      apply csInf_le_csInf      · -- S is bounded below (by 0)        use 0        intro d hd        simp only [Set.mem_setOf_eq] at hd        rcases hd with ⟨v, _, hfv_le_d⟩        exact (zero_le).trans hfv_le_d      · exact hS_nonempty      · -- S_dists ⊆ S        intro d' hd'        simp only [S_dists, Set.mem_image, Set.mem_setOf_eq, f] at hd' ⊢        rcases hd' with ⟨v, hv_mem, rfl⟩        use v    · -- sInf S_dists ≤ sInf S (because sInf S_dists is a lower bound for S)      apply le_csInf      · -- S is nonempty        obtain ⟨v, hv⟩ := Set.nonempty_coe_sort.mp (by (expose_names; exact inst_2))        use (f v : ENNReal)        simp only [Set.mem_setOf_eq]        use v, hv      · intro d' hd'        simp only [Set.mem_setOf_eq] at hd'        rcases hd' with ⟨v, hv_mem, hfv_le_d'⟩        -- `sInf S_dists` is a lower bound for `S_dists`, so `sInf S_dists ≤ f v`.        have h_sInf_le_fv := csInf_le (by          use 0; intro; (expose_names; exact fun a_1 ↦ zero_le)) (Set.mem_image_of_mem f hv_mem)        -- By transitivity, `sInf S_dists ≤ f v ≤ d'`, so `sInf S_dists ≤ d'`.        exact h_sInf_le_fv.trans hfv_le_d'  -- 6. The `sInf` of a finite, non-empty set is *in* the set.  have h_sInf_mem : sInf S_dists ∈ S_dists := by    -- exact NNReal.sInf_mem hS_finite hS_nonempty    exact Set.Nonempty.csInf_mem hS_nonempty hS_finite  -- 7. Unfold the definitions to get the goal.  rw [h_sInf_eq]  -- Goal: `sInf S_dists ∈ S_dists`  -- This is exactly `h_sInf_mem`.  exact h_sInf_mem