Dist row le dist To Interleaved Code

lemma dist_row_le_dist_ToInterleavedCode (U : InterleavedWord A (Fin m) ι) :    ∀ (rowIdx : Fin m), Δ₀((getRow U rowIdx), C) ≤ Δ₀(U, C ^⋈ (Fin m)) := by  intro i  let d_To_interleaved := Code.distFromCode (u := U) (C := C ^⋈ (Fin m))  -- There exists M achieving this distance e_int  have h_exists : ∃ M ∈ C ^⋈ (Fin m), Δ₀(U, M) = d_To_interleaved :=    @Code.exists_closest_codeword_of_Nonempty_Code _ _ _ _      (C ^⋈ (Fin m)) (instNonemptyInterleavedCode (κ := Fin m) (C := C)) U  rcases h_exists with ⟨M, hM_mem, hM_dist⟩  let Uᵢ := getRow U i  let iM : InterleavedCodeword (A := A) (κ := Fin m) (ι := ι) (C := C):= ⟨M, hM_mem⟩  let Mᵢ : C := getRow iM i  -- InterleavedCodeword.getRowCodeword (A := A) (κ := Fin m) (ι := ι) (C := C) (v := iM) i  -- We know d(Uᵢ, C) ≤ d(Uᵢ, Mᵢ) because Mᵢ ∈ C (from h_rows M hM_mem i)  have dist_le_dist : Δ₀(Uᵢ, C) ≤ Δ₀(Uᵢ, Mᵢ) := by    apply csInf_le' -- Using sInf property    --  ⊢ ↑Δ₀(Uᵢ, Mᵢ) ∈ {d | ∃ v ∈ ↑MC, ↑Δ₀(Uᵢ, v) ≤ d}    simp only [Set.mem_setOf_eq, Nat.cast_le]    -- ⊢ ∃ v ∈ C, Δ₀(Uᵢ, v) ≤ Δ₀(Uᵢ, Mᵢ)    use Mᵢ    simp only [Subtype.coe_prop, le_refl, and_self]  apply le_trans dist_le_dist  -- ⊢ ↑Δ₀(Uᵢ, ↑Mᵢ) ≤ Δ₀(U, ↑C_m)  have h_dist_row_le_dist_interleaved : Δ₀(Uᵢ, Mᵢ) ≤ Δ₀(U, M) := by    change Δ₀(getRow U i, getRow M i) ≤ Δ₀(U, M)    exact dist_row_le_dist_ToInterleavedWord U M i  calc    (Δ₀(Uᵢ, Mᵢ): ℕ∞) ≤ (Δ₀(U, M): ℕ∞) :=      ENat.coe_le_coe.mpr h_dist_row_le_dist_interleaved    _ ≤ Δ₀(U, C ^⋈ (Fin m)) := le_of_eq hM_dist